Incremental Inprocessing Rules beyond Resolution

Abstract

Formula simplification in the form of pre- and inprocessing is a crucial part of modern SAT solvers. While most inprocessing techniques focus on eliminating redundant clauses, significant performance improvements have recently been achieved with clause addition techniques. However, not all inprocessing techniques can be employed in incremental use cases. In particular, combining incremental reasoning with clause addition techniques based on more general redundancy properties in a sound and efficient way is an open challenge. In this paper, we extend the incremental inprocessing calculus for SAT solvers to facilitate some of these clause addition techniques and reason about the soundness and completeness of such systems. The resulting framework formally defines sufficient conditions for efficiently implementing in incremental SAT solvers such beyond resolution techniques, including Bounded Variable Addition (BVA) and certain Blocked Clause Addition (BCA) steps.