Schaefer's dichotomy theorem

In computational complexity theory, a branch of computer science, Schaefer's theorem states necessary and sufficient conditions under which a finite set S of Boolean relations yields polynomial-time or NP-complete problems when the relations of S are used to constrain some of the propositional variables. More precisely, Schaefer defines a decision problem which he calls the Generalized Satisfiability problem for S (denoted SAT(S)). An instance of the problem is an S-formula, i.e. a conjunction of constraints of the form $R(x_{i_{1}},\ldots ,x_{i_{n}})$ where R is a relation in S and the $x_{i_{j}}$ are propositional variables. The problem is to determine whether the given formula is satisfiable, in other words if the variables can be assigned values such that they satisfy all the constraints. Special cases of SAT(S) include the variants of Boolean satisfiability problem and the problem can also be viewed as a constraint satisfaction problem over the Boolean domain.

Schaefer identifies six classes of sets of Boolean relations for which SAT(S) is in P and proves that all other sets of relations generate an NP-complete problem. A finite set of Boolean relations S defines a polynomial time computable satisfiability problem if any one of the following conditions holds:

1. all relations which are not constantly false are true when all its arguments are true;
2. all relations which are not constantly false are true when all its arguments are false;
3. all relations are equivalent to a conjunction of binary clauses;
4. all relations are equivalent to a conjunction of Horn clauses;
5. all relations are equivalent to a conjunction of dual-Horn clauses;
6. all relations are equivalent to a conjunction of affine formulae (e.g., $x_{1}\oplus \cdots \oplus x_{n}={\text{true}}$).

On the other hand, if S does not satisfy any of these conditions, the problem SAT(S) is NP-complete.

A modern, streamlined presentation of Schaefer's theorem is given in an expository paper by Hubie Chen.

The analysis was later fine-tuned: SAT(S) is either solvable in co-NLOGTIME, L-complete, NL-complete, ⊕L-complete, P-complete or NP-complete and given S, one can decide in polynomial time which of these cases holds.