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 . The main difference between CDCL and DPLL is that CDCL's backjumping is non-chronological.
10-852: Conflict-driven clause learning was proposed by Marques-Silva and Karem A. Sakallah (1996, 1999) and Bayardo and Schrag (1997). 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: where A , B , C are Boolean variables, ¬ A {\displaystyle \lnot A} , ¬ C {\displaystyle \lnot C} , B {\displaystyle B} , and C {\displaystyle C} are literals, and ¬ A ∨ ¬ C {\displaystyle \lnot A\lor \lnot C} and B ∨ C {\displaystyle B\lor C} are clauses. A satisfying assignment for this formula
20-560: Is e.g.: since it makes the first clause true (since ¬ A {\displaystyle \lnot A} is true) as well as the second one (since C {\displaystyle C} is true). This examples uses three variables ( A , B , C ), and there are two possible assignments (True and False) for each of them. So one has 2 3 = 8 {\displaystyle 2^{3}=8} possibilities. In this small example, one can use brute-force search to try all possible assignments and check if they satisfy
30-558: Is in different SAT solvers including: The CDCL algorithm has made SAT solvers so powerful that they are being used effectively in several real world application areas like AI planning, bioinformatics, software test pattern generation, software package dependencies, hardware and software model checking, and cryptography. Related algorithms to CDCL are the Davis–Putnam algorithm and DPLL algorithm . The DP algorithm uses resolution refutation and it has potential memory access problem. Whereas
40-542: The Graph automorphism problem. He was elevated to the rank of IEEE Fellow in 1998. In 2009, he shared the CAV ( Computer Aided Verification ) award with eight other individuals "for major advances in creating high-performance Boolean satisfiability solvers." In 2012, Sakallah became an ACM Fellow "for algorithms for Boolean Satisfiability that advanced the state-of-the-art of hardware verification." In 2014, Sakallah help shape
50-574: 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. Karem A. Sakallah Karem Sakallah is an American electrical engineer and computer scientist, a professor at University of Michigan known for his work on computational logic , functional verification , SAT solvers , satisfiability modulo theories , and
60-520: The below unsatisfied clause is evaluated with A = F a l s e {\displaystyle A=\mathrm {False} } and B = F a l s e {\displaystyle B=\mathrm {False} } we must have C = T r u e {\displaystyle C=\mathrm {True} } in order for the clause ( A ∨ B ∨ C ) {\displaystyle (A\lor B\lor C)} to be true. The iterated application of
70-435: 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. For example, if
80-458: The resolution operation. Therefore, each learnt clause can be inferred from the original clauses and other learnt clauses by a sequence of resolution steps. If cN is the new learnt clause, then ϕ is satisfiable if and only if ϕ ∪ {cN} is also satisfiable. Moreover, the modified backtracking step also does not affect soundness or completeness, since backtracking information is obtained from each new learnt clause. The main application of CDCL algorithm
90-556: The two clauses and removing both ¬ C {\displaystyle \neg C} and C {\displaystyle C} , is called the resolvent of the two clauses. Conflict-driven clause learning works as follows. A visual example of CDCL algorithm: DPLL is a sound and complete algorithm for SAT. 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
100-552: The unit clause rule is referred to as unit propagation or Boolean constraint propagation (BCP). Consider two clauses ( A ∨ B ∨ C ) {\displaystyle (A\lor B\lor C)} and ( ¬ C ∨ D ∨ ¬ E ) {\displaystyle (\neg C\lor D\lor \neg E)} . The clause ( A ∨ B ∨ D ∨ ¬ E ) {\displaystyle (A\lor B\lor D\lor \neg E)} , obtained by merging
#49950