SAT solving
Conflict-driven clause learning
Abbreviated CDCL
A SAT search method that learns clauses from conflicts.
Definition
Conflict-driven clause learning
Conflict-driven clause learning (CDCL) combines Boolean propagation, chosen assignments, conflict analysis, backtracking, and learned clauses.
When a partial assignment makes a clause false, the solver analyzes the reasons for that conflict. It learns a clause that prevents the same failing combination from returning.
01
Example
If choosing a = true forces b and not b, conflict analysis can learn that a must be false under the current constraints.
02
Important distinction
A learned clause must follow from the existing formula. Adding an unjustified clause can turn a sat problem into an unsat one.
After reading this article, you should be able to
- Define CDCL in the sense used on this site.
- Trace propagation, conflict, learning, and backtracking in a small SAT search.