Every other Backtracking entry on this site tries a candidate, and if it's rejected, undoes it and
tries the next one — a queen placement, a Sudoku digit, a
color, always guessed and then checked.
Boolean satisfiability asks a differently-shaped question: given a set of boolean
variables and a formula built from them as a conjunction of clauses (an AND of ORs —
each clause a disjunction of variables or their negations, all clauses must hold at once), is there
an assignment of true/false to every variable that satisfies the whole
formula? 2-SAT already answers this site's version of that
question for clauses capped at exactly two literals, in linear time, by reducing it to
Strongly Connected Components — that
shortcut only exists because of the two-literal cap. Allow clauses of three or more literals and the
shortcut disappears entirely: general boolean satisfiability is NP-complete, and
this page's algorithm, DPLL (Davis–Putnam–Logemann–Loveland), searches for a
satisfying assignment the same guess-and-backtrack way N-Queens
searches for a placement. What makes it a different kind of backtracking, not just a new
problem: before ever guessing a variable's value, DPLL applies two inference rules that can force a
variable's value outright, with a proof that no other value could work — skipping the trial
entirely, something no other Backtracking entry on this site does even once.
Five variables, x₁ through x₅, and seven clauses:
C1: (x₄ ∨ ¬x₃) C2: (¬x₁ ∨ x₂)
C3: (¬x₄ ∨ ¬x₂) C4: (¬x₂ ∨ x₄)
C5: (¬x₃ ∨ ¬x₅ ∨ ¬x₂)
C6: (x₅ ∨ ¬x₃ ∨ ¬x₄)
C7: (x₄ ∨ ¬x₂ ∨ x₁)
Press Step or Run. At each node, the search first tries to force
a value with no guessing at all: a unit clause (only one literal left unresolved)
forces that literal true; a pure literal (a variable appearing with only one sign
across every not-yet-satisfied clause) can be set to satisfy all of them, since the opposite sign
never appears to conflict. Only when neither rule applies does it decide: pick the
first unassigned variable, try true, recurse, and if that whole branch fails, backtrack
and try false.
clauses:
Both shortcut rules are sound because each one only ever makes a move that every satisfying assignment consistent with what's already fixed would have to agree with anyway — neither one is a guess. A unit clause with one literal left unresolved and every other literal already false has exactly one way left to be satisfied: the last literal must be true. There's no other possibility to weigh, so forcing it costs nothing and loses no solutions. A pure literal is sound for a different reason: if a variable never appears negated anywhere among the clauses still unsatisfied, then setting it to satisfy its own sign can only ever help — every clause it appears in gets satisfied outright, and every clause it doesn't appear in is untouched, so no clause that was still satisfiable before becomes unsatisfiable after. Neither rule can ever throw away a solution that was reachable; they only skip trials whose outcome was already decided.
Run against this page's own seven clauses, the search finds x₁ = x₂ = x₃ =
false — with x₄ and x₅ left
unassigned. That's not a display bug: every clause is already satisfied without
them, and DPLL stops the instant the whole formula is satisfied rather than filling in every
variable for its own sake. The path there, straight from the demo's own reference implementation:
x₃ is pure-negative from the start (it only ever appears as ¬x₃,
in C1/C5/C6) and gets set false immediately, satisfying all three at once with zero
search. Nothing else is forced yet, so the search decides x₁ = true — which unit-propagates
x₂ = true from C2, which unit-propagates x₄ = false from C3, which
leaves C4 (¬x₂ ∨ x₄) with both literals false: a conflict.
Backtrack, try x₁ = false instead — C2 is satisfied outright, and now
x₂ appears only negated across every clause still open (C3, C4, C7), so it's pure and
gets set false, satisfying all three at once. Done: 5 search nodes
total. A plain backtracking search over the same formula — guess every variable in order, check all
seven clauses only once every variable has a value — visits 52 nodes to reach the
same conclusion: the two shortcut rules cut node count by 90.4% here, purely by
proving some trials unnecessary before ever running them.
// Literal encoding: variable v as a non-negative integer; the literal "v is true" is the
// number v itself, the literal "v is false" is the bitwise complement ~v (always negative).
// litVar() undoes either encoding back to the plain variable index; litSign() reports which one it was.
function litVar(l) { return l < 0 ? ~l : l; }
function litSign(l) { return l >= 0; }
// Evaluate one clause against the current partial assignment (a sparse object, var index -> bool).
function evalClause(clause, assign) {
const unresolved = [];
for (const lit of clause) {
const v = litVar(lit);
if (assign[v] === undefined) { unresolved.push(lit); continue; }
const value = litSign(lit) ? assign[v] : !assign[v];
if (value) return { status: 'sat' }; // already satisfied by this literal
}
if (unresolved.length === 0) return { status: 'conflict' }; // every literal false: unsatisfiable
if (unresolved.length === 1) return { status: 'unit', lit: unresolved[0] };
return { status: 'unresolved', lits: unresolved };
}
function dpll(nvars, clauses) {
function solve(assign) {
const assignedHere = [];
// Propagate every unit clause to a fixpoint before ever guessing.
let changed = true;
while (changed) {
changed = false;
for (const clause of clauses) {
const r = evalClause(clause, assign);
if (r.status === 'conflict') { for (const v of assignedHere) delete assign[v]; return { sat: false }; }
if (r.status === 'unit') {
const v = litVar(r.lit);
if (assign[v] === undefined) {
assign[v] = litSign(r.lit);
assignedHere.push(v);
changed = true;
}
}
}
}
// Is every clause satisfied? Also collect one still-unresolved clause's literals, in case not.
let allSat = true, pending = null;
for (const clause of clauses) {
const r = evalClause(clause, assign);
if (r.status === 'conflict') { for (const v of assignedHere) delete assign[v]; return { sat: false }; }
if (r.status !== 'sat') { allSat = false; if (!pending) pending = r.lits; }
}
if (allSat) return { sat: true, assign: Object.assign({}, assign) };
// Pure-literal elimination: a variable appearing with only one sign among unsatisfied clauses
// can be set to satisfy every one of them, no trial needed.
for (let v = 0; v < nvars; v++) {
if (assign[v] !== undefined) continue;
let pos = false, neg = false;
for (const clause of clauses) {
const r = evalClause(clause, assign);
if (r.status === 'sat') continue;
for (const lit of (r.status === 'unit' ? [r.lit] : r.lits)) {
if (litVar(lit) === v) { if (litSign(lit)) pos = true; else neg = true; }
}
}
if (pos !== neg) {
assign[v] = pos; // true if only-positive, false if only-negative
const res = solve(assign);
if (!res.sat) delete assign[v];
for (const u of assignedHere) delete assign[u];
return res;
}
}
// Nothing left to force — decide. Try true, and if the whole branch fails, backtrack to false.
const v = litVar(pending[0]);
for (const val of [true, false]) {
assign[v] = val;
const res = solve(assign);
if (res.sat) return res;
delete assign[v];
}
for (const u of assignedHere) delete assign[u];
return { sat: false };
}
return solve({});
}Flipping which value a pure literal gets set to — the natural off-by-one mistake, since
"appears only negated" and "set it true" sound like they should pair up — turns a sound shortcut
into one that can report a satisfiable formula as unsatisfiable. A tiny hand-checkable
example: three variables and three clauses, (x₁ ∨ ¬x₂),
(¬x₂ ∨ ¬x₁), (¬x₂ ∨ x₃).
x₂ appears only negated across all three, so the correct rule sets it
false immediately — every clause is satisfied outright by ¬x₂
alone, regardless of x₁ or x₃, so the formula is trivially
satisfiable. Flip the rule's sign and it sets x₂ = true instead: clause 1 now
needs x₁ = true to survive (unit propagation), and clause 2 needs
¬x₁ — both x₁ and x₂ true at once, a
direct conflict. Because pure-literal elimination is applied unconditionally, with no fallback
branch the way a decision gets one, that conflict is never retried the other way: the search reports
unsatisfiable for a formula that's actually satisfied by simply leaving
x₂ false. Checked against a from-scratch brute-force oracle over 20,000 random
6-variable instances, this exact sign flip reports the wrong verdict on 34.6% of
them — always the same direction, a real formula wrongly called unsatisfiable, never the reverse.
Checking for a unit clause in a single top-to-bottom sweep over the clause list, instead
of looping back to a fixpoint, still finds the correct answer — just with more branching than
necessary — because a forced assignment near the end of the sweep can't yet trigger a clause nearer
the front that depended on it. Built to show it clearly: a chain of twelve variables,
(x₁) as a unit clause, then (¬x₁ ∨ x₂),
(¬x₂ ∨ x₃), and so on down the chain, listed in reverse order so each
clause depends on a variable the sweep hasn't reached yet. Proper fixpoint propagation resolves the
entire chain — all twelve variables — in a single search node, since it keeps
re-scanning until nothing new is forced. A single sweep per node forces only the first link before
stopping, then treats each remaining link as an ordinary decision to branch on (both
true and false tried) instead of a forced consequence: 7
node visits instead of 1 on this chain, and the gap widens the longer the chain
gets, even though both versions land on the identical satisfying assignment.
Time: O(2n) in the worst case, the same order as every
other search-and-backtrack entry on this site — boolean satisfiability with three or more literals
per clause is NP-complete, so no known algorithm (this one included) avoids exponential worst-case
time on adversarial input; unit propagation and pure-literal elimination shrink the constant factor
in practice, sometimes dramatically as measured above, never the underlying order. Each node's own
work is O(n·m) for n variables and m clauses (every
clause re-evaluated against the current assignment, possibly several times per node during
propagation). Space: O(n + m) for the assignment and the clause list,
plus O(n) for the recursion stack — no separate table, same as every other entry here.
This site's guide, Choosing a Backtracking Strategy, compares this entry against the other ten Backtracking entries side by side, including why this is the first one able to skip a trial outright rather than just reject it quickly. 2-SAT is the special case this page's own general search doesn't need for clauses capped at two literals — that page's own implication-graph shortcut runs in linear time precisely because it never has to guess anything at all.