Conflict-Driven Clause Learning (CDCL)

The core deduction engine of a CDCL solver. After a variable is assigned a truth value (True/False), BCP uses unit propagation to deduce the values of other variables forced by unit clauses (clauses with only one unassigned literal). This is performed efficiently using a watch literal data structure, which only examines clauses when one of their two watched literals becomes false, avoiding scanning all clauses after every assignment. BCP continues until either no more deductions can be made (a decision is required) or a conflict (an empty clause) is detected.

When BCP leads to a contradiction (an empty clause), the solver performs conflict analysis. It constructs an implication graph tracing the deductions that led to the conflict. From this graph, it derives a learned clause (or asserting clause) that explains the root cause of the conflict. This new clause is added to the clause database. Key properties of a learned clause:

• It is logically implied by the original formula.
• It is asserting: it will become a unit clause after backtracking, forcing a new deduction.
• It prevents the solver from re-entering the same dead-end search subspace, fundamentally pruning the search tree.

Instead of undoing the last decision (chronological backtracking), CDCL uses the conflict analysis to perform backjumping. The solver calculates the assertion level—the second-highest decision level in the learned clause—and backtracks to that level. All assignments made at higher decision levels are undone. This allows the solver to jump over large portions of the search tree that are irrelevant to the current conflict, guided by the learned clause. This is a direct application of Conflict-Directed Backjumping (CBJ) principles to SAT solving.

A critical data structure optimization for efficient Boolean Constraint Propagation. For each clause, the solver maintains pointers to two unassigned or satisfied literals (the "watched" literals). A clause can only become unit or empty if one of these two watched literals becomes false. This scheme ensures that BCP only needs to examine a clause when one of its watched literals is assigned False, dramatically reducing the overhead of scanning the entire clause database after each assignment. It is the standard implementation for BCP in solvers like MiniSAT and Glucose.

The dominant decision heuristic in modern CDCL solvers. VSIDS prioritizes variables that have recently appeared in learned clauses. It works by:

• Initially: All variable activities are zero.
• On clause learning: Increment the activity score of every variable appearing in the newly learned clause.
• Periodically: Multiply all activity scores by a decay factor (e.g., 0.95).
• For decisions: Choose the unassigned variable with the highest activity score. This heuristic is conflict-driven and efficient, as it focuses the search on the volatile, constrained part of the problem space revealed by recent conflicts.

To manage the potentially exponential growth of the clause database from learning, solvers employ aggressive clause deletion policies. Learned clauses are ranked by metrics like Literal Block Distance (LBD)—a measure of how many decision levels the clause spans. Clauses with high LBD (considered less globally useful) are periodically deleted to free memory and speed up BCP. Restarts are also essential: the solver periodically abandons the current search path, clears all assignments (but keeps learned clauses), and starts anew. This prevents getting stuck in unfruitful regions of the search space and allows the VSIDS heuristic to re-prioritize variables.

The Boolean Satisfiability Problem (SAT) is the canonical NP-complete decision problem of determining whether a given Boolean formula, composed of variables, logical AND (conjunction), OR (disjunction), and NOT (negation), can be assigned truth values (TRUE/FALSE) to make the entire formula evaluate to TRUE. It is the fundamental problem that CDCL solvers are designed to solve efficiently.

• CNF Form: Problems are typically encoded in Conjunctive Normal Form (CNF), a conjunction of clauses, where each clause is a disjunction of literals (a variable or its negation).
• NP-Completeness: Its status as NP-complete means many combinatorial problems (scheduling, verification, planning) can be reduced to SAT, making efficient solvers like CDCL critically important.

The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is the classic, complete, backtracking-based search procedure that forms the direct predecessor to CDCL. It recursively assigns values to variables and backtracks upon encountering a contradiction (an empty clause).

• Core Operations: It relies on unit propagation (forcing the assignment of a variable if a clause becomes a unit) and pure literal elimination (assigning variables that appear only positively or only negatively).
• Contrast with CDCL: Unlike CDCL, DPLL uses chronological backtracking, simply undoing the most recent decision, and does not learn new clauses from conflicts. CDCL enhances DPLL with conflict analysis and non-chronological backtracking.

Conflict-Directed Backjumping (CBJ) is an intelligent backtracking technique used in Constraint Satisfaction Problem (CSP) solvers that directly inspired the non-chronological backtracking in CDCL. When a dead-end (conflict) is reached, CBJ analyzes the reason for the failure.

• Conflict Set: It identifies the set of past variable assignments that are directly responsible for the current inconsistency.
• Non-Chronological Jump: Instead of backtracking one step, the algorithm jumps back to the most recent decision variable in the conflict set, effectively skipping over irrelevant branches of the search tree that did not contribute to the failure. This is a key efficiency gain inherited by CDCL.

Satisfiability Modulo Theories (SMT) is the problem of determining the satisfiability of logical formulas with respect to combinations of background theories (e.g., arithmetic, arrays, bit-vectors). SMT solvers often use a CDCL SAT solver as their Boolean engine.

• Architecture: An SMT solver typically follows a lazy or DPLL(T) approach. The formula is abstracted into a Boolean skeleton. The CDCL engine searches for a satisfying Boolean assignment, which is then checked for consistency with the underlying theories by a theory solver. If inconsistent, a theory lemma (a new Boolean clause) is learned and fed back to the CDCL engine.
• Extended Reach: This allows CDCL to solve problems far beyond pure Boolean logic, including software verification and hybrid systems analysis.

Unit propagation (also called Boolean constraint propagation) is the fundamental inference rule at the heart of CDCL and DPLL search. It is the process that immediately forces variable assignments when a clause becomes a unit clause.

• Mechanism: A clause is a unit clause if all but one of its literals are assigned FALSE under the current partial assignment. To avoid making the entire clause FALSE, the remaining literal must be assigned TRUE.
• Engine of Search: This deterministic deduction is applied exhaustively after every decision (variable assignment). It is responsible for the bulk of the search progress and can lead to cascading implications, efficiently pruning the search space. CDCL's conflict analysis critically relies on tracing the implication graph built by unit propagation.

The First Unique Implication Point (1-UIP) is a specific, dominant heuristic for choosing the asserting clause during conflict analysis in a CDCL solver. It defines the learning and backtracking point.

• Implication Graph: Conflicts are analyzed using a directed graph showing how unit propagation led from decisions to a contradiction.
• 1-UIP Cut: The algorithm traverses backwards from the conflict node, stopping at the most recent node (the 1-UIP) where all paths from the decision variables to the conflict pass through it. The clause derived from this cut has the property of being asserting—it will become a unit clause after backtracking, forcing a new assignment and directing the search into a new region.
• Practical Impact: The 1-UIP scheme is empirically superior, producing short, powerful learned clauses that maximize pruning while controlling database size.