Algebraic Techniques for Satisfiability Problems (English shop)

Preview

Table of Contents, Datei (35 KB)
Extract, Datei (140 KB)

This thesis deals with several generalizations of the classical satisfiability problem,
which plays a central role in complexity theory. Many important complexity classes can
be characterized using satisfiability problems, and many open questions in complexity
theory can be phrased in this context. The classical satisfiability problem is the question,
if a given propositional formula built from variables and the connectors ∧ (and), ∨ (or),
and ¬ (not), has a satisfying truth assignment. This problem can be generalized in several
ways.
First, we can allow arbitrary connectors instead of the three mentioned above. For
many of the classes of formulas which can be defined this way, it can be shown that the
satisfiability problem and other interesting problems can be solved by efficient algorithms.
In this thesis, we study the complexity of the question if a given variable-free Boolean
formula evaluates to 0 or to 1. We also consider the problem of computing the set of
satisfying assignments for a given formula.
Second, formulas in conjunctive normal form are studied. Here, formulas consist of
clauses of a very simple form, which must be satisfied simultaneously. Classical examples
of these problems are 3SAT or 2SAT, where the clauses consist of disjunctions of up to 2 or
3 literals. Again, generalizations can be studied, where arbitrary relations are allowed as
clauses. These problems are called constraint satisfaction problems. For the Boolean case,
the complexity of these problems was determined in 1978 by Thomas Schaefer. He showed
that such problems can either be solved efficiently, or are already NP-complete. In this
thesis, we generalize this “dichotomy”-result in several ways. For the Boolean problem,
we give a complete classification of the cases where efficient algorithms exist and show that
the dichotomy property still holds: there is only a finite number of “complexity degrees”
which arise in this classification. Further, we study the corresponding quantified problem,
where formulas may additionally contain the quantifiers ∃ and ∀. For these formulas, we
study the complexity of satisfiability problems, counting problems, and the equivalence
problem. Again, we show dichotomy-like results: the problems are either solvable by
efficient algorithms, or complete for levels of the polynomial hierarchy.
The main techniques that we use to obtain results on the complexity classifications
of these problems are applications of different algebraic closure operators on the set of
functions and relations. There is an interesting Galois correspondence which allows to
transfer results from one type of restriction to the other. An important question in this
thesis is the question for limitations of the applicability of these techniques.