Introduction

Every time a compiler checks for impossible conditions, a chip designer verifies a circuit, or a planner allocates resources, the same question lurks underneath: Is there any assignment of true/false values to a list of boolean variables that satisfies all the constraints? That question is called SAT, and it is NP-complete — yet modern software solves instances with millions of variables in seconds.

The credit goes to two algorithms invented six decades apart. DPLL — named for Martin Davis, Hilary Putnam, George Logemann and Donald Loveland — was published in 1960–1962. It is a systematic backtracking search: pick a variable, guess a value, propagate the forced consequences, and backtrack when a contradiction appears. It works, but it can revisit the same dead end over and over.

CDCL (Conflict-Driven Clause Learning), developed through the 1990s and 2000s in solvers like GRASP, Chaff and MiniSat, adds a single powerful idea: when the solver hits a contradiction, it analyzes the conflict, extracts a compact clause that captures why this path failed, and learns it as a new constraint. Every future branch that would lead to the same failure is pruned immediately — without ever re-exploring it.

The combination is why practical SAT solving went from a theoretical curiosity to an industrial workhorse in one generation.

Try It: Solve SAT Step by Step

The demo below runs a tiny DPLL/CDCL solver on a small 3-SAT instance. Each step shows the current assignment, which unit propagation rules fired, and — when a conflict occurs — the learned clause that prevents the same mistake later.

<div class="demo-layout">
  <div class="formula-panel">
    <div class="panel-title">Formula (3-SAT, 4 variables)</div>
    <div id="clauses"></div>
  </div>
  <div class="right-panel">
    <div class="assign-panel">
      <div class="panel-title">Assignment</div>
      <div id="assignment"></div>
    </div>
    <div class="learned-panel">
      <div class="panel-title">Learned clauses <span id="learned-count">(0)</span></div>
      <div id="learned"></div>
    </div>
  </div>
</div>
<div class="log-box" id="log"></div>
<div class="btns">
  <button id="btn-step" type="button">Step</button>
  <button id="btn-run" type="button">Run</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.demo-layout { display: flex; gap: 10px; margin-bottom: 8px; }
.formula-panel { flex: 1 1 55%; }
.right-panel { flex: 1 1 45%; display: flex; flex-direction: column; gap: 8px; }
.panel-title { font-size: .78rem; font-weight: 700; text-transform: uppercase;
               letter-spacing: .04em; color: #5a7088; margin-bottom: 4px; }
#clauses { display: flex; flex-direction: column; gap: 4px; }
.clause { display: flex; gap: 4px; align-items: center; padding: 5px 8px;
          border-radius: 6px; background: #e8eef3; border: 1px solid #cdd9e3;
          font-family: ui-monospace, monospace; font-size: 13px; flex-wrap: wrap; }
.clause.sat { background: #d4edda; border-color: #a3cfb5; }
.clause.conflict { background: #f8d7da; border-color: #e8a3a8; }
.clause.learned { background: #fff3cd; border-color: #e0c97a; }
.lit { padding: 2px 5px; border-radius: 4px; }
.lit.true-lit { background: #0a7d33; color: #fff; }
.lit.false-lit { background: #c92f3c; color: #fff; text-decoration: line-through; }
.lit.unset-lit { background: #c9ccd1; color: #333; }
.clause-label { font-size: .75rem; color: #888; margin-right: 2px; }
#assignment { display: flex; flex-direction: column; gap: 3px; min-height: 60px; }
.var-row { display: flex; align-items: center; gap: 6px; padding: 3px 6px;
           border-radius: 5px; background: #f4f6f8; font-family: ui-monospace, monospace; }
.var-name { font-weight: 700; min-width: 24px; color: #1d3557; }
.var-val { padding: 1px 8px; border-radius: 4px; font-size: .85rem; }
.var-val.true-val { background: #0a7d33; color: #fff; }
.var-val.false-val { background: #c92f3c; color: #fff; }
.var-val.unset-val { background: #ccc; color: #555; }
.var-reason { font-size: .75rem; color: #666; }
#learned { display: flex; flex-direction: column; gap: 3px; max-height: 90px; overflow-y: auto; }
.log-box { background: #f0f2f5; border-radius: 6px; padding: 6px 10px; height: 72px;
           overflow-y: auto; font-size: .8rem; color: #333; margin-bottom: 8px;
           font-family: ui-monospace, monospace; line-height: 1.5; }
.log-line.info { color: #1d3557; }
.log-line.ok { color: #0a7d33; font-weight: 600; }
.log-line.conflict { color: #c92f3c; font-weight: 600; }
.log-line.learn { color: #b8860b; }
.btns { display: flex; gap: .5rem; }
button { font: 600 13px system-ui; padding: .38rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// DPLL/CDCL demo — 4 variables (A,B,C,D), 6 original 3-SAT clauses.
// Formula: (A|B|C) & (~A|B|D) & (~B|C|~D) & (A|~C|D) & (~A|~C|~D) & (B|~C|D)
// One solution: A=T, B=T, C=F, D=F  (6 satisfying assignments total)
const VARS = ['A','B','C','D'];
const ORIG_CLAUSES = [
  [ 1, 2, 3],   // A|B|C
  [-1, 2, 4],   // ~A|B|D
  [-2, 3,-4],   // ~B|C|~D
  [ 1,-3, 4],   // A|~C|D
  [-1,-3,-4],   // ~A|~C|~D
  [ 2,-3, 4],   // B|~C|D
];

function litName(l) {
  return (l < 0 ? '¬' : '') + VARS[Math.abs(l)-1];
}
function clauseStr(c) { return c.map(litName).join(' ∨ '); }

// Solver state
let clauses, assign, trail, level, decisionLevel, done, sat;

function reset() {
  clauses = ORIG_CLAUSES.map(c => [...c]);
  assign = new Array(VARS.length + 1).fill(null); // 1-indexed; null=unset
  trail = []; // {var, val, level, reason} reason=null for decisions
  level = 0;
  decisionLevel = 0;
  done = false;
  sat = false;
  render();
  setLog([{cls:'info', text:'Formula loaded. Press Step to begin.'}]);
}

// Evaluate a literal given current assignment
function evalLit(l) {
  const v = Math.abs(l), val = assign[v];
  if (val === null) return 'unset';
  return (val === (l > 0)) ? 'true' : 'false';
}

// Evaluate a clause: 'true' if any lit true, 'false' if all false, 'unit' if exactly one unset and rest false, 'open' otherwise
function evalClause(cl) {
  let unset = 0, unitLit = null;
  for (const l of cl) {
    const e = evalLit(l);
    if (e === 'true') return {status:'true'};
    if (e === 'unset') { unset++; unitLit = l; }
  }
  if (unset === 0) return {status:'false'};
  if (unset === 1) return {status:'unit', lit: unitLit};
  return {status:'open'};
}

// Unit propagation; returns {conflict: clause|null, propagated: [{var,val,reason}]}
function unitProp() {
  const propagated = [];
  let changed = true;
  while (changed) {
    changed = false;
    for (const cl of clauses) {
      const e = evalClause(cl);
      if (e.status === 'unit') {
        const l = e.lit, v = Math.abs(l), val = l > 0;
        if (assign[v] !== null) continue;
        assign[v] = val;
        const entry = {v, val, level, reason: cl};
        trail.push(entry);
        propagated.push(entry);
        changed = true;
      } else if (e.status === 'false') {
        return {conflict: cl, propagated};
      }
    }
    // re-check conflicts after propagations
    for (const cl of clauses) {
      if (evalClause(cl).status === 'false') return {conflict: cl, propagated};
    }
  }
  return {conflict: null, propagated};
}

// Conflict analysis: returns learned clause (1UIP approximation)
function analyzeConflict(conflictClause) {
  // Collect all vars at current level in the conflict reason chain
  const involved = new Set();
  function addClause(cl) {
    for (const l of cl) { involved.add(Math.abs(l)); }
  }
  addClause(conflictClause);
  // Walk trail backwards at current level to resolve
  for (let i = trail.length - 1; i >= 0; i--) {
    const t = trail[i];
    if (t.level !== level) continue;
    if (involved.has(t.v) && t.reason) {
      involved.delete(t.v);
      addClause(t.reason);
    }
  }
  // Build learned clause: negate current assignments of involved vars
  const learned = [];
  for (const v of involved) {
    if (assign[v] !== null) learned.push(assign[v] ? -v : v);
  }
  return learned.length > 0 ? learned : conflictClause.map(l => -l);
}

// Backtrack to level bl, undoing assignments above it
function backtrack(bl) {
  for (let i = trail.length - 1; i >= 0; i--) {
    if (trail[i].level > bl) { assign[trail[i].v] = null; trail.splice(i, 1); }
  }
  level = bl;
}

// Pick next unassigned variable (first unset)
function pickVar() {
  for (let v = 1; v <= VARS.length; v++) if (assign[v] === null) return v;
  return null;
}

let logLines = [];
function setLog(lines) { logLines = lines; renderLog(); }
function addLog(l) { logLines.push(l); if (logLines.length > 50) logLines.shift(); renderLog(); }
function renderLog() {
  const box = document.getElementById('log'); box.innerHTML = '';
  logLines.forEach(l => { const d = document.createElement('div'); d.className = 'log-line ' + l.cls; d.textContent = l.text; box.appendChild(d); });
  box.scrollTop = box.scrollHeight;
}

function render() {
  // Clauses
  const cd = document.getElementById('clauses'); cd.innerHTML = '';
  clauses.forEach((cl, i) => {
    const e = evalClause(cl);
    const div = document.createElement('div');
    const isLearned = i >= ORIG_CLAUSES.length;
    div.className = 'clause' + (e.status==='true'?' sat':e.status==='false'?' conflict':'') + (isLearned?' learned':'');
    const lbl = document.createElement('span'); lbl.className = 'clause-label';
    lbl.textContent = isLearned ? `L${i-ORIG_CLAUSES.length+1}` : `C${i+1}`;
    div.appendChild(lbl);
    cl.forEach(l => {
      const s = document.createElement('span'); s.className = 'lit';
      const e2 = evalLit(l);
      s.className = 'lit ' + (e2==='true'?'true-lit':e2==='false'?'false-lit':'unset-lit');
      s.textContent = litName(l);
      div.appendChild(s);
      const sep = document.createElement('span'); sep.textContent = ' '; div.appendChild(sep);
    });
    cd.appendChild(div);
  });
  // Assignment
  const ad = document.getElementById('assignment'); ad.innerHTML = '';
  for (let v = 1; v <= VARS.length; v++) {
    const row = document.createElement('div'); row.className = 'var-row';
    const name = document.createElement('span'); name.className = 'var-name'; name.textContent = VARS[v-1];
    const val = document.createElement('span');
    if (assign[v] === null) { val.className = 'var-val unset-val'; val.textContent = '?'; }
    else { val.className = 'var-val ' + (assign[v] ? 'true-val' : 'false-val'); val.textContent = assign[v] ? 'T' : 'F'; }
    const reason = trail.find(t => t.v === v);
    const reas = document.createElement('span'); reas.className = 'var-reason';
    if (reason) reas.textContent = reason.reason ? '(propagated)' : fmt('(decision L%level%)', { level: reason.level });
    row.appendChild(name); row.appendChild(val); row.appendChild(reas);
    ad.appendChild(row);
  }
  // Learned
  const ld = document.getElementById('learned'); ld.innerHTML = '';
  const learned = clauses.slice(ORIG_CLAUSES.length);
  document.getElementById('learned-count').textContent = '(' + learned.length + ')';
  learned.forEach((cl, i) => {
    const div = document.createElement('div'); div.className = 'clause learned';
    div.style.cssText = 'font-family:ui-monospace,monospace;font-size:12px;padding:3px 6px;border-radius:5px;background:#fff3cd;border:1px solid #e0c97a;';
    div.textContent = `L${i+1}: ` + clauseStr(cl);
    ld.appendChild(div);
  });
  // Button state
  document.getElementById('btn-step').disabled = done;
  document.getElementById('btn-run').disabled = done;
}

// Solver step
let stepState = 'propagate'; // 'propagate' | 'decide'
function step() {
  if (done) return;
  if (stepState === 'propagate') {
    const {conflict, propagated} = unitProp();
    if (propagated.length > 0) {
      addLog({cls:'info', text:fmt('Propagated: %map%', { map: propagated.map(p => VARS[p.v-1]+'='+(p.val?'T':'F')).join(', ') })});
      render();
    }
    if (conflict) {
      addLog({cls:'conflict', text:fmt('Conflict in clause: %clauseStr%', { clauseStr: clauseStr(conflict) })});
      if (level === 0) {
        addLog({cls:'conflict', text:'UNSATISFIABLE — no solution exists.'});
        done = true; render(); return;
      }
      const learned = analyzeConflict(conflict);
      clauses.push(learned);
      addLog({cls:'learn', text:fmt('Learned: %clauseStr%', { clauseStr: clauseStr(learned) })});
      backtrack(Math.max(0, level - 1));
      addLog({cls:'info', text:fmt('Backtracked to level %level%', { level: level })});
      stepState = 'propagate';
      render(); return;
    }
    // Check if all clauses satisfied
    if (clauses.every(cl => evalClause(cl).status === 'true')) {
      addLog({cls:'ok', text:fmt('SATISFIABLE! Solution: %map%', { map: VARS.map((n,i) => n+'='+(assign[i+1]?'T':'F')).join(', ') })});
      done = true; sat = true; render(); return;
    }
    stepState = 'decide';
    if (propagated.length === 0) { step(); return; } // nothing propagated, go decide
    return;
  }
  if (stepState === 'decide') {
    const v = pickVar();
    if (v === null) {
      // All assigned
      if (clauses.every(cl => evalClause(cl).status === 'true')) {
        addLog({cls:'ok', text:fmt('SATISFIABLE! Solution: %map%', { map: VARS.map((n,i) => n+'='+(assign[i+1]?'T':'F')).join(', ') })});
        done = true; sat = true;
      } else {
        addLog({cls:'conflict', text:'UNSATISFIABLE.'});
        done = true;
      }
      render(); return;
    }
    level++;
    assign[v] = true; // decide true first
    trail.push({v, val: true, level, reason: null});
    addLog({cls:'info', text:fmt('Decision L%level%: %v%=T', { level: level, v: VARS[v-1] })});
    stepState = 'propagate';
    render();
  }
}

function runAll() {
  let guard = 0;
  while (!done && guard++ < 2000) step();
  if (guard >= 2000) addLog({cls:'conflict', text:'Guard limit reached.'});
}

document.getElementById('btn-step').addEventListener('click', step);
document.getElementById('btn-run').addEventListener('click', runAll);
document.getElementById('btn-reset').addEventListener('click', reset);
reset();
Result
Console

Press Step to advance one decision or propagation at a time, or Run to solve instantly. Watch the learned clauses panel grow each time a conflict is resolved — those clauses are the memory that makes CDCL so much faster than plain DPLL on hard instances.

The Real Complexity

SAT is NP-complete (Cook–Levin theorem, 1971), so any complete solver must be worst-case exponential unless P = NP. DPLL is no exception: on adversarially chosen formulas it explores 2n2^{n} branches.

But complexity theory also explains why CDCL is faster in practice:

  • Resolution proof system: DPLL implicitly searches for a resolution refutation — a proof that no assignment works. The clauses it derives correspond to resolution steps.
  • CDCL uses non-chronological backtracking: after a conflict, it jumps back not just one level but to the earliest decision that caused the conflict, guided by the learned clause. This is sometimes called backjumping.
  • Superpolynomial separation: in 2004, Ben-Sasson and Wigderson showed that CDCL's clause learning can produce proofs exponentially shorter than any regular-resolution proof. This is a formal separation: there exist formulas where plain DPLL needs 2n2^{n} steps but CDCL needs only polynomially many.
  • Practical heuristics: real solvers add VSIDS (variable-state independent decaying sum) activity scores, restarts, and clause-database management on top of CDCL, pushing the empirical boundary even further.

The key insight is that learned clauses act as lemmas: instead of re-deriving the same fact every time a similar situation arises, the solver stores it and applies it instantly. This is analogous to how human mathematicians build on proved theorems rather than re-proving them from axioms each time.

Despite being NP-complete in theory, modern CDCL solvers routinely handle industrial formulas with 10610^{6} variables — a gap between worst-case and typical-case complexity that is one of the most striking phenomena in all of algorithm design.

Where It Matters

CDCL-based SAT solvers have escaped the theory lab and become indispensable across engineering and science:

  • Hardware verification: Intel, AMD, and ARM use SAT solvers to check that circuits have no reachable bug states. The Pentium FDIV bug (1994) — a famous hardware error — helped motivate formal verification, and modern solvers can check designs with billions of gates.
  • Software model checking: tools like CBMC translate C/C++ programs into SAT formulas and prove (or disprove) properties like "this buffer never overflows."
  • AI planning and scheduling: encoding a planning problem as SAT and handing it to a CDCL solver often beats hand-crafted search — the solver's conflict learning maps naturally onto detecting infeasible sub-plans.
  • Cryptanalysis: attacking block ciphers, hash functions, and stream ciphers can be cast as SAT; CDCL solvers have broken reduced-round variants of several standardized algorithms.
  • MaxSAT and optimization: weighted variants (MaxSAT) extend CDCL to find the assignment that satisfies the most clauses, powering combinatorial optimization and machine-learning training.
  • Package management: dependency resolution in Linux package managers (apt, rpm) is a SAT problem; some distributions use MiniSat under the hood.

Whenever you need to know whether a system of boolean constraints has any solution, DPLL and CDCL are almost certainly the tool of choice — solving instances that pure backtracking could not finish before the heat death of the universe.

Conclusion

DPLL gave computer science its first complete, systematic procedure for satisfiability. CDCL gave it memory — the ability to learn from every dead end and never walk down the same wrong path twice.

Together they illustrate a profound lesson: the worst-case complexity of a problem and the typical difficulty of its instances can be separated by orders of magnitude, and the right algorithmic idea — clause learning, in this case — can cross that gap in one step.

The next time your compiler catches an impossible combination of flags, or your phone's navigation app rules out a route in milliseconds, there is a good chance a CDCL engine is somewhere in the chain. SAT may be NP-complete, but thanks to sixty years of insight, it is also one of the most practically solved hard problems we have — a reminder that P vs NP is a question about worst cases, and the real world rarely hands you the worst case.

Share this article

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

Comments

Loading comments...

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