Generalized satisfiability problems

Oliver Kullmann

(Swansea University)

In my talk I want to discuss "systems of problem instances", a very general (and natural) framework for "satisfiability problems", where it has to be decided whether a "satisfying assignment" of some sort exists or not. Examples for systems of problem instances are clause-sets, constraint satisfaction problems, or systems of polynomial equations over any field (in case of an ordered field like the real numbers also inequalities can be considered).

To handle unsatisfiability for systems of problem instances, a general form of relativised resolution is introduced. Relativised tree resolution in this general context (corresponding to backtracking algorithms searching for satisfying assignments) can be quasi-automatised, that is, there is a (natural) satisfiability decision procedure D* whose running time on unsatisfiable instances is quasi-polynomial in the length of a shortest tree resolution refutation. Full resolution admits a weaker form of automisation. Both general procedures use an "oracle" U for detecting "easy" cases of unsatisfiable instances to capture *relativised* resolution.

An important feature of D* is, that D* also finds satisfying assignments parallel to the search for short refutations. The running time of D* in inputs P is tightly governed by a hardness measure h(P), which on unsatisfiable inputs is closely related to (relativised) tree resolution complexity, and on satisfiable instances now opens up the possibility to prove also some kind of general lower bounds on *satisfiable* inputs.

D* deploys also an oracle S for detection of "easy" satisfiable cases, and thus can be adapted to a given problem class from "practice" (in fact, in this way a far reaching generalisation of Stalmarck's algorithm is reached). Efficient handling of satisfiable inputs needs different algorithmic "resources" than what is needed for handling unsatisfiability, and therefore I consider the separation of oracles U and S as important. In order to construct efficient oracles S, I will give a short overview on the theory of "autarky systems" for the search of satisfying assignments, which enables us to use methods from combinatorial optimisation.
Tuesday 18th September 2001, 14:00
Robert Recorde Room
Department of Computer Science