Introduction

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.

Try It: Classify a Constraint

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">Constraint type:</label>
  <select id="ctype">
    <option value="and">AND / Horn (at most one positive literal)</option>
    <option value="or">OR / 3-SAT clause (general disjunction)</option>
    <option value="xor">XOR / Affine (linear equation mod 2)</option>
    <option value="nae">NAE-3 (not-all-equal, 3 literals)</option>
    <option value="horn2">2-SAT clause (Horn or dual-Horn, 2 literals)</option>
    <option value="maj">Majority (at least 2 of 3 must be true)</option>
  </select>
</div>
<div id="verdict" class="verdict"></div>
<div id="explanation" class="explanation"></div>
<div class="vars-row">
  <span class="vars-label">Variables:</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">Check assignment</button>
  <button id="findBtn">Find satisfying assignment</button>
  <button id="resetBtn" class="ghost">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Schaefer’s Dichotomy Theorem demo.
// Constraint types and their classification:
//   AND/Horn       -> P  (unit propagation)
//   OR/3-SAT       -> NP-complete
//   XOR/Affine     -> P  (Gaussian elimination mod 2)
//   NAE-3          -> NP-complete
//   2-SAT (Horn2)  -> P  (2-SAT algorithm)
//   Majority       -> P  (polymorphism: majority function)

const TYPES = {
  and: {
    label: 'AND / Horn',
    complexity: 'P',
    why: 'Horn clauses (at most one positive literal) are solvable by unit propagation in linear time. This is one of Schaefer’s six tractable cases.',
    // clauses: a AND b, b AND c, a AND c (all must hold)
    clauses: [
      { label: 'a ∧ b', check: (a,b,c) => a && b },
      { label: 'b ∧ c', check: (a,b,c) => b && c },
      { label: '¬a ∨ b', check: (a,b,c) => !a || b },
    ]
  },
  or: {
    label: 'OR / 3-SAT clause',
    complexity: 'NP-complete',
    why: '3-SAT clauses (disjunctions of 3 literals) are the canonical NP-complete constraint. They escape all six of Schaefer’s tractable templates.',
    clauses: [
      { label: 'a ∨ b ∨ c', check: (a,b,c) => a || b || c },
      { label: '¬a ∨ b ∨ c', check: (a,b,c) => !a || b || c },
      { label: 'a ∨ ¬b ∨ ¬c', check: (a,b,c) => a || !b || !c },
    ]
  },
  xor: {
    label: 'XOR / Affine (mod 2)',
    complexity: 'P',
    why: 'Linear equations over GF(2) — XOR constraints — form an affine system solvable by Gaussian elimination in polynomial time. Schaefer’s affine case.',
    clauses: [
      { label: 'a ⊕ b = 1', check: (a,b,c) => (a ^ b) === 1 },
      { label: 'b ⊕ c = 0', check: (a,b,c) => (b ^ c) === 0 },
      { label: 'a ⊕ b ⊕ c = 1', check: (a,b,c) => (a ^ b ^ c) === 1 },
    ]
  },
  nae: {
    label: 'NAE-3 (not-all-equal)',
    complexity: 'NP-complete',
    why: 'Not-all-equal on 3 variables: the tuple cannot be all-true or all-false. NAE-3SAT is NP-complete and falls outside all six of Schaefer’s tractable cases.',
    clauses: [
      { label: 'NAE(a,b,c)', check: (a,b,c) => !((a===b)&&(b===c)) },
      { label: 'NAE(¬a,b,c)', check: (a,b,c) => !((!a===b)&&(b===c)) },
      { label: 'NAE(a,¬b,c)', check: (a,b,c) => !((a===!b)&&(!b===c)) },
    ]
  },
  horn2: {
    label: '2-SAT clause (2 literals)',
    complexity: 'P',
    why: '2-SAT clauses (disjunctions of exactly 2 literals) are solvable in linear time via implication graphs and strongly connected components. A special case of Schaefer’s theorem.',
    clauses: [
      { label: 'a ∨ b', check: (a,b,c) => a || b },
      { label: '¬a ∨ c', check: (a,b,c) => !a || c },
      { label: '¬b ∨ ¬c', check: (a,b,c) => !b || !c },
    ]
  },
  maj: {
    label: 'Majority (≥2 of 3 true)',
    complexity: 'P',
    why: 'A constraint preserved by the majority polymorphism: f(x,y,z) = majority(x,y,z). Algebraically this makes the CSP tractable — one of the polymorphism-based tractable cases generalised by Bulatov–Zhuk.',
    clauses: [
      { label: 'maj(a,b,c)', check: (a,b,c) => (a+b+c) >= 2 },
      { label: 'maj(a,b,¬c)', check: (a,b,c) => (a+b+(!c?1:0)) >= 2 },
      { label: 'maj(¬a,b,c)', check: (a,b,c) => ((!a?1:0)+b+c) >= 2 },
    ]
  }
};

let currentType = 'and';

function getVars() {
  const a = document.getElementById('vA').checked ? 1 : 0;
  const b = document.getElementById('vB').checked ? 1 : 0;
  const c = document.getElementById('vC').checked ? 1 : 0;
  return [a, b, c];
}

function renderVerdict(type) {
  const t = TYPES[type];
  const v = document.getElementById('verdict');
  v.textContent = t.label + ' → ' + t.complexity;
  v.className = 'verdict ' + (t.complexity === 'P' ? 'p' : 'npc');
  document.getElementById('explanation').textContent = t.why;
}

function renderClauses(type) {
  const [a, b, c] = getVars();
  const area = document.getElementById('clauses-area');
  area.innerHTML = '';
  TYPES[type].clauses.forEach(cl => {
    const div = document.createElement('div');
    const sat = cl.check(a, b, c);
    div.className = 'clause';
    div.textContent = cl.label;
    area.appendChild(div);
  });
}

function checkAssignment() {
  const [a, b, c] = getVars();
  const t = TYPES[currentType];
  const area = document.getElementById('clauses-area');
  let allSat = true;
  Array.from(area.children).forEach((div, i) => {
    const sat = t.clauses[i].check(a, b, c);
    div.className = 'clause ' + (sat ? 'sat' : 'unsat');
    if (!sat) allSat = false;
  });
  const r = document.getElementById('result');
  if (allSat) {
    r.textContent = fmt('✓ All constraints satisfied for a=%a%, b=%b%, c=%c%.', { a: a, b: b, c: c });
    r.className = 'result ok';
  } else {
    r.textContent = '✗ Some constraint violated. Try a different assignment.';
    r.className = 'result bad';
  }
}

function findAssignment() {
  const t = TYPES[currentType];
  let found = null, checked = 0;
  for (let mask = 0; mask < 8; mask++) {
    checked++;
    const a = (mask >> 2) & 1;
    const b = (mask >> 1) & 1;
    const c = mask & 1;
    if (t.clauses.every(cl => cl.check(a, b, c))) {
      found = [a, b, c];
      break;
    }
  }
  const r = document.getElementById('result');
  if (found) {
    document.getElementById('vA').checked = !!found[0];
    document.getElementById('vB').checked = !!found[1];
    document.getElementById('vC').checked = !!found[2];
    renderClauses(currentType);
    r.textContent = fmt('✓ Found: a=%v%, b=%v2%, c=%v3% (checked %checked%/8 assignments).', { v: found[0], v2: found[1], v3: found[2], checked: checked });
    r.className = 'result ok';
    const area = document.getElementById('clauses-area');
    Array.from(area.children).forEach((div, i) => {
      div.className = 'clause sat';
    });
  } else {
    r.textContent = '✗ No satisfying assignment exists (all 8 tried).';
    r.className = 'result bad';
  }
}

function reset() {
  document.getElementById('vA').checked = false;
  document.getElementById('vB').checked = false;
  document.getElementById('vC').checked = false;
  renderClauses(currentType);
  const r = document.getElementById('result');
  r.textContent = '';
  r.className = 'result';
  const area = document.getElementById('clauses-area');
  Array.from(area.children).forEach(div => div.className = 'clause');
}

document.getElementById('ctype').addEventListener('change', function() {
  currentType = this.value;
  renderVerdict(currentType);
  renderClauses(currentType);
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
  const area = document.getElementById('clauses-area');
  Array.from(area.children).forEach(div => div.className = 'clause');
});

document.getElementById('checkBtn').addEventListener('click', checkAssignment);
document.getElementById('findBtn').addEventListener('click', findAssignment);
document.getElementById('resetBtn').addEventListener('click', reset);

// Initial render
renderVerdict(currentType);
renderClauses(currentType);
Result
Console

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.

The Real Complexity

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):

Case Allowed constraints Why tractable
0-valid every relation contains the all-zeros tuple trivially satisfiable
1-valid every relation contains the all-ones tuple trivially satisfiable
Horn clauses with at most one positive literal unit propagation
dual Horn clauses with at most one negative literal unit propagation
Affine linear equations over GF(2) Gaussian elimination
2-colorable every relation is the kernel of an XOR-like symmetry 2-SAT-style algorithm

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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/dichotomy-theorems/Content licensed under CC BY-NC 4.0.