TBUDDY: a Proof-Generating BDD Package

EasyChair Preprint 8471

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, Gaussian elimination, clausal proofs

@booklet{EasyChair:8471,
  author    = {Randal Bryant},
  title     = {TBUDDY: a Proof-Generating BDD Package},
  howpublished = {EasyChair Preprint 8471},
  year      = {EasyChair, 2022}}