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. The main difference between CDCL and DPLL is that CDCL's backjumping is non-chronological.

Conflict-driven clause learning was proposed by Marques-Silva and Karem A. Sakallah (1996, 1999)[1][2] and Bayardo and Schrag (1997).[3]

Background edit

Boolean satisfiability problem edit

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   and   are clauses.

A satisfying assignment for this formula is e.g.:


since it makes the first clause true (since   is true) as well as the second one (since   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   possibilities. 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.

Unit clause rule (unit propagation) edit

If an unsatisfied 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 the below unsatisfied clause is evaluated with   and   we must have   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).

Resolution edit

Consider two clauses   and  . The clause  , obtained by merging the two clauses and removing both   and  , is called the resolvent of the two clauses.

Algorithm edit

Conflict-driven clause learning works as follows.

  1. Select a variable and assign True or False. This is called decision state. Remember the assignment.
  2. Apply Boolean constraint propagation (unit propagation).
  3. Build the implication graph.
  4. If there is any conflict
    1. Find the cut in the implication graph that led to the conflict
    2. Derive a new clause which is the negation of the assignments that led to the conflict
    3. Non-chronologically backtrack ("back jump") to the appropriate decision level, where the first-assigned variable involved in the conflict was assigned
  5. Otherwise continue from step 1 until all variable values are assigned.

Example edit

A visual example of CDCL algorithm:[4]

Completeness edit

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 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.[5]

Applications edit

The main application of CDCL algorithm is in different SAT solvers including:

  • MiniSAT
  • Zchaff SAT
  • Z3
  • Glucose[6]
  • ManySAT etc.

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 edit

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.[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.

Works cited edit

  1. ^ J.P. Marques-Silva; Karem A. Sakallah (November 1996). "GRASP-A New Search Algorithm for Satisfiability". Digest of IEEE International Conference on Computer-Aided Design (ICCAD). pp. 220–227. CiteSeerX doi:10.1109/ICCAD.1996.569607. ISBN 978-0-8186-7597-3.
  2. ^ J.P. Marques-Silva; Karem A. Sakallah (May 1999). "GRASP: A Search Algorithm for Propositional Satisfiability" (PDF). IEEE Transactions on Computers. 48 (5): 506–521. doi:10.1109/12.769433. Archived from the original (PDF) on 2016-03-04. Retrieved 2014-11-29.
  3. ^ Roberto J. Bayardo Jr.; Robert C. Schrag (1997). "Using CSP look-back techniques to solve real world SAT instances" (PDF). Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI). pp. 203–208.
  4. ^ a b In the pictures below, " " is used to denote "or", multiplication to denote "and", and a postfix " " to denote "not".
  5. ^ Biere, Heule, Van Maaren, Walsh (February 2009). Handbook of Satisfiability (PDF). IOS Press. p. 138. ISBN 978-1-60750-376-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
  6. ^ "Glucose's home page".

References edit