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.

翻译：我们提出可回溯处理（BI）框架，该框架允许在增量SAT求解过程中，于任意决策层级下的当前回溯链（trail）中执行处理操作。这一方法突破了传统处理必须仅在全局决策层级执行的长期限制，从而大幅提升其潜在有效性。我们聚焦三项高效核心技术：子句归并、自蕴含消解及有界变量消除（BVE）。我们证明如何在存在处理操作的情况下确保回溯的正确性，并验证在传播假设后应用BI进行增量预处理，能够在硬件模型检测竞赛2017的有界模型检测（BMC）基准测试中带来显著性能提升。该框架已在Island SAT求解器（IntelSAT的分支）中实现，相较于基线全局级增量预处理器，BI能够解决约1.5倍的困难边界问题。