CP-SAT Data Structures: Trail, Watch Lists, and Clause Database

Every modern SAT solver maintains a flat array called the trail (sometimes called the assignment stack). Each slot records one variable assignment in the order it was made. The trail has a crucial extra dimension: every slot is annotated with its decision level — an integer that counts how many branching decisions have been made so far.

The power of this layout is what backjumping costs. When CDCL decides to backjump to asserting level $k$, the implementation does not search for the affected variables — it reads level_start[k+1], slices the trail back to that index, and resets the propagation pointer. The number of variables unset is trail.length - level_start[k+1], each of which is cleared in one array write. No traversal, no searching.

With the trail understood, we need unit propagation to be fast. In a formula with, say, 100,000 clauses, naively checking every clause after every assignment would be quadratic. The two-watched-literal (2WL) scheme, introduced in the Chaff solver in 2001, cuts this cost dramatically. ^{[Chaff: Engineering an Efficient SAT Solver]}

The idea: each clause designates exactly two of its literals as watchers. A global index maps each literal to the list of clauses watching it. When the solver assigns a variable, it only needs to inspect the clauses watching the two literals that just became false — all other clauses are guaranteed to still have at least two unset or true literals, so they cannot yet be unit or conflict.

The key insight: a clause whose watchers are both True or both Unset never wakes up, no matter how many other variables are assigned. The cost of unit propagation is proportional to the number of watcher-falsifications, not to the total number of clauses. In practice, most assignments only wake a small fraction of all clauses.

Clause learning — the core of CDCL — adds a new clause to the database on every conflict. After solving a problem with millions of conflicts, the database can contain hundreds of thousands of learned clauses. This creates a tension: more clauses mean stronger pruning, but they also slow down unit propagation (more watch-list entries to chase) and consume memory. Modern solvers manage this via periodic garbage collection.

The quality metric used almost universally is Literal Block Distance (LBD), introduced in 2009. ^{[Predicting Learnt Clauses Quality in Modern SAT Solvers (LBD)]}

Garbage collection typically runs when the learned clause count exceeds a threshold. The solver sorts clauses by LBD and removes those above a cutoff. Clauses with LBD = 1 or 2 are almost always kept (they are binary or near-binary “glue clauses”). Clauses with high LBD are evicted first.

The trail, the watch lists, and the clause database are not independent — they form a single feedback loop that is the engine of CDCL.

flowchart LR
  A[Decision
Trail append] --> B[2WL Watch-lists
wake clauses watching ¬x]
  B --> C{Unit or Conflict?}
  C -- Unit --> D[Propagate
Trail append + reason]
  D --> B
  C -- Conflict --> E[Conflict analysis
Implication graph]
  E --> F[New learned clause
Clause database append
Watch 2 literals]
  F --> G[Backjump
Trail slice at level_start]
  G --> H[Unit propagation
learned clause fires]
  H --> B
  style A fill:#1d4ed8,color:#e2e8f0
  style F fill:#065f46,color:#e2e8f0
  style G fill:#92400e,color:#fef3c7
  style E fill:#3b0764,color:#e2e8f0

Reading the loop. Every decision appends to the trail. The trail append triggers the 2WL watch-lists: literals that just became false wake up their watching clauses. If a unit clause fires, its forced assignment appends to the trail (with the clause stored as the reason — needed for implication-graph reconstruction). If a conflict is detected, conflict analysis builds the implication graph from the stored reason clauses, derives a learned clause, appends it to the clause database with two watched literals registered, and backjumps by slicing the trail back to level_start[asserting_level + 1]. The newly added learned clause then fires unit propagation immediately, appending to the trail — and the loop continues.