Conflict-Driven Clause Learning

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.All clauses making a CNF formulaPick a variableMake a decision, variable a = False (0), thus green clauses becomes TrueAfter several decision making, we find an implication graph that leads to a conflict.Now backtrack to immediate level and by force assign opposite value to that variableBut a forced decision still leads to another conflictBacktrack to previous level and make a forced decisionMake a new decision, but it leads to a conflictMake a forced decision, but again it leads to a conflictBacktrack to previous levelContinue in this way and the final implication graphAt first pick a branching variable, namely x1. A yellow circle means an arbitrary decision.Now apply unit propagation, which yields that x4 must be 1 (i.e. True). A gray circle means a forced variable assignment during unit propagation. The resulting graph is called an implication graph.Arbitrarily pick another branching variable, x3.Apply unit propagation and find the new implication graph.Here the variable x8 and x12 are forced to be 0 and 1, respectively.Pick another branching variable, x2.Find implication graph.Pick another branching variable, x7.Find implication graph.Found a conflict!Find the cut that led to this conflict. From the cut, find a conflicting condition.Take the negation of this condition and make it a clause.Add the conflict clause to the problem.Non-chronological back jump to appropriate decision level, which in this case is the second highest decision level of the literals in the learned clause.Back jump and set variable values accordingly.DPLL: no learning and chronological backtracking.CDCL: conflict-driven clause learning and non – chronological backtracking. 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) and Bayardo and Schrag (1997).