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.

Conflict-Driven Clause Learning was proposed by Marques-Silva and Sakallah (1996,^[1] 1999 ^[2]) and Bayardo and Schrag (1997 ^[3])

Background

Background knowledge about the following issues is needed to have a clear idea about the CDCL algorithm.

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:

$(A' + C') (B + C)$

where A,B,C are Boolean variables, $A'$, $C'$, $B$, and $C$ are literals, and $A' + C'$ and $B + C$ are clauses.

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

$A = False, B = False , C = True$

since it makes the first clause true (since $A'$ is true) as well as the second one (since $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$ 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 appilcations 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)

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 $A = False$ and $B = False$ we must have $C = True$ in order for the clause $(A \or B \or C )$ to be true.

Boolean constraint propagation (BCP)

The iterated application of the unit clause rule is referred to as unit propagation or Boolean constraint propagation (BCP).

Resolution

Consider two clauses $(A \or B \or C )$ and $(\neg C \or D \or \neg E)$. The clause $(A \or B \lor D \lor \neg E)$, obtained by merging the two clauses and removing both $\neg C$ and $C$, is called the resolvent of the two clauses.

DP algorithm

The DP algorithm has been introduced by Davis and Putnam in 1960. Informally, the algorithm iteratively performs the following steps until no more variables are left in the formula:

• Select a variable $A$ and add all non-tautological resolvents upon $A$ (a resolvent is non-tautological if it does not contain $V$ and $\neg V$ for some variable $V$).
• Remove all original clauses that contain $A$.

See more details here DP Algorithm

DPLL algorithm

Davis, Putnam, Logemann, Loveland (1962) had developed this algorithm. Some properties of this algorithms are:

• It is based on search.
• It is the basis for almost all modern SAT solvers.
• It uses learning and chronological back tracking (1996).

See more details here DPLL algorithm. An example with visualization of DPLL algorithm having chronological back tracking:

• 

  All clauses making a CNF formula

• 

  Pick a variable

• 

  Make a decision, variable a = False (0), thus green clauses becomes True

• 

  After 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 variable

• 

  But force decision still lead to another conflict

• 

  Backtrack to previous level and make a force decision

• 

  Make a new decision, but it lead to a conflict

• 

  Make a forced decision, but again it lead to a conflict

• 

  Backtrack to previous level

• 

  Continue in this way and the final implication graph

CDCL (Conflict-Driven Clause Learning)

The main difference between CDCL and DPLL is that CDCL's back jumping is non-chronological.

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 then analyze the conflict and non-chronologically backtrack ("back jump") to the appropriate decision level.
5. Otherwise continue from step 1 until all variable values are assigned.

Example

A visual example of CDCL algorithm:

• 

  At first pick a branching variable, viz. 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 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.

• 

  Back jump and set variable values accordingly.

Completeness

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 does not affect soundness or 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.^[4]

Applications

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

• MiniSAT
• Zchaff SAT
• Z3
• 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

Related algorithms to CDCL are the DP and DPLL algorithm described before. The DP algorithm uses resolution refutation and it has potential memory access problem. 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.

• 

  DPLL: no learning and chronological backtracking.

• 

  CDCL: conflict-driven clause learning and non - chronological backtracking.

References

• Martin Davis and Hilary Putnam (1960). "A Computing Procedure for Quantification Theory". J.ACM 7 (3): 201—215. doi:10.1145/321033.321034.
• Martin Davis and George Logemann and Donald Loveland (Jul 1962). "A machine program for theorem-proving". CACM 5 (7): 394—397. doi:10.1145/368273.368557.
• Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik (2001). "Chaff: engineering an efficient SAT solver" (PDF). Proc. 38th Ann. Design Automation Conference (DAC). pp. 530—535.
• Lintao Zhang and Conor F. Madigan and Matthew H. Moskewicz and Sharad Malik (2001). "Efficient conflict driven learning in a boolean satisfiability solver" (PDF). Proc. IEEE/ACM Int. Conf. on Computer-aided design (ICCAD). pp. 279—285.
• Presentation – "SAT-Solving: From Davis-Putnam to Zchaff and Beyond" by Lintao Zhang. (Several pictures are taken from his presentation)

1. J.P. Marques-Silva and 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.
2. J.P. Marques-Silva and 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.
3. Roberto J. Bayardo Jr. and 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. Biere, Heule, Van Maaren, Walsh (February 2009). Handbook of Satisfiability (PDF). IOS Press. p. 138. ISBN 978-1-60750-376-7.

Other material

Besides CDCL there are other approaches which are used to speed up SAT solvers. Some of them are:

• Restart
• Watched literal
• Failed literal
• Stochastic search