CDCL

CDCL (Conflict-Driven Clause Learning) is the dominant algorithmic paradigm for solving the Boolean satisfiability problem (SAT). It is not merely an improvement over earlier DPLL-based search; it is a fundamentally different computational architecture that treats the search process as a theory-building exercise rather than a trial-and-error exploration. The core insight is that every conflict encountered during search is an opportunity to learn a new clause — a constraint that prevents the same conflicting combination from being explored again — and the accumulation of these learned clauses progressively refines the solver's understanding of the formula's structure.

The CDCL loop consists of four phases: propagation, decision, conflict analysis, and backtracking. During propagation, the solver deduces forced assignments from unit clauses. During decision, it chooses a variable to assign when no more propagations are possible. When a conflict is detected, the solver analyzes the conflict graph to derive a learned clause and a backtracking level, then returns to propagation. The decision heuristic (typically VSIDS, Variable State Independent Decaying Sum) prioritizes variables that appear in recent conflicts, which means the solver's attention is dynamically directed toward the most active regions of the formula. This is not a fixed search strategy; it is an emergent search strategy that adapts to the formula's structure during the search itself.

CDCL is the computational equivalent of a scientist who learns from failed experiments. Each conflict generates a new hypothesis about what cannot be true, and the solver's performance improves not despite its failures but because of them. The fact that CDCL solvers routinely handle millions of variables despite SAT being NP-complete is not a refutation of complexity theory. It is a demonstration that adaptive systems can exploit structural regularities that worst-case analysis ignores.