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.
Conflict-driven clause learning was proposed by Marques-Silva and Karem A. Sakallah (1996, 1999)[1][2] and Bayardo and Schrag (1997).
[3] 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: or, using a common notation:[4] where A,B,C are Boolean variables,
A satisfying assignment for this formula is e.g.: since it makes the first clause true (since
This examples uses three variables (A, B, C), and there are two possible assignments (True and False) for each of them.
In this small example, one can use brute-force search to try all possible assignments and check if they satisfy the formula.
But in realistic applications with millions of variables and clauses brute force search is impractical.
The responsibility of a SAT solver is to find a satisfying assignment efficiently and quickly by applying different heuristics for complex CNF formulas.
If a clause has all but one of its literals or variables evaluated at False, then the free literal must be True in order for the clause to be True.
The iterated application of the unit clause rule is referred to as unit propagation or Boolean constraint propagation (BCP).
A sequent calculus-similar notation can be used to formalize many rewriting algorithms, including CDCL.
The following are the rules a CDCL solver can apply in order to either find or fail or find a satisfying assignment, i.e.
This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.
This rule represents detecting a conflict when all literals in a clause are assigned to false under the current assignment.
This rule performs a non-chronological backtracking by jumping back to a decision level implied by the conflict clause and asserting the negation of the literal that caused the conflict at a lower decision level.
This rule represents the clause learning mechanism of CDCL solvers, where conflict clauses are added back to the clause database to prevent the solver from making the same mistake again in other branches of the search tree.
These 6 rules are sufficient for basic CDCL, but modern SAT solver implementations also usually add additional heuristic-controlled rules in order to be more efficient at traversing the search space and solve SAT problems faster.
Forget Learned clauses can be removed from the formula
This rule represents the restart mechanism, which allows the solver to jump out of a potentially unproductive search space and start over, often guided by the learned clauses.
Note, learned clauses are still remembered through restarts, ensuring termination of the algorithm.
CDCL SAT solvers implement DPLL, but can learn new clauses and backtrack non-chronologically.
Clause learning with conflict analysis affects neither soundness nor completeness.
Conflict analysis identifies new clauses using the resolution operation.
Moreover, the modified backtracking step also does not affect soundness or completeness, since backtracking information is obtained from each new learnt clause.
[5] The main application of CDCL algorithm is in different SAT solvers including: The CDCL algorithm has made SAT solvers so powerful that they are being used effectively in several[citation needed] real world application areas like AI planning, bioinformatics, software test pattern generation, software package dependencies, hardware and software model checking, and cryptography.
The DP algorithm uses resolution refutation and it has potential memory access problem.
[citation needed] Whereas the DPLL algorithm is OK for randomly generated instances, it is bad for instances generated in practical applications.
CDCL is a more powerful approach to solve such problems in that applying CDCL provides less state space search in comparison to DPLL.