Math 2.0

Computer science Computational complexity: resources and classes Theorem

Schaefer's dichotomy theorem

Builds on Constraint satisfaction problemBoolean satisfiability problemPNP-completenessConjunctive normal formLadner's theorem

Statement

Let Γ\Gamma be a finite set of nonempty relations on {0,1}\set{0, 1}. Let SAT(Γ)\mathrm{SAT}(\Gamma) be the constraint satisfaction problem CSP(Γ)\mathrm{CSP}(\Gamma) with domain {0,1}\set{0, 1}. Then SAT(Γ)\mathrm{SAT}(\Gamma) lies in P if at least one of the following holds.

  1. Every relation in Γ\Gamma contains the all-zero tuple.
  2. Every relation in Γ\Gamma contains the all-one tuple.
  3. Every relation in Γ\Gamma is the set of models of a conjunctive normal form whose clauses each have at most one positive literal.
  4. Every relation in Γ\Gamma is the set of models of a conjunctive normal form whose clauses each have at most one negative literal.
  5. Every relation in Γ\Gamma is the set of models of a conjunctive normal form whose clauses each have at most two literals.
  6. Every relation in Γ\Gamma is the set of solutions of a system of linear equations over the field 𝔽2\F_2.

Otherwise SAT(Γ)\mathrm{SAT}(\Gamma) is NP-complete.

Remarks

The classes are called 00-valid, 11-valid, Horn, dual Horn, bijunctive and affine. In cases 1 and 2 the constant assignment works. In cases 3 and 4 unit propagation decides the problem, in case 5 the method for 2-SAT does, and in case 6 Gaussian elimination does. For the hardness, assume that none of the six conditions holds. Schaefer showed that the relations of Γ\Gamma then express every Boolean relation by existentially quantified conjunctions, possibly with the help of constants. So SAT reduces to SAT(Γ)\mathrm{SAT}(\Gamma). Thomas Schaefer proved the theorem in 1978.

Example: 3-SAT is SAT(Γ)\mathrm{SAT}(\Gamma) for the eight relations given by clauses of three literals. The relation of the clause x∨y∨zx \lor y \lor z fails conditions 1, 3, 5 and 6, and the relation of ¬x∨¬y∨¬z\neg x \lor \neg y \lor \neg z fails conditions 2 and 4. So 3-SAT is NP-complete, in agreement with the Cook–Levin theorem.

Going deeper

For a student

The theorem is the two-element case of the dichotomy for constraint satisfaction problems on finite domains. That general dichotomy, conjectured by Feder and Vardi, was proved by Bulatov and by Zhuk in 2017. By Ladner's theorem, NP contains intermediate problems if P≠NP\mathrm{P} \ne \mathrm{NP}, so a dichotomy for a whole family is a strong structural fact. The six tractable cases are described by closure under polymorphisms: constants, the binary minimum, the binary maximum, the majority operation, and the operation x+y+zx + y + z modulo 22.

Reading path

To understand this page from the ground up, read these 18 pages in order. The foundations come first.

Show the path as a graph
Conjunctive normal form, concept, no evidence levelConjunctive normal fo…conceptGraph homomorphism, concept, no evidence levelGraph homomorphismconceptNP, concept, no evidence levelNPconceptNP-completeness, concept, no evidence levelNP-completenessconceptP, concept, no evidence levelPconceptPolynomial-time reduction, concept, no evidence levelPolynomial-time reduc…conceptProposition, concept, no evidence levelPropositionconceptSatisfiability, concept, no evidence levelSatisfiabilityconceptConstraint satisfaction problem, problem, no evidence levelConstraint satisfacti…problemLadner's theorem, statement, no evidence levelLadner's theoremstatementConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionPropositional logic, concept, no evidence levelPropositional logicconceptBoolean satisfiability problem, problem, no evidence levelBoolean satisfiabilit…problemSchaefer's dichotomy theorem, statement, no evidence levelSchaefer's dichotomy …statement
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Conjunctive normal form concept
  2. Graph homomorphism concept
  3. NP concept
  4. NP-completeness concept
  5. P concept
  6. Polynomial-time reduction concept
  7. Proposition concept
  8. Satisfiability concept
  9. Constraint satisfaction problem problem
  10. Ladner's theorem statement
  11. Conjunction definition
  12. Disjunction definition
  13. Implication definition
  14. Negation definition
  15. Biconditional definition
  16. Propositional logic concept
  17. Boolean satisfiability problem problem
  18. Schaefer's dichotomy theorem statement

Further reading

  1. Web https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem
About this page
TagHFW5G8EG99
URIm2://HFW5G8EG99
Kindstatement, theorem
WritingW0 stub
MSC68Q17, 03B05
StatusThis copy of the site has no build data. Run m2 status HFW5G8EG99.
AboutConstraint satisfaction problem
UsesConstraint satisfaction problem, Boolean satisfiability problem, P, NP-completeness, Conjunctive normal form, Ladner's theorem
Same as
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.