Backtrackable Inprocessing
For SAT solver users, especially in incremental settings like BMC, BI significantly improves performance by allowing inprocessing at any decision level.
Backtrackable Inprocessing (BI) lifts the restriction that inprocessing must occur only at the global decision level, enabling it at any point during incremental SAT solving. Applied to Bounded Model Checking benchmarks, BI solves ~1.5× as many difficult bounds as the baseline global-level incremental preprocessor.
We introduce Backtrackable Inprocessing (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solving. Our approach lifts the long-standing restriction that inprocessing must be performed only at the global decision level, thereby substantially increasing its potential effectiveness. We focus on three highly efficient core techniques: subsumption, self-subsuming resolution, and Bounded Variable Elimination (BVE). We show how to ensure sound backtracking in the presence of inprocessing, and demonstrate that applying BI for incremental preprocessing after propagating assumptions yields significant performance improvements on Bounded Model Checking (BMC) benchmarks from the Hardware Model Checking Competition 2017. Implemented in the Island SAT solver (IntelSAT's fork), BI enables solving $\sim$1.5$\times$ as many difficult bounds as the baseline global-level incremental preprocessor.