In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by modifying an existing BDD package, to several challenging Boolean satisfiability problems. Our resultsdemonstrate scaling for parity formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.

翻译：2006年，Biere、Jussila和Sinz发现了一个关键现象：用于构建有序二元决策图（BDD）的算法所依赖的底层逻辑，可以编码为扩展消解逻辑框架中的证明步骤。通过这一方法，基于BDD的布尔可满足性（SAT）求解器能够为子句集生成可验证的不可满足性证明。此类证明表明公式确实不可满足，而无需用户信任BDD包或基于其构建的SAT求解器。我们将其工作扩展至支持公式变量的任意存在量化——这是基于BDD的SAT求解器的关键能力。通过修改现有BDD包实现基于BDD的求解器，并将其应用于多个具有挑战性的布尔可满足性问题，我们验证了该方法的实用性。实验结果表明，在奇偶校验公式、Urquhart问题、残缺棋盘问题及鸽巢问题上，该方法展现出的扩展性远超其他能够生成证明的SAT求解器。