Course:CPSC522/ConflictDriven Clause Learning for the Boolean Satisfiability Problem
ConflictDriven Clause Learning for the Boolean Satisfiability Problem
We discuss the development of conflictdriven clause learning (CDCL) in the context of the DavisPutnamLogemannLoveland (DPLL) algorithm for SAT solving.
Principal Author: Carl Kwan
Abstract
Boolean satisfiability (SAT) was the first decision problem to be proven complete. Despite lack of a known tractable algorithm, many practical problems throughout automated reasoning are solved via reduction to SAT. Most modern SAT solvers instead implement some procedure based on the DavisPutnamLogemannLoveland (DPLL) algorithm. In particular, the inspired conflictdriven clause learning (CDCL) algorithm has found explicit success in the SAT solving community and applications.
In this article, we discuss the seminal paper “A Machine Program for TheoremProving” which introduces the DPLL algorithm and the more recent paper “Using CSP LookBack Techniques to Solve RealWorld SAT Instances” which introduces CDCL  the improved sequal to DPLL.
Builds On
It is assumed that the reader is familiar with predicate calculus and possesses some background in the theory of computation. Mathematical maturity is also beneficial but not imperative.
Related Pages
SAT solvers have a large role to play in logic programming and its subparadigms where the satisfiability of conjunctions of constraints is an important question. AI planning and scheduling were among the first successful applications of SAT solvers.^{[1]} Outside of AI, applications of SAT solving include circuit design, model checking, automatic testpattern generation, bioinformatics, and theorem proving.
Content
SAT
Consider a formula over a Boolean algebra, say,
or
It is clear that the former formula will always evaluate to false independently of the truth assignments of . But what about the latter formula? Does it have an assignment such that it will evaluate to true? This is the Boolean satisfiability problem.
Definition (SAT). Given a formula over a Boolean algebra, is there a truth assignment such that it is satisfied?
Occasionally, a restriction is made that the provided formula is in conjunctive normal form (CNF), ie. the form
where each is a literal. We say a formula is in CNF if it is CNF and each clause has literals. SAT is sometimes posed as the equivalent 3SAT problem.
Definition (3SAT). Given a formula over a Boolean algebra in 3CNF, is there an assignment such that such that is satisfied?
Note that 3SAT is already an instance of SAT and it is a common excercise to show SAT can be reduced to 3SAT.^{[2]}
In the early 1970’s, Stephen Cook and Leonid Levin both independently discovered and proved SAT was complete.^{[3]}^{[4]} However, notions of satisfiablity date back to Aristotle’s discovery of logic^{[5]} and, since then, heuristics have been developed to combat the problem. A particular successful (and more recent) algorithm is the namesake of its pioneers: Martin Davis, Hilary Putnam, George Logemann, and Donald W. Loveland.
DPLL
In 1960, Davis and Putnam published a algorithm for SAT which was refined two years later by Davis along with Logemann and Loveland.^{[6]}^{[7]} The original motivations of Davis et al. for the two papers is towards an automated theorem prover for quantification theory. Moreover, the majority of the DPLL algorithm (the portion occasionally referred to as the DP algorithm) is already set out in "A Computing Procedure for Quantification Theory" and, instead, "A Machine Program for Theorem Proving" serves as a (much shorter) discussion regarding the programming implementation of DP. However, the later paper is sufficiently significant for its modifications  especially its spacesaving techniques  that it would prove unbecoming to not discuss it in this article. Thus we primarily reference the second paper for the purposes of this article.
"A Machine Program for Theorem Proving" begins with a pointer to the original DP algorithm and then proceeds to discuss storage techniques for their implementation. The paper also introduces the notion of deleting literals and eliminating clauses. Finally, it concludes with some comments on results pertaining to feasibility and spaceefficiency.
For pedagogical purposes, we begin by introducing a potential approach to SAT with a quick and simple example. Then we discuss the DPLL algorithm along with the refinements of the second paper. Lastly, we consider the results and performance of DPLL as outlined in the paper in its historical context.
Naïve Approach
From here on, we suppose any formula is provided in CNF.
First, it will prove enlightening to consider a naïve approach to SAT, ie. simply assign variables with arbitrary truth values until a satisfying assignment is found or if there are no other cases. Visually, this can be represented with a tree. For example, suppose the formula of interest is
in which case, this process can be viewed as so:
Here, the box denotes an unsatisfactory assignment (unsat) and the empty clause denotes a satisfactory assignment (sat). In the example, the initial choice of was a poor one in that the path to the solution is the longest possible. It is clear that the naïve approach has exponential time complexity. While DPLL remains exponential, there remains small rules to improve performance.
Unit Propagation
There are some very obvious immediate improvements that can be made. For example, if an atom and its negation both appear as oneliteral clauses, then the formula is immediately unsat, ie.
Now suppose an atom appears as a oneliteral clause. Then that atom must be assigned true and any clause containing it is immediately satisfied. However, any negation of the atom will be false. In particular, we may ignore any clauses containing the atom and any instance of the negation of the atom will otherwise have no bearing on the satisfiability of the formula. For example,
The same applies if a negation of an atom appears as a oneliteral clause. A oneliteral clause is also called a unit. The process of eliminating the clauses containing the atom (or its negation) and instances of the negation (or its atom, respectively) is called unit propagation.
Algorithm UnitPropagation
1 # Given a formula f in CNF, return one of: a) another formula, b) unsat, c) sat. 2 UnitPropagation (f) 3 if a literal and its negation both appear as oneliteral clauses, then return unsat 4 if a literal appears as a oneliteral clause, then eliminate every clause containing the literal and delete every instance of its negation 5 if f is the empty clause (ie. f == {}), then return sat 6 return f
Pure Literals
Now suppose instead of as an oneliteral clause, an atom appears in arbitrary clauses but only as a nonnegated literal. Observe the following example
If , then the formula only depends on those clauses not containing . In fact, we have
It is a simple exercise that the above equivalence holds for arbitrary formulas. Moreover, the same can be said for a literal that only appears in negated form throughout the formula except we asign the atom to false. If a literal only appears in either its affermitive form or negated form throughout a formula, then it is a pure literal.
Algorithm PureLiterals
1 # Given a formula f in CNF, return another formula or sat 2 PureLiterals (f) 3 if a pure literal exists, then delete every clause containing it 4 if f == {}, then return sat 5 return f
Full Implementation
Putting the above together, we get DPLL:
Algorithm DPLL
1 # Given a formula f in CNF, return sat or unsat 2 DPLL (f) 3 UnitPropagation(f) 4 PureLiterals(f) 5 pick a branching variable a # take, say, the first variable of the shortest clause 6 return DPLL (f and a) or DPLL (f and not a)
It should be noted that the original paper recursed on formulas with factored out and as oneliteral clauses but this is equivalent to step 6 anyways since and already have those oneliteral clauses.
Performance
The earliest introduction of the asymptotic computational complexity theory with which we are familiar today wasn't published until 1965  3 years after our paper of interest.^{[9]} Even notions of completeness were only first seen in the 1970's. The original discussion by Davis et al., consequently, focuses primarily on spacesaving techniques and results for the machine on which they programmed DPLL  the IBM 704. The IBM 704, understandably, is limited in terms of computational resources when compared to the machines of late. However, Davis et al. show, via a combinatorical argument, that their method is at least 100 times more space efficient than any previous attempt. Indeed, considering also that the previous upper bound was in the order of 10's of lines, the improvement is quite impressive  especially when taking into account the scaling that would occur as computational machines improved resourcewise.
CDCL
The DPLL algorithm forms the basis of many modern and successful SAT solving techniques among which is CDCL. The notion of conflictdriven clause learning for SAT was developed in the late 1990's by a series of papers.^{[10]}^{[11]}^{[12]} In this article, we cite “Using CSP LookBack Techniques to Solve RealWorld SAT Instances” by Roberto J. Bayardo Jr. and Robert C. Schrag as it pertains to applications thematically relavent to this course.
The motivations of Bayardo Jr. et al. were in stark contrast to those of Davis et al. By this time in history, the SAT solving scene has began to explode and SMT solvers were also taking shape.^{[13]} Technically, SAT and SMT can be considered special instances of constraint satisfaction problems (CSPs) which included a breadth of applications far greater than the certification of proofs as Davis et al. had intended.^{[5]} Boyardo Jr. et al. begins similarly to Davis et al. by introducing the DP algorithm for SAT albeit framed from a CSP perspective. After describing CDCL, however, the performance of the algorithm is evaluated on test suites pertaining to more pragmatic pursuits such as planning, circuit diagnosis, and scheduling instances as opposed to the classical theorems put forth by Davis et al.
As a whole, however, CDCL is very similar to DPLL with two main exceptions. We discuss these two exceptions as well as the performance of CDCL.
Backjumping
Consider again visualizing the process of DPLL on some formula, say,
in the form of a tree and suppose it has
Now, within UnitPropagation
, CDCL instead maintains a pointer to the clause as the reason an assignment is excluded. For example, in the above, if and is assigned, then the reason we exclude is because of the pointer to . However, eventually, we will need to exclude as well because of the reason and we obtain a contradiction. In this case we resolve the two reasons, and obtain the working reason . But is also excluded for the reason . In this case, we immediately backjump to the assignment of .
Learning
Recall the previous example. Learning in CDCL is very simple: since assigning would lead to unsat, we simply conjunct the formula with the oneliteral thus ensuring the exclusion of that “branch” of the search. Explicitly, we obtain
In the case that there are other clauses in the formula, say,
the inclusion of as a oneliteral clause will ensure its proper truth assignment and save the time spent in the wrong part of the search tree.
Performance
Since SAT remains complete at the moment, any increases in performance that CDCL has over other implementations are unfortunately purely experimental. However, implementations with varying extents of backjumping and learning implemented saw significant increases in performance over simple DPLL implementations and some other thenmodern implementations. The complexity of solving makes it necessary for hard cutoff times in the execution of the solver which upon reaching will result in failure. Under certain standardized test suites, simple DPLL implementations saw a 100% failure rate whereas CDCL implementations saw a 0% failure rate. Test suites were taken from a variety of sources to include planning, circuit diagnosis and synthesis, and scheduling instances.
The figure (right) contains an overview of CDCL on some of the test suites.
Bayardo Jr. et al. implemented four solvers based on DPLL and CDCL in C++. In the figure, naivesat is the DPLL implementation without backjumping or learning; cbjsat is DPLL with backjumping but without learning; sizesat is CDCL (ie. backjumping and learning) but only reasons with a bounded number of variables are retained; relsat is CDCL but only reasons with an upper bound on the number of variables with changed assignments since the reason was derived are retained.
For example, sizesat(2) would retain reasons such as and since these clauses have at most 2 variables. However, it will not retain reasons such as .
On the other hand, relsat(2) will retain reasons such as as long as remains assigned to its original assignment (assuming that , , and were assigned in the order they appear) because a reassignment of would mean that both and have already been reassigned prior. The reassignment of would then be the third change in assignment since the reason was derived and so then the reason is discarded.
Conclusion
The official justification behind the research in "A Computing Procedure for Quantification Theory" and "A Machine Program for Theorem Proving" was the goal of automatically proving novel theorems mechanically. However, Davis later revealed that, together with Putnam, their primary motivation was for DPLL to be a source of funding for their work towards a more foundational and theoretical question in computability theory.^{[5]} It was unknown at the time that DPLL would lead to such widespread application. In the conclusion to their paper, Bayardo Jr. et al. cites not only planning, scheduling, circuit processing as systems in which DPLL appears, but also in more recent developments such as higherorder theorem provers or larger hybrid algorithms. Indeed, SAT solving techniques has inspired the closely related but more expressive SMT solvers which, loosely stated, combines SAT with firstorder theories (eg. integer arithmetic, arrays, etc.). Moreover, DPLL has recently been further abstractified for the sake of compatibility with satisfiability modulo theories with the aim of theorem proving in mind.^{[14]}
On the other hand, the constant appearance of DPLL in contemporary systems, in a less positive light, suggests the lack of asymptotic improvements in the area.
Despite the improved experimental performance in practice,
it should be noted that CDCL is not significantly different from DPLL in that much of the original structure is maintained in the new algorithm.
Progress usually attacks one of three places in the DPLL algorithm.
Either novel techniques in backtracking are considered in the UnitPropagation
section or different policies for choosing the branching variable are created or different data structures for storing the formula and clauses are introduced.
CDCL falls into the first category.
The lack of an asymptotic speedup for SAT since the 1960's is a testament to its complexity; the ubiquitous nature of SAT in not only automated reasoning but also theoretical computer science is a testament to its utility. It is wholly possible that, even if the event is realized, the search for more efficient procedures for SAT  experimental or otherwise  will continue.
Annotated Bibliography
 ↑ MarquesSilva, Joao (2008) Practical Applications of Boolean Satisfiability At Workshop on Discrete Event Systems (WODES'08), Sweden
 ↑ Michael Sipser. 1996. Introduction to the Theory of Computation: Preliminary Edition (1st ed.). PWS Pub. Co., Boston, MA, USA.
 ↑ Levin, Leonid (1973). "Универсальные задачи перебора,". Problems of Information Transmission (in Russian). 9 (3): 115–116.
 ↑ Cook, Stephen (1971). "The complexity of theorem proving procedures". Proceedings of the Third Annual ACM Symposium on Theory of Computing. pp. 151–158. doi:10.1145/800157.805047
 ↑ ^{5.0} ^{5.1} ^{5.2} A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands.
 ↑ Davis, Martin; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201–215. doi:10.1145/321033.321034.
 ↑ Davis, Martin; Logemann, George; Loveland, Donald (1962). "A Machine Program for Theorem Proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557.
 ↑ https://en.wikipedia.org/wiki/File:IBM_Electronic_Data_Processing_Machine__GPN2000001881.jpg
 ↑ Hartmanis, J.; Stearns, R. E. "On the computational complexity of algorithms". Trans. Amer. Math. Soc. 117 1965 285–306.
 ↑ J. P. Marques Silva and K. A. Sakallah, "GRASPA new search algorithm for satisfiability," Proceedings of International Conference on Computer Aided Design, San Jose, CA, USA, 1996, pp. 220227. doi: 10.1109/ICCAD.1996.569607
 ↑ ^{11.0} ^{11.1} Roberto J. Bayardo Jr.; Robert C. Schrag (1997). "Using CSP lookback techniques to solve real world SAT instances". Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI). pp. 203–208.
 ↑ J. P. MarquesSilva and K. A. Sakallah, "GRASP: a search algorithm for propositional satisfiability," in IEEE Transactions on Computers, vol. 48, no. 5, pp. 506521, May 1999. doi: 10.1109/12.769433
 ↑ ^{13.0} ^{13.1} https://github.com/enzet/symbolicexecution/blob/master/diagram
 ↑ Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004), "Abstract DPLL and Abstract DPLL Modulo Theories", Proceedings Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, pp. 36–50
To Add
Formatting, Images, Diagrams, Sources
