Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lazy Reimplication in Chronological Backtracking

Robin Coutelier, Mathias Fleury, Laura Kovács

TL;DR

A lazy reimplication procedure for missed lower implications in chronological backtracking by reimplying literals on demand, rather than eagerly, that can be replicated in other solvers, as shown by the results in the solvers CaDiCaL and Glucose.

Abstract

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.

Lazy Reimplication in Chronological Backtracking

TL;DR

A lazy reimplication procedure for missed lower implications in chronological backtracking by reimplying literals on demand, rather than eagerly, that can be replicated in other solvers, as shown by the results in the solvers CaDiCaL and Glucose.

Abstract

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.
Paper Structure (25 sections, 5 theorems, 5 equations, 7 figures, 2 tables, 4 algorithms)

This paper contains 25 sections, 5 theorems, 5 equations, 7 figures, 2 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Related work.
  3. Our contributions.
  4. Preliminaries
  5. Invariant Properties on CDCL Variants
  6. CDCL Invariants on Implications
  7. Chronological Backtracking
  8. Weak chronological backtracking (WCB).
  9. Restoration.
  10. Prophylaxis.
  11. Adapting CDCL with Lazy Reimplications
  12. Our solution: Lazy reimplication in CDCL.
  13. Lazy reimplication for strong chronological backtracking -- LSCB.
  14. Propagation in LSCB.
  15. Backtracking in LSCB.
  16. ...and 10 more sections

Key Result

Theorem 14

Let $C \in F$ be a conflicting clause with the partial assignment $\pi$. Then, conflict analysis in $\Call{Analyze}{C}$ from alg:cdcl returns a conflicting clause that is implied by the clause set.

Figures (7)

  • Figure 1: Invariant properties for CDCL-based SAT solving and maintained by the different chronological backtracking (CB) strategies, particularly by non-chronological backtracking (NCB) and weak chronological backtracking (WCB).
  • Figure 2: $C_4$ is a MLI since it is satisfied only $v_2$ at level 2, and $v_3, \neg v_5$ are falsified at level 1. We use the notation $v@1$ to indicate that literal $v$ is on level $1$.
  • Figure 3: Different CB ways of handling the missed lower implications of \ref{['fig:mli-ex']}.
  • Figure 4: The clause $\neg v_{3}@2 \lor \neg v_4@1 \lor v_2@1$ is a missed lower implication in this example. $v_2$ and $\neg v_4$ are falsified at level 1, whereas $\neg v_{3}$ is only satisfied at level 2.
  • Figure 5: Average total number of propagations performed by NapSAT on the SATLIB 3-SAT random problem, clustered by the number of variables, and backtracking technique employed.
  • ...and 2 more figures

Theorems & Definitions (11)

  • Example 1: Missed Lower Implications -- MLI
  • Example 6
  • Example 8
  • Example 11
  • Definition 12: Candidate literal
  • Example 13
  • Theorem 14: Soundness of conflict analysis
  • Theorem 15: No missed unit implication
  • Corollary 16: No missed conflict/implication
  • Theorem 17: LSCB soundness and completeness
  • ...and 1 more