Let the Clause Sleep
Most clauses in a SAT solver deserve to be ignored most of the time.
That is not a philosophical statement. It is an implementation opportunity.
A clause like
(a OR ~b OR c OR d OR ~e OR f)
does not need attention when its first literal becomes false, then its second, then its third. It only becomes operationally interesting when the assignment has nearly killed it:
all literals false except one -> force the remaining literal
all literals false -> conflict
Modern SAT solvers spend a large fraction of their time doing Boolean constraint propagation: repeatedly finding clauses that have become unit, assigning the forced literal, and stopping when a conflict appears or no more implications can be found. The Chaff paper put the engineering point bluntly: BCP dominates SAT runtime on many instances, so the propagation engine is the heart of the solver.1
The trick is to let clauses sleep until there is real news.
Before Learning, There Is Propagation
The Davis-Putnam-Logemann-Loveland procedure gave the classic backtracking shape for propositional satisfiability: simplify by unit clauses and pure literals, split on a variable, and recurse.2 In modern SAT-solver language, we usually describe the loop as:
decide a variable
propagate forced consequences
if conflict, analyze and backtrack
repeat
Conflict-driven clause learning, developed through systems such as GRASP and Chaff, made conflicts useful rather than merely terminal. A conflict can explain which earlier decisions caused trouble, produce a learned clause, and backjump past irrelevant decisions.3 MiniSat later became famous partly because it showed how small and extensible a Chaff-style solver could be while still containing the essential machinery.4
But before conflict analysis can do anything, the solver must discover implications. That means it must notice clauses that have become unit.
The naive thought is:
when literal L becomes false,
visit every clause containing L
inspect the clause
if it is unit, enqueue the remaining literal
if it is false, report conflict
This is already better than scanning the whole formula. It uses occurrence lists. But it still wakes many clauses that cannot possibly be unit yet.
If a six-literal clause has four live literals left, it is not unit. The solver does not need to know exactly which four. It only needs a certificate that at least two are still not false.
That certificate is two watched literals.
Clause Sets Two Alarms
For every clause, pick two literals to watch. Maintain this invariant:
if the clause might become unit, one of the watched literals will reveal it
Operationally, when a watched literal becomes false, the solver visits that clause and tries to move the watch to another literal that is not false. If it can move the watch, the clause goes back to sleep. It still has at least two non-false literals, so it cannot be unit.
If it cannot move the watch, the other watched literal determines the clause’s state:
other watch true -> clause is already satisfied
other watch unassigned -> clause is unit; assign the other watch
other watch false -> conflict
The solver does not maintain an exact count of false literals in every clause. It maintains a cheap alarm system.
This is why watched literals are so effective. A clause with ten literals can ignore the first several falsifications if they are not watched. If a watched literal is falsified, the clause often pays a short scan to find a replacement and then goes back to sleep.
The second half of the trick is backtracking. Chaff emphasized that watched literals do not need to be repaired when variables are unassigned.1 A watch that was valid before backtracking remains safe after backtracking because unassigning variables can only make literals less false. That turns undoing a decision level into stack popping, not clause surgery.
Two Engines, Same Trail
The lab below generates a planted CNF formula: random clauses plus a chain of binary implications. It runs two propagation engines on the same decisions:
- an occurrence-list engine that visits every clause containing the newly falsified literal,
- a two-watched-literal engine that visits only clauses currently watching that falsified literal.
Both engines implement the same unit-propagation semantics. The lab checks that they agree: if propagation finishes, the final assignments match; if propagation conflicts, both engines detect a conflict.
The occurrence-list engine is not a straw man: it only visits clauses that contain the literal just falsified. The watched-literal engine asks a narrower question: was that falsified literal one of the clause's two alarms?
What the Bars Count
The lab is not solving SAT end-to-end. There is no VSIDS heap, learned-clause database, restart policy, or first-UIP conflict analysis. It isolates the propagation kernel.
That isolation is deliberate. In a CDCL solver, the famous trick is conflict learning: turn a contradiction into a clause that prevents repeating the same mistake. But conflict learning only pays off if the engine can cheaply run the boring loop:
take one newly assigned literal
find consequences
enqueue consequences
repeat
The occurrence-list engine and the watched engine produce the same logical consequences. Their cost differs because they ask different memory questions.
The occurrence-list engine asks:
which clauses contain this falsified literal?
The watched engine asks:
which clauses are currently watching this falsified literal?
The second set is much smaller when long clauses have already moved their watches away from dying literals. In the default lab setting, the watched engine visits less than half as many clauses and reads about a third as many literals. Move the clause width up and the effect often gets larger. Add wrong decisions and the run may stop at a conflict; the engines still agree that propagation has failed, though their partial trails can differ because the conflict was found before a unique fixed point was reached.
That last caveat is important. Watched literals are not a theorem that every micro-count is lower on every input. They are an engineering data structure that usually removes irrelevant memory traffic from the solver’s hottest loop.
Backtracking Makes the Trick Better
The watch invariant is asymmetric in time.
When assigning variables, a watched literal can become false, so the clause may need repair. When backtracking, variables become unassigned. A false literal can become unknown, but an unknown literal cannot make a previously safe clause more dangerous.
So there is no work to do.
That is the small gift. The solver can pop assignments off the trail without walking through all affected clauses and repairing their counters. The watched positions may be arbitrary, but they remain sound. They are not a summary of the current clause state. They are a lazily maintained alarm.
This is why the data structure feels almost too simple after you see it. A clause does not need to know exactly how close it is to failure. It only needs two witnesses that it is not there yet.
Around the Alarm System
Watched literals are one piece of a larger design.
GRASP helped establish conflict analysis, nonchronological backtracking, and conflict-induced clauses as core SAT ideas.3 Chaff combined fast BCP, VSIDS-style branching, and engineering attention to memory behavior.1 MiniSat compressed the design into a solver that became a reference point for researchers and implementers.4
The through-line is not that SAT became easy. SAT remains NP-complete. The through-line is that solver performance came from a stack of concrete representational decisions:
- store implications on a trail;
- explain implications by clauses;
- learn clauses from conflicts;
- rank variables by recent conflict activity;
- keep clauses dormant until they can matter.
The last item is the watched-literal trick. It does not reduce the search space by itself. It makes each node of the search tree cheaper to process.
That distinction is easy to miss. A heuristic changes where the solver walks. A watch list changes how much it pays for each step.
Weak Witnesses Are a Design Pattern
The broader software lesson is useful outside Boolean formulas:
do not eagerly maintain the exact statistic if a cheap witness is enough
A clause could maintain a counter of false literals. That counter would be more informative than two watches. It would also be updated constantly. Watched literals keep a weaker invariant that is exactly strong enough for the next operational decision.
You see the same pattern in good systems code:
- dirty bits instead of eagerly recomputed state;
- indexes that wake only on relevant keys;
- incremental compilers that invalidate dependency edges, not whole programs;
- caches that keep enough metadata to avoid scanning cold entries;
- streaming sketches that preserve the query contract, not the raw data.
The art is choosing the witness. Too weak, and the system wakes up too late. Too strong, and the witness becomes the workload.
Two watched literals hit a beautiful point: they are weak enough to be cheap, strong enough to preserve unit propagation, and stable under backtracking.
That is why this tiny data structure belongs in the same conversation as conflict learning. Clause learning tells the solver what not to forget. Watched literals tell the solver what it can safely ignore.
-
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, “Chaff: Engineering an Efficient SAT Solver”, DAC 2001. ↩ ↩2 ↩3
-
Martin Davis, George Logemann, and Donald Loveland, “A Machine Program for Theorem-Proving”, New York University Institute of Mathematical Sciences report, 1961; later published in Communications of the ACM, 1962. ↩
-
Joao P. Marques-Silva and Karem A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers, 1999. ↩ ↩2
-
Niklas Een and Niklas Sorensson, “An Extensible SAT-solver”, SAT 2003. ↩ ↩2