Classical Chronological Backtracking

See appendix for credits.

Chronological backtracking is an improvement for the DPLL algorithm backtracking. It can provide multiple jumps back to the assignment tree, while DPLL when there is a conflict, it simply flips the last assigned literal (thus one step).

The idea

There are two types of assignment, one is binary decision, the other is unit propagation, which is implied by the decisions. So when we reach a conflict, we jump back to the binary decision point, omitting all the implied assignment caused by that decision.

Implementation

Assignments are stored in a stack with tags: unit, open, closed. They respectively mean unit-propagation, first try (chances are still there, thus open), second try (no more chances on this literal). When a conflict is met, we pop the stack till the most recent open assignment and toggle it into closed, and continues the search.

Example

The background is a CNF SAT problem. The presented is part of its assignment tree. Red literals are already assigned. We make a binary decision (true) on $A_1$, leading the clauses $c_7$, $c_8$ be satisfied.

Fig. 1

As a consequence, $A_2, A_3, A_4, A_5, A_6$ are unit-propagated in order. But then $c_6$ would be false, reaching a conflict. Hence due to chronological backtracking idea, we remove all these new assignments since $A_1$, and push $\neg A_1$ to the stack.

Fig. 2

---

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.