Dichotomy Theorems

When you try to satisfy a set of rules — color a map so no two neighbors share a color, schedule meetings so no two overlap, assign truth values so a formula holds — you are solving a constraint satisfaction problem (CSP). Some CSPs yield to fast algorithms; others seem to demand searching an exponential space.

A natural question is whether there is any intermediate difficulty: a CSP that is harder than the easy ones but softer than NP-complete. The answer, for enormous families of CSPs, is a clean no.

Schaefer's dichotomy theorem (1978) settled this for all Boolean CSPs — problems where each variable can be true or false. He showed that every Boolean CSP either falls into one of six easy cases (each solvable in polynomial time) or is NP-complete. No Boolean CSP sits in between. The result was stunning: not every individual problem is understood, but the landscape of Boolean constraint satisfaction has no grey zone.

In 2017 Andrei Bulatov and independently Dmitriy Zhuk extended this to all finite domains, resolving the CSP Dichotomy Conjecture posed by Feder and Vardi in 1993. Every CSP over a finite domain is either solvable in polynomial time or NP-complete.

Select a Boolean constraint type from the list. The demo shows sample clauses, lets you pick an assignment, and reveals whether the constraint family is in P or NP-complete according to Schaefer's theorem.

<div class="top-row">
  <label for="ctype">{{label_ctype}}</label>
  <select id="ctype">
    <option value="and">{{opt_and}}</option>
    <option value="or">{{opt_or}}</option>
    <option value="xor">{{opt_xor}}</option>
    <option value="nae">{{opt_nae}}</option>
    <option value="horn2">{{opt_horn2}}</option>
    <option value="maj">{{opt_maj}}</option>
  </select>
</div>
<div id="verdict" class="verdict"></div>
<div id="explanation" class="explanation"></div>
<div class="vars-row">
  <span class="vars-label">{{label_vars}}</span>
  <label><input type="checkbox" id="vA"> a</label>
  <label><input type="checkbox" id="vB"> b</label>
  <label><input type="checkbox" id="vC"> c</label>
</div>
<div id="clauses-area" class="clauses-area"></div>
<div class="btns">
  <button id="checkBtn">{{btn_check}}</button>
  <button id="findBtn">{{btn_find}}</button>
  <button id="resetBtn" class="ghost">{{btn_reset}}</button>
</div>
<div id="result" class="result"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 15px; }
.top-row { display: flex; align-items: center; gap: .6rem; flex-wrap: wrap; margin-bottom: .5rem; }
label { font-weight: 600; }
select { font: 14px system-ui; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px; background: #f5f7fa; color: #222; cursor: pointer; max-width: 340px; }
.verdict { font-size: 1.05rem; font-weight: 700; padding: .35rem .7rem; border-radius: 8px; margin-bottom: .4rem; display: inline-block; }
.verdict.p { background: #d4edda; color: #155724; }
.verdict.npc { background: #f8d7da; color: #721c24; }
.explanation { font-size: .88rem; color: #444; line-height: 1.5; margin-bottom: .7rem; max-width: 540px; }
.vars-row { display: flex; align-items: center; gap: .8rem; margin-bottom: .5rem; }
.vars-label { font-weight: 600; }
.vars-row label { font-weight: 400; display: flex; align-items: center; gap: .3rem; cursor: pointer; }
.clauses-area { display: flex; flex-wrap: wrap; gap: .5rem; margin-bottom: .7rem; min-height: 2.2rem; }
.clause { background: #e8eef3; border: 1px solid #cdd9e3; border-radius: 8px; padding: .3rem .7rem; font: 600 14px ui-monospace, monospace; color: #1d3557; transition: background .15s; }
.clause.sat { background: #d4edda; border-color: #a8d5b3; color: #155724; }
.clause.unsat { background: #f8d7da; border-color: #e8b4b8; color: #721c24; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .5rem; }
button { font: 600 14px system-ui; padding: .42rem .9rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.result { font-size: .95rem; font-weight: 600; min-height: 1.4em; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }

// Code not found

Notice the pattern: AND (Horn clauses) and XOR (linear equations mod 2) are both tractable, yet for completely different algorithmic reasons — unit propagation vs Gaussian elimination. NAE-3SAT (not-all-equal) and 3-coloring-style OR are NP-complete even though they look almost as simple. Schaefer's theorem says there is no other case: every Boolean CSP either matches one of the six tractable templates or reduces to NP-complete.

Schaefer's theorem classifies Boolean CSPs by the type of constraints allowed. A constraint is a relation — a set of allowed tuples. The theorem says:

The six tractable cases (all solvable in polynomial time):

Everything else is NP-complete. If your constraint set escapes all six cases, Schaefer showed you can encode any 3-SAT formula inside your CSP, making it NP-complete.

The proof technique is gadget reduction: craft small constraint patterns that act as AND, OR and NOT gates, then wire them to simulate any Boolean formula. The same wire-and-gate trick that Minesweeper uses to prove NP-completeness is at work here.

Bulatov and Zhuk (2017) extended the classification to all finite domains using universal algebra. They showed that a CSP (over any finite domain) is tractable if and only if its constraint relations are preserved by a Siggers polymorphism — a specific algebraic condition. If no such polymorphism exists, the CSP is NP-complete. This resolved the Feder–Vardi conjecture after 24 years.

The theorem is a proven result — status: solved — proven by Bulatov and Zhuk independently in 2017, building on Schaefer's 1978 foundation and the algebraic framework developed by Jeavons, Cohen, Gyssens, and others throughout the 1990s–2000s.

Knowing the shape of tractability matters far beyond pure theory:

• Solver design: when you add a constraint type to your solver library, the dichotomy tells you in advance whether a polynomial-time algorithm can exist or whether you must fall back to heuristic search or approximation.
• Database query optimization: conjunctive query evaluation maps directly to CSP. The dichotomy theorem implies that the tractability of a query class is determined by its algebraic structure — a result now encoded into database theory.
• Constraint programming languages: language designers use dichotomy results to separate built-in global constraints (tractable) from user-defined constraints that may require backtracking search.
• P vs NP research: dichotomy theorems are one of the few places where the P vs NP question is completely resolved for an infinite family of problems. They show that NP-completeness is not a pathological edge case — it is the generic fate.
• Coding theory and cryptography: affine CSPs (linear equations mod 2) correspond to linear codes. The tractability of affine systems underlies decoding algorithms and lattice-based cryptography.

The lesson: structure determines tractability. Identify your constraint's algebraic type, and the dichotomy tells you which side of the P/NP divide you are on before you write a single line of code.

Schaefer's dichotomy theorem is one of the most elegant results in complexity theory: an infinite family of problems, and yet the complexity landscape has only two levels — polynomial and NP-complete — with nothing in between.

The theorem says that difficulty is not a spectrum but a binary split. The moment your constraints escape the six safe algebraic templates, you inherit the full hardness of P vs NP. There is no gentle slope, no intermediate plateau.

Bulatov and Zhuk's 2017 proof shows this binary split extends to every finite domain, settling a conjecture that stood for 24 years. Together, these results give us a complete map of constraint satisfaction — and they do so in a field where complete maps are extraordinarily rare.

The next time you design a constraint system, check which side of the divide you are on. The answer will tell you whether a clever polynomial algorithm is waiting to be found, or whether you should stop looking and reach for an approximation instead.