CDCL

CDCL stands for Conflict-Driven Clause Learning, a refinement of the DPLL procedure used in modern SAT solvers. It is designed to efficiently determine propositional satisfiability by not only searching assignments but also learning from conflicts to prune the search space.

In CDCL, the solver alternates between decision steps and unit propagation. When a conflict occurs, meaning a clause has all its literals false under the current assignment, the solver analyzes the conflict using the implication graph to derive a new clause, the learned clause. This clause is added to the formula to prevent the same conflicting combination of assignments from reoccurring. The solver then backtracks non-chronologically to a prior decision level, called the assertion level, where the learned clause becomes unit and triggers further propagation. This non-chronological backtracking, or backjumping, is a key feature that speeds up search by skipping irrelevant portions of the search tree.

A common learning scheme is the first Unique Implication Point (UIP) approach, which aims to produce compact, effective learned clauses. CDCL solvers also rely on heuristics to choose the next decision variable, with activity-based schemes like VSIDS being widely used, and on restart strategies and clause database management to balance learning and memory use.

Impact and scope: CDCL is the dominant paradigm behind most practical SAT solvers, enabling efficient handling of large and complex instances from hardware and software verification to planning and scheduling. It has influenced extensions to Satisfiability Modulo Theories and continues to be an active area of research in solver design and heuristics.