Questions: SAT Solving and Conflict-Driven Clause Learning

Question 1

What distinguishes CDCL backjumping from the chronological backtracking used in basic DPLL?

• A. CDCL always backtracks to decision level 0 and starts over
• B. CDCL analyzes the conflict to identify the most recent decision actually responsible, then backtracks directly to that level, skipping irrelevant intermediate decisions
• C. CDCL backtracks one level at a time but faster because it uses parallel computation
• D. CDCL never backtracks -- it restarts from scratch whenever a conflict occurs

Answer: (B)

When CDCL detects a conflict, it performs conflict analysis by tracing the implication graph backward to find the set of decisions that caused the conflict. It derives a learned clause from this analysis. The backjump level is determined by the second-highest decision level in the learned clause -- the solver jumps directly there, undoing all intermediate decisions that played no role in the conflict. This non-chronological backjumping can skip many decision levels at once, dramatically pruning the search space compared to chronological backtracking which can only undo one level at a time.

Question 2

Unit propagation determines the value of a variable when a clause has exactly one unassigned literal and all other literals are false.

• T. True
• F. False

Answer: True

A unit clause (or a clause that has become unit under the current partial assignment) has exactly one unassigned literal with all others evaluating to false. The remaining literal must be set to true to satisfy that clause -- this is a forced assignment, not a decision. Unit propagation applies this rule repeatedly: each forced assignment may make additional clauses unit, triggering a cascade of implications. This cascade is recorded in the implication graph, which CDCL later uses for conflict analysis. Efficient unit propagation (via watched literals) is the single most performance-critical component of a CDCL solver.

Question 3

Explain how the watched-literals data structure achieves efficient unit propagation without scanning all clauses after every assignment.

Model answer: Each clause watches exactly two of its unassigned literals. When a variable is assigned, only clauses watching that literal need examination -- not all clauses containing it. A watched literal is replaced only when it becomes false: the solver scans the clause for another non-false literal to watch. A clause requires attention (becomes unit or conflicting) only when both watched literals are false and no replacement can be found. This means most assignments trigger no clause scanning for most clauses, giving amortized near-constant-time propagation.

Watched literals, introduced in the Chaff solver (Moskewicz et al., 2001), were a breakthrough in SAT solver engineering. Unlike earlier schemes that maintained full occurrence lists or head/tail pointers requiring updates on backtracking, watched literals require no bookkeeping during backtracking at all -- the watches remain valid because they only track 'at least two non-false literals exist.' This lazy approach dramatically reduces the overhead of the propagation-backtrack cycle that dominates solver runtime.

Question 4

Why do modern CDCL solvers periodically restart the search despite losing the current partial assignment?

Model answer: Restarts allow the solver to escape from unproductive parts of the search tree where early variable decisions have channeled it into a region containing no solutions. Crucially, learned clauses survive restarts, so the knowledge gained from conflicts is preserved. The combination of restarts with VSIDS heuristics means the solver effectively re-prioritizes its variable ordering based on recently active conflicts, focusing on the variables that matter most. Luby and geometric restart strategies have been shown empirically to improve performance on structured industrial instances by orders of magnitude.

The theoretical justification comes from heavy-tailed runtime distributions observed in combinatorial search: some runs get lucky with early decisions and solve quickly, while others get stuck exponentially long. Restarts with increasing frequency exploit this by repeatedly sampling fresh starting points while retaining learned knowledge. The Luby sequence (1, 1, 2, 1, 1, 2, 4, 1, ...) provides an optimal universal restart strategy for Las Vegas algorithms.