In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem, proved by Thomas Jerome Schaefer, states necessary and sufficient conditions under which a finite set S of relations over the Boolean domain yields polynomial-time or NP-complete problems when the relations of S are used to constrain some of the propositional variables. It is called a dichotomy theorem because the complexity of the problem defined by S is either in P or is NP-complete, as opposed to one of the classes of intermediate complexity that is known to exist (assuming P ≠ NP) by Ladner's theorem. Special cases of Schaefer's dichotomy theorem include the NP-completeness of SAT (the Boolean satisfiability problem) and its two popular variants 1-in-3 SAT and not-all-equal 3SAT (often denoted by NAE-3SAT). In fact, for these two variants of SAT, Schaefer's dichotomy theorem shows that their monotone versions (where negations of variables are not allowed) are also NP-complete.
Original presentation Schaefer defines a decision problem that he calls the Generalized Satisfiability problem for S (denoted by SAT(S)), where S = { R 1 , … , R m } {\displaystyle S=\{R_{1},\ldots ,R_{m}\}} is a finite set of relations over the binary domain { 0 , 1 } {\displaystyle \{0,1\}} . An instance of the problem is an S-formula, i.e. a conjunction of constraints of the form R j ( x i 1 , … , x i n ) {\displaystyle R_{j}(x_{i_{1}},\dots ,x_{i_{n}})} where R j ∈ S {\displaystyle R_{j}\in S} and the x i j {\displaystyle 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 as given by the relations from S. 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 relations S over the Boolean domain defines a polynomial-time computable satisfiability problem if any one of the following conditions holds:
all relations that are not constantly false are true when all its arguments are true; all relations that are not constantly false are true when all its arguments are false; all relations are equivalent to a conjunction of binary clauses; all relations are equivalent to a conjunction of Horn clauses; all relations are equivalent to a conjunction of dual-Horn clauses; all relations are equivalent to a conjunction of affine formulae. Otherwise, the problem SAT(S) is NP-complete.
Modern presentation A modern, streamlined presentation of Schaefer's theorem is given in an expository paper by Hubie Chen. In modern terms, the problem SAT(S) is viewed as a constraint satisfaction problem over the Boolean domain. In this area, it is standard to denote the set of relations by Γ and the decision problem defined by Γ as CSP(Γ). This modern understanding uses algebra, in particular, universal algebra. For Schaefer's dichotomy theorem, the most important concept in universal algebra is that of a polymorphism. An operation f : D m → D {\displaystyle f:D^{m}\to D} is a polymorphism of a relation R ⊆ D k {\displaystyle R\subseteq D^{k}} if, for any choice of m tuples ( t 11 , … , t 1 k ) , … , ( t m 1 , … , t m k ) {\displaystyle (t_{11},\dotsc ,t_{1k}),\dotsc ,(t_{m1},\dotsc ,t_{mk})} from R, it holds that the tuple obtained from these m tuples by applying f coordinate-wise, i.e. ( f ( t 11 , … , t m 1 ) , … , f ( t 1 k , … , t m k ) ) {\displaystyle (f(t_{11},\dotsc ,t_{m1}),\dotsc ,f(t_{1k},\dotsc ,t_{mk}))} , is in R. That is, an operation f is a polymorphism of R if R is closed under f: applying f to any tuples in R yields another tuple inside R. A set of relations Γ is said to have a polymorphism f if every relation in Γ has f as a polymorphism. This definition allows for the algebraic formulation of Schaefer's dichotomy theorem. Let Γ be a finite constraint language over the Boolean domain. The problem CSP(Γ) is decidable in polynomial time if Γ has one of the following six operations as a polymorphism:
… excerpt ends here. Continue reading the full article.
