A propositional formula in conjunctive normal form is an AND of clauses; each clause is an OR of literals; each literal is a variable or its negation. A total assignment satisfies the formula exactly when at least one literal is true in every clause. The definition is compact, yet naive search traverses an exponential space. Complete solvers therefore interleave decisions, forced implications and backtracking.

The paper calls the underlying family Davis–Putnam search, following contemporary SAT terminology. The loop it sketches is more precisely associated today with the Davis–Putnam–Logemann–Loveland style: choose an unassigned variable, propagate every unit clause, and reverse decisions when propagation reaches contradiction. This naming distinction matters historically but does not change Chaff’s engineering argument.

Boolean constraint propagation, or BCP, applies the unit-clause rule transitively. If every literal in a clause except one is false and the survivor is unassigned, that survivor must become true. A conflict appears if no literal can satisfy a clause, equivalently when implications demand both values of one variable. BCP is logically simple but repeatedly touches clause data, so its physical cost can dominate.

The authors report more than 90 per cent of runtime in BCP for many problems. Elsewhere, for difficult instances under the implemented balance, they give an indicative division of roughly 80 per cent BCP, 10 per cent decision work and 10 per cent conflict analysis. These figures are measurements of their solver and workloads, not universal constants. Their design inference is robust: optimise the operation executed most often and count memory access, not just abstract inference steps.

Chaff therefore offers a methodological claim as important as any individual mechanism. Search quality cannot be judged by decision or conflict counts alone. One decision may trigger many propagations; an intellectually attractive branching score may cost so much to maintain that a cruder choice finishes first. The metric that ultimately matters in the paper is elapsed problem-solving performance under controlled comparisons.

A decision assigns an unassigned variable a tentative value and pushes that choice onto a stack. BCP then adds every value forced by unit clauses. Implications following a decision are tagged with that decision level: a compact indication of the branch state that made them necessary. When a branch conflicts, assignments at invalidated levels are removed and an alternative is tried or a learned analysis sends the solver farther back.

The basic pseudocode alternates decide and bcp. If no variable remains unassigned and propagation has not contradicted a clause, the assignment is a model. If conflict resolution finds no decision with an untried alternative, the formula is unsatisfiable. Completeness comes from preserving alternatives or deriving clauses that soundly prove them impossible.

BCP must reach a fixed point before the next free choice. One unit may imply a second variable, which shortens another clause to a unit, which creates a third assignment. Stopping after one pass would let a decision occur while a logical consequence remains undiscovered. Efficient propagation is consequently not an optional preprocessor; it is the inner closure operation of search.

A clause has four operational states under a partial assignment. It is satisfied when some literal is true; unresolved when at least two literals are not false; unit when exactly one literal is unassigned and all others are false; conflicting when every literal is false. The watched-literal structure must detect transitions into the last two states without repeatedly recounting the whole clause.

Chaff’s later conflict learning is philosophically close to GRASP: analyse implications, add a conflict clause and use unique implication points. The six-page DAC paper explicitly leaves implementation differences largely undescribed because of space. A faithful reconstruction must not invent those missing details or quietly substitute a later first-UIP routine. Chaff’s documented novelty here is the engineering around propagation and choice.

Suppose a clause contains five literals. If its first literal becomes false, four candidates remain; if a second becomes false, three remain. Neither event can make the clause unit. A counter implementation nevertheless locates the clause and mutates its count on both assignments. Across millions of occurrences, those harmless visits dominate memory traffic.

The theoretical ideal is to visit the clause only when its count of false literals changes from N−2 to N−1, the exact boundary into unit status. Maintaining the exact count still costs an update for every falsification and a reverse update for every unassignment. Chaff approximates the ideal with two certificates: as long as two selected literals have not become false, the clause cannot be unit or conflicting.

These certificates are the watched literals. The watch list for literal ℓ contains the clauses currently watching ℓ. Only when ℓ is made false must those clauses be inspected. Occurrences not presently watched disappear from the hot path. A clause remains a logical disjunction of all its literals; watches are an index, not a weakening of semantics.

The distinction between “not false” and “true” is load-bearing. An unassigned watched literal is enough to certify that the clause still has a possible survivor. Requiring two true literals would fail during ordinary partial search. Conversely, watching arbitrary positions without repairing a falsified watch would lose the guarantee that a future unit transition must touch a watch list.

Chaff’s claim is about physical locality as well as visit counts. Clause scanning follows pointers into a large database, and data-cache misses magnify each unnecessary access. The design concentrates work on clauses near a logical transition. It therefore aligns the abstract event: one of two sentinels was falsified: with the memory event: load and examine this clause now.

Let w₁ be the watch just falsified and w₂ the other watch. Load the clause and first consider whether w₂ is true; if so, the clause is already satisfied and no implication is required. Otherwise scan the unwatched literals for one that is not false. If found, replace w₁ with that literal and update the watch lists. The clause returns to sleep.

If no replacement exists, every literal except possibly w₂ is false. If w₂ is unassigned, the clause is unit and BCP assigns it true. If w₂ is also false, the clause conflicts. If w₂ is true, satisfaction was already established. The other watched literal is therefore exactly the place where the only remaining consequence appears.

The initial choice of watches may be arbitrary. Correctness depends on the maintained relationship, not on choosing semantically important literals. Performance can still depend on layout and scan order, because a replacement found early costs less. Yet the logical result is invariant under valid watch choices.

A useful implementation convention stores the two watched literals in privileged positions or keeps explicit watch indices. When a watch moves, only the two affected watch lists need repair. The clause’s other occurrences can remain in a static body. This separation between immutable logical content and mutable access metadata is a general systems pattern.

The paper contrasts Chaff with SATO’s head-and-tail scheme. Both watch two literals, but SATO constrains their direction of motion. Chaff does not impose that fixed direction, and its watches need not be repaired on unassignment. The authors present this difference as central to the asymmetry that makes backtracking cheap; a historical account should preserve SATO’s prior related mechanism rather than claiming two-literal attention appeared from nowhere.

Falsifying variables reduces the set of non-false literals and can threaten the two-watch certificate. Unassigning variables expands that set. Expansion cannot create a new unit clause or conflict; it can only turn a conflict into unit, a unit into unresolved, or preserve satisfaction. Therefore an undo cannot require urgent clause discovery.

Suppose a watch moved from a to c because a became false. Later backtracking unassigns a. Leaving the watch on c is sound: c and the other watch still represent valid non-false positions, and a merely becomes another unwatched candidate. If c is falsified again, the scan may even find a as a replacement. The data structure has no obligation to remember its original geometry.

This gives constant-time unassignment with respect to watch maintenance. The solver pops assignments from its trail and marks variables unknown; it does not traverse all their clause occurrences to decrement counters or reverse watch motion. On backtracking-heavy workloads, avoiding symmetric repair removes a large class of writes and cache misses.

The authors also argue that reassigning a recently undone variable often becomes cheaper. Some clauses that once watched that variable moved their watches elsewhere during the previous descent. They no longer occur on its active watch list, so repeating the assignment visits a smaller subset. Search history has reorganised the index towards the clauses that remain sensitive.

This benefit is amortised and empirical, not a guarantee that every repeat costs less. A later scan can move watches back, and adversarial orders can still cause substantial work. The formal guarantee is narrower: no unit or conflict transition is missed, and undo does not require restoring every watch. The performance claim concerns reduced total accesses under observed search trajectories.

An occurrence-list counter scheme touches metadata for every clause containing each falsified literal. Those clause records may be scattered across memory and larger than cache. Even a constant-time counter update can be slow when its cache line is absent. As formula size grows, the logical operation count understates the cost of fetching remote records.

Watch lists act as a selective frontier. They narrow each falsified literal’s work queue to clauses whose certificate is at risk. Within a visited clause, the implementation scans for a replacement and can arrange its literal storage contiguously. The result reduces both the number of loads and the indirection needed to discover them.

There is no promise that a single watched-literal event is cheaper than incrementing a counter. A visited long clause may scan many literals before finding a replacement. The saving comes from avoiding visits on other assignments and from leaving the structure untouched on undo. Amortised behaviour over an entire search is the relevant unit.

This is why the paper resists judging heuristics by isolated abstract counts. A solver is a composition of logical deductions, indexing choices, allocation policies, cache behaviour and branching trajectories. Changing any component can alter the distribution of work in the others. Chaff’s “careful engineering” is a claim that these layers belong inside algorithm design.

The same lesson survives hardware change. Modern caches, prefetchers and memory capacities differ radically from the 336 MHz UltraSPARC II used in the experiments. Yet irregular pointer-rich data remains costly, and contemporary solvers continue to optimise propagation layout. The historical timing numbers age; the demand to align inference with memory locality does not.

Chaff maintains a counter for each variable in each polarity, initially zero. Whenever a clause is added, the counter for every literal in that clause increases. At a decision, the solver chooses the highest-scoring unassigned literal, with configurable random tie-breaking. Periodically all counters are divided by a constant, so old contributions fade relative to new ones.

The name “variable state independent” describes the score, not eligibility. Assigned variables cannot be selected, but the counter itself is not recomputed from which original clauses are currently unresolved. Chaff maintains an ordered set of unassigned variables during propagation and conflict analysis so the maximum can be retrieved with low decision-time overhead.

On hard instances, conflict clauses accumulate rapidly and dominate literal increments. Decay acts as a low-pass temporal filter: variables appearing in recent learned clauses retain relatively high scores, while old activity recedes. Decisions are thereby coupled to the portion of the formula that recent failures have exposed as difficult.

The score is not a probability that a literal is true, nor a proof that selecting it minimises the remaining tree. It is an attention signal derived from conflict involvement. A high positive-polarity count also selects a polarity in the original presentation. Later solvers changed update schedules, data structures, phase selection and activity scaling; modern EVSIDS should not be read backwards as every detail of 2001 Chaff.

The authors compare against random choice, DLIS and more elaborate state-dependent heuristics. They argue that numbers of decisions or conflicts alone are misleading and report that VSIDS improved the difficult tested problems by roughly an order of magnitude without harming simpler ones. This is empirical support within their workload, not a theorem that VSIDS dominates every distribution.

When BCP falsifies a clause, conflict analysis derives a clause intended to block the responsible combination. Adding it changes the clause database. Its literals receive VSIDS increments, so the same proof object that prunes search also raises attention around the conflict. The next decision may therefore return to the variables most implicated by recent failure.

Learned clauses also enter propagation’s watched structure. A short learned clause can become unit much earlier than the original long clauses from which it was derived. It may then generate another implication, another conflict and another learned clause. Clause learning is therefore not merely a record consulted at the end; it changes the frequency and locality of the hot loop.

This feedback makes isolated comparisons delicate. A faster BCP engine may reach more conflicts in the same wall time, which increases clause production and score updates. A different decision heuristic changes which clauses become unit and which watches move. A deletion threshold changes the propagation database and the evidence retained by VSIDS. Counts downstream of an intervention are effects as well as measurements.

The paper’s engineering philosophy is to profile the complete coupled system. It implemented several published decision heuristics and evaluated their actual speed rather than assuming a “smarter” formula must win. Its strongest claim is consequently architectural: low-overhead mechanisms can compound because each leaves more time for useful search.

This does not eliminate the need for logical validation. An efficient wrong propagator can miss a unit or conflict, and a buggy learned clause can delete real models. A production solver should check small instances against exhaustive truth tables, validate returned assignments directly and, where available, emit independently checkable unsatisfiability proofs. Speed measurements begin only after semantic equivalence is secured.

When an added conflict clause enters the database, Chaff schedules a future relevance test. The paper’s metric asks when more than N of its literals: typically N around 100 to 200: become unassigned for the first time. At that event the clause can be marked deleted. This criterion reflects how far the current search has moved from the state in which the clause was locally constraining.

Marking does not immediately recover its memory. Actual reclamation occurs in an infrequent monolithic database-compaction pass. The common conflict path therefore avoids allocator work and pervasive pointer repairs. Deletion becomes a two-stage process: a cheap logical status change followed by batched physical maintenance.

The policy is scheduled and lazy, not an oracle of permanent uselessness. A deleted learned clause is still an implicate, and it might have helped later. The solver trades potential future pruning against memory and propagation cost. The relevance parameter controls that compromise; keeping every clause protects information but can overwhelm storage and watch traversal.

Clause deletion interacts with completeness under repeated restarts. The paper observes that retaining all learned clauses would preserve the accumulated exclusions, whereas deleting information and indefinitely restarting could in principle avoid exhaustive progress. It suggests increasing relevance limits over time; similarly, expanding restart intervals can ensure eventual coverage. Practical performance and formal fairness need compatible schedules.

Later CDCL systems developed different quality signals, including activity and literal block distance, and much more aggressive database management. Those should not be attributed to the 2001 paper. Chaff’s documented insight here is the separation of scheduled relevance, logical deletion and rare compaction: a systems response to learning’s memory pressure.

Early decisions can trap the solver in a difficult region. Learned clauses reveal structure that was unavailable when those choices were made, yet ordinary backtracking may retain them for a long time. A restart removes the whole trail, allowing VSIDS: now informed by subsequent conflicts: to choose a different early route.

Still-relevant learned clauses remain in the database and retain their watches. They can propagate at the root or prune combinations before the previous conflict depth. Chaff also preserves decision statistics, distinguishing its restart behaviour from a complete reset. Small transient randomness may perturb the first few choices so the solver does not reconstruct the same path exactly.

The paper reports that default Chaff may restart thousands of times on hard satisfiable or unsatisfiable instances, while noting that similar results can sometimes occur with restarts disabled. Frequency and randomness are configurable. These observations support restarts as a robustness mechanism, not a claim that more restarts monotonically improve every instance.

Completeness requires attention because a schedule that always abandons branches while forgetting clauses might postpone some region forever. Chaff expands its restart period by default; the paper also discusses slowly increasing the clause-relevance parameter. Such schedules make room for eventual exhaustive progress while preserving the practical benefit of early resets.

Restarts expose the difference between state and knowledge. The assignment trail is a provisional state describing where the solver currently stands. Learned clauses are justified knowledge about where no solution can stand. Clearing the former while retaining the latter is rational precisely because their epistemic roles differ.

Chaff was compared with GRASP and SATO on almost a thousand formulas. The experiments ran on a four-CPU 336 MHz UltraSPARC II Solaris machine with 4 GB of memory; typical memory use was 50–150 MB depending on runtime. These details anchor the measurements in a specific software and hardware environment.

On many smaller DIMACS sets, all solvers were comparable. Chaff showed advantages on harder pigeonhole and parity classes, while the authors omitted large random 3-SAT f and g sets and par32 because none of the compared solvers performed well. That exclusion narrows the empirical domain and directly contradicts any retelling in which Chaff simply dominated SAT as a whole.

The CMU verification suites produced the most striking results. Chaff completed all instances in several families where GRASP or SATO aborted many under the stated limits. The paper reports approximately one-order improvements on hard satisfiable cases and up to two orders on hard unsatisfiable cases relative to available runs. Some GRASP random-restart configurations could not be locally reproduced because required profiles were unavailable; the authors state this limitation.

One Chaff parameter was changed for the DIMACS pret instances, and comparison solvers were run under selected recommended settings. Aborted times contribute to summary totals, while some families stopped after repeated aborts. The tables are valuable precisely because these conventions are exposed; a modern reproduction would need original binaries, configurations, benchmarks and machine-sensitive controls.

The evidence supports a 2001 result: careful BCP and decision engineering made a complete solver dramatically faster on difficult tested EDA workloads than the public systems the authors could run. It does not establish timeless superiority, identify the isolated causal contribution of every feature, or remove exponential worst cases. Later solver evolution is evidence of influence, not a retroactive randomised trial.

The “move until unit” trace falsifies a, b, c and d. Watches begin on a and b. Each falsified watch moves to a later non-false literal until d fails and e is the only survivor; the clause then implies e=true. Unwatched false assignments would not inspect the clause at all.

The satisfied trace eventually makes a watched literal true. Satisfaction requires no replacement scan until a watched false event threatens the certificate. The conflict trace continues past the unit boundary by assigning the implied survivor false, so the same local mechanism reports that every literal has failed.

Tests are run independently across every prefix of all three traces. A brute-force oracle classifies the full clause without consulting watches. The watch audit asserts that a unit’s only survivor is watched and that unresolved clauses preserve two non-false watches after repair. The undo audit removes the last assignments and requires watch indices to remain byte-for-byte unchanged.

Represent each variable as true, false or unassigned, and keep a trail with decision levels and antecedent clauses for implications. Parse every CNF clause without changing literal polarity. Before optimisation, implement a brute-force clause classifier and a small exhaustive SAT oracle; these become independent references for the watched engine.

Give every non-unit clause two watch positions and index clauses by watched literal. When a watched literal is falsified, check the other watch, search for a non-false replacement, or emit the precise unit or conflict consequence. Mutate both watch lists atomically. Never require watches to return to earlier positions on backtrack.

Validate every assignment prefix. If the brute classifier says unit, the watched routine must identify the sole unassigned literal; if it says conflict, propagation must stop with the offending clause. Verify returned models against original clauses. For learned clauses, verify entailment on small formulas or use proof logging at scale.

Implement VSIDS as the paper defines it before importing later variants: counters for literal polarities, increments on clause addition, periodic division and maximum unassigned selection. Record the exact decay interval, division factor, tie-breaking and ordered-set cost. Do not label a modern EVSIDS heap as a bit-for-bit reproduction.

Separate logical clause deletion from physical compaction and document the relevance threshold. Make restart state explicit: assignments clear, retained clauses and decision statistics remain. Increase schedules if a completeness argument depends on eventual progress. Finally profile clause visits, scanned literals, propagations, cache behaviour, decisions, conflicts, learned-clause growth, compaction time and wall time together.

Review one: scholarship. The reconstruction preserves CNF semantics, unit propagation, decision levels, the paper’s baseline backtracking loop, the two-watched-literal transition, arbitrary initial watches, forward-only repair, constant-time undo, cache-access motivation, SATO’s related head-and-tail scheme, the five stated VSIDS steps, conflict-clause coupling, scheduled lazy deletion, restart state, completeness qualifications and the benchmark environment. It distinguishes documented Chaff from later CDCL conventions.

Review two: teaching and execution. Ten paper-specific SVGs trace runtime allocation, causal trails, quiet clauses, watch repair, undo asymmetry, memory traffic, VSIDS decay, feedback, lazy deletion and restart memory. Twelve examples and twelve causal probes target independent load-bearing links. The laboratory runs three traces and tests every prefix against a separate clause oracle.

Evidence and AI-telltale review. Claims use bounded verbs and carry experimental conditions. The article does not universalise 2001 speedups, pretend omitted benchmark families were victories, describe VSIDS as a truth estimator, attribute later EVSIDS or clause-quality policies to Chaff, or erase SATO’s related watching. Repeated generic praise has been removed in favour of mechanisms and falsifiable interventions.

Accessibility and responsive review. Figures contain unique titles, descriptions, captions and source scopes; colour is redundant with labels; animation stops under reduced-motion preference. Controls are labelled, outputs use text and a live region, tables scroll on narrow screens, and grids collapse at 900 and 600 pixels. The laboratory’s pass/fail claims arise from explicit exact checks rather than decorative status.

Chaff is often remembered through two names: watched literals and VSIDS. Their deeper unity is selective attention. Watches decide which clauses deserve inspection after an assignment; VSIDS decides which variables deserve a choice after recent conflicts. Both replace global rescanning with compact, continuously maintained signals.

The signals have different guarantees. Two valid watches support an exact logical promise: a unit or conflict transition cannot pass unnoticed. VSIDS offers no such optimality theorem; it is an empirical priority that recent conflicts reveal productive neighbourhoods. Combining a sound event filter with a heuristic attention filter is part of the architecture’s strength.

Backtracking and restarting then show two scales of forgetting. Backtracking removes a suffix of assignments but does not reverse the watch index. Restarting removes the entire trail but retains learned clauses and activity. The solver forgets where it stood while keeping structures that summarise why previous positions failed.

Lazy deletion adds a third scale. Learned knowledge is sound yet not free. Some clauses are marked operationally irrelevant and their storage is reclaimed in batches. The system therefore treats memory not as a binary archive but as a managed resource whose contents must justify continuing access cost.

These mechanisms illuminate bounded agency without anthropomorphism. The solver has a goal, provisional commitments, forced consequences, detected contradictions, durable exclusions, decaying priorities and controlled resets. Every component is mechanistic and auditable. Its competence demonstrates how much organised search can emerge from explicit state and carefully engineered access; it supplies no independent evidence of subjective experience.