
TL;DR
Backtrackable Inprocessing (BI) is a novel framework allowing inprocessing during incremental SAT solving at any decision level, significantly improving performance on Bounded Model Checking benchmarks.
Contribution
It introduces a method to perform sound inprocessing at any decision level during incremental SAT solving, expanding its applicability and effectiveness.
Findings
BI enables solving approximately 1.5 times more difficult bounds.
Applying BI after propagating assumptions improves performance on BMC benchmarks.
The framework is implemented in the Island SAT solver, demonstrating practical benefits.
Abstract
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 1.5 as…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
