Tbuddy: A Proof-Generating BDD Package
Tbuddy: A Proof-Generating BDD Package
复制标题
DOI：
10.34727/2022/isbn.978-3-85448-053-2_10
复制
发表时间：
2022-10
期刊：
影响因子：
--
通讯作者：
R. Bryant
中科院分区：
文献类型：
--
作者：
R. Bryant
TBUDDY库允许构造和操作简化的有序二元决策图（BDD）。它扩展了BUDDY BDD包的功能，以支持可信的BDD，其中生成的BDD伴随着其逻辑属性的证明。这些证明是在一个标准的子句框架中表达的，有各种各样的证明检查器可供使用。通过其应用程序接口（API）构建TBUDDY，使开发人员能够实现自动推理工具，为其结果生成正确性证明。在某些情况下，BDD充当工具的核心推理机制，而在其他情况下，它们提供了从核心推理器到证明生成的桥梁。一个基于TBUDDY的布尔可满足性（SAT）求解器在为一些问题生成不可满足性证明时实现多项式缩放，这些问题使用标准求解器生成指数大小的证明。它对于包含奇偶约束的公式表现得特别好，其中它可以采用高斯消去法来系统地简化约束。
The TBUDDY library enables the construction and manipulation of reduced, ordered binary decision diagrams (BDDs). It extends the capabilities of the BUDDY BDD package to support trusted BDDs, where the generated BDDs are accompanied by proofs of their logical properties. These proofs are expressed in a standard clausal framework, for which a variety of proof checkers are available. Building on TBUDDY via its application-program interface (API) enables developers to implement automated reasoning tools that generate correctness proofs for their outcomes. In some cases, BDDs serve as the core reasoning mechanism for the tool, while in other cases they provide a bridge from the core reasoner to proof generation. A Boolean satisfiability (SAT) solver based on TBUDDY achieves polynomial scaling when generating unsatisfiability proofs for a number of problems that yield exponentially-sized proofs with standard solvers. It performs particularly well for formulas containing parity constraints, where it can employ Gaussian elimination to systematically simplify the constraints.