Conflict-driven clause learning
Conflict-driven clause learning, commonly abbreviated CDCL, is an algorithmic framework for determining the satisfiability of propositional formulas expressed in conjunctive normal form. It extends the DPLL algorithm by deriving new clauses from conflicts, returning nonchronologically to an earlier decision level, and retaining selected information obtained during failed portions of the search. Modern Boolean satisfiability problem solvers generally combine this framework with specialized branching heuristics, efficient propagation structures, restart policies, and mechanisms for deleting learned clauses.
A CDCL solver searches for an assignment satisfying a formula
[ F=C_1\land C_2\land\cdots\land C_m, ]
where every clause (C_i) is a disjunction of literals. A conflict occurs when the current partial assignment makes every literal in some clause false. Rather than treating the conflict solely as a signal to reverse the most recent decision, the solver analyzes the implications that produced it and derives a clause excluding a broader class of incompatible assignments.
Search state and propagation
The state of the search is represented by a partial assignment arranged as an ordered trail. Each assigned variable is associated with a decision level. A variable introduced directly by the branching heuristic begins a new level, whereas assignments forced by existing clauses remain at the level at which their antecedents became active.
The principal inference rule during search is unit propagation. If all but one literal in a clause are false and the remaining literal is unassigned, that remaining literal must be true in every extension satisfying the clause. The clause responsible for such an assignment is recorded as its reason clause. Decision assignments have no reason clause because they arise from the solver's branching policy rather than from logical implication by the current formula.
Most implementations organize propagation through the watched-literal method. Each non-unit clause maintains two designated literals, and the clause ordinarily requires examination only when one of those literals becomes false. This representation avoids repeatedly scanning every clause after each assignment and permits propagation cost to depend largely on the clauses affected by recent changes to the trail.
A conflict clause is encountered when propagation determines that both watched literals, together with every other literal in the clause, are false. At that point the current decision path cannot be extended into a satisfying assignment. The conflict nevertheless contains information about an entire region of the search space rather than only about the latest branch.
Implication graphs and conflict analysis
The causal structure of the current trail can be represented by an implication graph. Vertices correspond to assignments, while directed edges connect the assignments falsifying the other literals of a reason clause to the assignment implied by that clause. Decision assignments appear as vertices without incoming reason edges, and a conflict is represented by a terminal node whose predecessors jointly falsify the conflicting clause.
Conflict analysis applies propositional resolution to the conflict clause and to reason clauses associated with assignments at the current decision level. Given clauses
[ (A\lor x) ]
and
[ (B\lor\neg x), ]
resolution on (x) produces the logical consequence
[ A\lor B. ]
Repeated resolution removes selected current-level literals from the developing conflict clause. The resulting clause is entailed by the original formula because every individual resolution step preserves logical consequence.
A widely used stopping condition is the first unique implication point, usually written first UIP. Within the implication graph, a UIP is a current-level assignment through which every directed path from the current decision assignment to the conflict passes. Resolution terminates when the learned clause contains exactly one literal assigned at the current decision level. That literal is the negation of the first-UIP assignment, while the other literals identify assignments at earlier levels that jointly caused the conflict.
You Watanabe's late-1990s work on implication-graph cut selection established an equivalent trail-based formulation of first-UIP analysis in which reason clauses are resolved in reverse assignment order. This formulation treated the graph as an implicit structure recoverable from the trail and its antecedent references, rather than as a separately allocated graph. It entered several contemporary solver implementations because the same bookkeeping used for propagation could also support clause derivation.
Learned clauses and nonchronological backtracking
Suppose conflict analysis produces the learned clause
[ L=(\ell\lor \ell_1\lor\cdots\lor\ell_k), ]
where (\ell) is the only literal assigned at the current decision level. The solver computes the highest decision level among the assignments falsifying (\ell_1,\ldots,\ell_k). It then removes all trail assignments above that level. This operation is called nonchronological backtracking, or backjumping, because it may skip several intervening decisions that have no remaining relevance to the analyzed conflict.
After the backjump, every literal other than (\ell) in the learned clause is false, while (\ell) is unassigned. The learned clause therefore becomes unit and immediately propagates (\ell). Clauses with this property are described as asserting clauses. First-UIP analysis produces an asserting clause under the standard decision-level organization of CDCL.
Clause learning differs from recording an individual failed assignment. A learned clause blocks every future partial assignment that falsifies all of its literals, including assignments reached through a different sequence of decisions. It also becomes part of subsequent propagation and may participate in later conflict analyses. The search thus modifies its own deductive environment while preserving the set of satisfying assignments.
If analysis derives the empty clause at decision level zero, the original formula is unsatisfiable. If every variable becomes consistently assigned without producing a conflict, the resulting total assignment is a satisfying model.
Historical development
The logical basis of CDCL originates in the Davis–Putnam procedure and its search-oriented refinement by Martin Davis, George Logemann, and Donald Loveland. Their work established recursive case splitting combined with unit propagation as a general method for propositional satisfiability. Chronological DPLL search discards a failed branch and reverses the most recent unresolved decision, but it does not inherently retain an explanation of the failure.
The connection between failed search and reusable constraints developed through research on constraint satisfaction, automated deduction, and logic programming. Work on nogood recording and dependency-directed backtracking supplied general models for retaining combinations of assignments known to be inconsistent. In satisfiability solving, these ideas became clause learning because every recorded nogood could be represented directly as a clause.
During the 1990s, João Marques-Silva and Karem Sakallah presented the GRASP architecture, which integrated implication-graph analysis, clause recording, and nonchronological backtracking into a systematic SAT procedure. Robert Bayardo and Robert Schrag independently developed related methods in the rel_sat solver, including relevance-bounded learning and dynamic management of recorded constraints. These systems established the core operational structure later identified as conflict-driven clause learning.
The early-2000s Chaff solver, developed by Matthew Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, combined learning with watched literals and an activity-based decision heuristic. Subsequent solvers such as MiniSat reduced the architecture to a compact implementation model, while later systems refined clause management, restart scheduling, preprocessing, and inprocessing. The term CDCL consequently refers to a family of related solver designs rather than to a single fixed algorithm.
Branching and search adaptation
When propagation reaches a fixed point without producing either a conflict or a complete assignment, the solver selects an unassigned variable and assigns a provisional polarity. This branching decision determines which region of the remaining search space is explored next. The logical validity of CDCL does not depend on a particular decision heuristic, but the size and structure of the explored search tree depend strongly on the sequence of decisions.
The variable state independent decaying sum heuristic, known as VSIDS, increases the activity of variables appearing in recent conflicts and periodically reduces the relative influence of older activity. Its scores approximate the current concentration of unresolved interactions in the clause database. Variants maintain activities for variables, literals, or clauses, and many implementations preserve the most recently successful polarity when a variable is selected again.
Conflict information also influences clause retention. Learned clauses vary substantially in their future propagation behavior. A short clause directly constrains a small combination of assignments, but clause length alone does not determine usefulness. The literal block distance measure counts the distinct decision levels represented in a learned clause, thereby estimating how closely its literals were connected in the search that produced it.
Restarts and clause-database reduction
A restart removes most or all current assignments while retaining learned clauses and heuristic state. The solver then begins a new branching sequence over a formula strengthened by the consequences obtained before the restart. Restarts therefore differ from independent repetition because accumulated clauses alter propagation during every later search phase.
Restart schedules may be based on conflict counts or on statistics describing recent learned clauses and trail behavior. Frequent restarting limits the duration of an unproductive decision sequence, while the retained clause database preserves deductions made along that sequence. The interaction between restarts and activity-based branching often causes the solver to revisit related variables under a different ordering.
Unrestricted learning can produce more clauses than can be propagated efficiently. Clause-database reduction periodically removes learned clauses according to measures such as activity, size, or literal block distance. Clauses currently serving as reasons for active assignments are normally retained until those assignments leave the trail. Original clauses and learned unit clauses also receive distinct treatment because deleting them would either reconstruct existing input or discard globally forced assignments.
Deletion does not affect soundness because every learned clause is already entailed by the original formula. Removing one weakens only the solver's stored representation of previously derived consequences. Completeness remains compatible with deletion provided that the underlying branching and propagation process continues to explore unresolved assignments rather than permanently excluding them without logical justification.
Correctness and proof production
The soundness of clause learning follows from the resolution derivation used during conflict analysis. Every learned clause is a logical consequence of clauses already present in the database, and induction traces these consequences back to the original input formula. Consequently, learning cannot remove a satisfying assignment of the original formula.
For an unsatisfiable instance, a terminating CDCL run can be interpreted as constructing a resolution proof of the empty clause. Practical solvers commonly emit proof traces in formats such as DRAT or LRAT. An independent proof checker verifies that each added clause satisfies the format's admissibility conditions and that the trace eventually derives contradiction.
Proof logging separates the potentially complex search procedure from validation of its final result. The solver may use preprocessing, clause deletion, restarts, and specialized internal representations, while the checker verifies a comparatively narrow sequence of logical transformations. This division is significant in applications where an unsatisfiability result forms part of a larger formal or computational claim.
CDCL is complete for finite propositional formulas when its control policy does not indefinitely avoid unresolved portions of the assignment space. In the absence of deletion, only finitely many distinct non-tautological clauses exist over a fixed variable set, although that number is exponential. Practical completeness arguments account for restarts and clause removal through the fairness of decisions and the preservation of enough information to prevent endless repetition without progress.
Relationship to related solving frameworks
CDCL shares its central conflict-analysis mechanism with satisfiability modulo theories. In an SMT solver, Boolean propagation is supplemented by theory reasoning over domains such as arithmetic or arrays. A theory conflict is translated into a Boolean clause explaining which asserted literals are jointly inconsistent, after which ordinary CDCL analysis can derive a learned clause and a backjump level.
In answer set programming, conflict-driven nogood learning applies analogous operations to nogoods generated from logic-program semantics. The representation differs from a conventional CNF clause database, but propagation, implication analysis, and nonchronological backtracking retain closely corresponding roles.
Constraint-programming systems also use explanation-based propagation and learned nogoods. Their constraints may have richer domains than Boolean clauses, so explanations translate domain reductions into a form suitable for conflict analysis. These frameworks reflect the broader interpretation of CDCL as search augmented by explicit causal explanations of failure.