Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver
复制标题
DOI：
10.1007/978-3-030-79876-5_25
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
R. Bryant;Marijn J. H. Heule
中科院分区：
文献类型：
--
作者：
R. Bryant;Marijn J. H. Heule
现有的证明生成量化布尔公式（QBF）求解器必须根据公式是假（反驳）还是真（满意）来构造不同类型的证明。我们表明，QBF求解器的基础上有序二元决策图（BDDs）可以发出一个单一的双重证明，因为它的运作，支持任何一种结果。这种形式包括一系列的equivalencepreserving子句添加和删除步骤中的扩展的决议框架。对于假公式，证明以空子句终止，表示冲突。对于一个真的，它以删除所有分句结束，表示重言式。证明的长度和检查它所需的时间都与执行的BDD操作的总数成正比。我们使用基于双人瓷砖游戏的可扩展基准来评估我们的求解器。
Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalencepreserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.