Download PDFOpen PDF in browser

TBUDDY: a Proof-Generating BDD Package

EasyChair Preprint no. 8471

17 pagesDate: July 12, 2022

Abstract

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 can achieve 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.

Keyphrases: Binary Decision Diagrams, clausal proofs, Gaussian elimination

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:8471,
  author = {Randal Bryant},
  title = {TBUDDY: a Proof-Generating BDD Package},
  howpublished = {EasyChair Preprint no. 8471},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser