Clause Learning

Clause learning is the mechanism by which modern SAT solvers transform failure into knowledge. When a conflict is detected during search — a contradiction that proves the current partial assignment cannot be extended to a satisfying solution — the solver analyzes the conflict graph to derive a new clause that explains why the failure occurred. This learned clause is added to the formula, preventing the same conflicting combination from being explored again. The process is not merely a caching optimization; it is an emergent theory-building mechanism in which the solver constructs an increasingly refined description of the formula's unsatisfiable regions through direct experience with them.

The clause learned from a conflict is always a logical consequence of the original formula, which means clause learning preserves soundness while expanding the solver's strategic options. Over the course of a search, a solver may learn thousands or millions of clauses, many of which are far more powerful than the original constraints. The learned clause database becomes a kind of negative image of the solution space — a compressed representation of what does not work. This is why clause learning is the decisive innovation that separates modern CDCL solvers from earlier DPLL-based systems: it converts search into a process of cumulative refinement rather than blind trial and error.

Clause learning is the computational equivalent of scientific induction: each failed experiment generates a new constraint on future hypotheses, and the accumulation of those constraints is what makes progress possible.