Lazy Reimplication in Chronological Backtracking

TL;DR

This paper introduces a lazy reimplication method for chronological backtracking in SAT solvers, reducing unnecessary propagations by reapplying literals on demand, and demonstrates its effectiveness in existing solvers.

Contribution

It presents a novel lazy reimplication technique for chronological backtracking, improving efficiency and modularity in SAT solving.

Findings

Reduces propagations in SAT solving

Applicable to multiple solvers like CaDiCaL and Glucose

Enhances efficiency of chronological backtracking

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.