Conflict-Driven Backtracking and Clause-Learning

See appendix for credits.

Conflict-Driven backtracking is a huge advancement to the classical chronological backtracking applied to the DPLL algorithm. It solves the Boolean formulas with about $10^7$ variables.

State of the art

The idea was to learn from error. When we see a conflict, we find the cause (building a conflict set), and we go back to the decision point where we could do it differently if we have had known this conflict set. It seems hard to catch for a machine. However, it is operable through the following algorithm. This is the most advanced modern approach in many SAT solvers.

Deciphering the myth

Data structure: stack partitioned into decision levels. Each level comprises of a decision literal and its implied literals (unit-propagated). Every implied literal is tagged with the clause causing its unit propagation (aka. antecedent clause).

One level in the stack can be depicted by an implication graph, where there are nodes and edges. A node without edges means a decision literal , because an edge is are marked with the antecedent clause of the literal. E.g.,

Fig. 1 An Implication Graph (Shown on Right)

Building the conflict set

It has two steps,

1. C := conflicting clause
2. repeat {
      C <- resolve C with the antecedent clause of the last
      unit-propagated literal in C
}
until { C verifies some termination criteria }

Well, we wonder what this "resolve" mean, it is a disjunction but removing $A_i \vee \neg A_i$ since they become true. Resolution is a rule saying two input clauses entails the output clause (aka. resolvent). For a detailed discussion, see Resolution (logic). By performing this, the unit propagation is undone. What about some termination criteria? Here comes the magic.

1st UIP

It means First Unique Implication Point, this is the state-of-the-art strategy. It is the first point where we find only one literal of current decision level in C. For instance (built from the same example above),

Fig. 2 Conflict set construction

Upon this, we build the conflict set: $\{ \neg A_{10} , \neg A_{11} , A_4 \}$, and "learn" (add) a new clause $c_{10} := A_{10} ∨ A_{11} ∨ \neg A_4$. Now that we reached the conflict, also we know these $\neg A_{10}$, $\neg A_{11}$ can not survive with $A_4$, so we backtrack to $\neg A_{11}$, and right there we assign $\neg A_4$. Yes, we cut off all paths to $A_4$ from that point on. We would never fall into this conflict set again (we learned from the error).

Drawbacks and a solution

We saved all these learned clauses, on a larger scale ($10^7+$), we can reach an exhaustion of space. The solution is to keep only the active ones, i.e. the ones showed up (on the edges of implication graph) in the current decision level.

Fig. 3 The breath-taking jump

---

Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.