In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to true. The internal workings of CDCL SAT solvers were inspired by DPLL solvers.
Conflict-driven clause learning was proposed by Marques-Silva and Sakallah (1996, 1999)[1][2] and Bayardo and Schrag (1997).[3]
Background knowledge about the following issues is needed to have a clear idea about the CDCL algorithm.
Main article: Boolean satisfiability problem
The satisfiability problem consists in finding a satisfying assignment for a given formula in conjunctive normal form (CNF).
An example of such a formula is:
( (not A) or (not C) ) and (B or C),
or, using a common notation:[4]
where A,B,C are Boolean variables,
,
,
, and
are literals, and