Ordered Binary Decision Diagrams (BDDs) Wiki

Ordered Binary Decision Diagrams (BDDs)

Technique WIKI v1 · 5/30/2026

Ordered Binary Decision Diagrams (BDDs) are described in the provided sources as Boolean methods used in both formal verification and SAT solving. The evidence shows their use after reducing EUF formulas to propositional logic for processor verification, and public context reports BDD-based SAT solvers that can generate polynomial-size unsatisfiability proofs for the pigeonhole problem under favorable variable-ordering choices.

Overview

Ordered Binary Decision Diagrams (BDDs) are referenced in the provided sources as a Boolean method that can be applied once verification conditions have been reduced to propositional logic. In the processor-verification setting, formulas in the logic of equality with uninterpreted functions (EUF) are reduced to propositional formulas so that Boolean methods such as BDDs and SAT checkers can be used.

Use in processor verification

The cited processor-verification work uses EUF as an abstraction for data manipulation in processor correctness proofs. It states that reducing EUF formulas to propositional formulas enables the use of BDDs and Boolean satisfiability checkers for verification. The same source also reports simplifications based on the observation that many equations appear only in positive form, allowing the verification method to restrict attention to "maximally diverse" interpretations of function symbols. Experimental results in that paper are reported as demonstrating efficiency on pipelined-processor verification using the Burch-and-Dill method.

Use in BDD-based SAT solving

Public context also describes SAT solvers based on BDDs, especially solvers capable of generating proofs of unsatisfiability. In particular, a 2023 note reports that for the pigeonhole problem in the standard direct encoding, a BDD-based bucket-elimination approach can generate polynomial-time unsatisfiability proofs when different variable orderings are used for the BDDs and for the buckets. The same note reports experimental scaling of approximately (O(n^5)) for these proofs, while using the same variable ordering for both BDDs and buckets leads to exponential scaling.

Evidence-backed scope

Within the provided evidence, BDDs are therefore supported as a technique used in:

propositionalized EUF-based processor verification, and
SAT solving and unsatisfiability proof generation, where variable ordering can strongly affect scaling.

The sources provided do not supply a fuller construction-level description of BDDs, so this article is limited to these evidence-backed uses and reported properties.

LINKED ENTITIES

1 links

Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic USES

CITATIONS

5 sources

5 citations

[1] EUF formulas can be reduced to propositional formulas so that Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and SAT checkers can be used for processor verification. Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic

[2] The processor-verification approach simplifies generated propositional formulas by exploiting that many equations appear only in positive form and by restricting attention to 'maximally diverse' interpretations. Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic

[3] The cited processor-verification paper reports experimental results demonstrating efficiency when verifying pipelined processors using the Burch-and-Dill method. Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic

[4] A 2023 note reports that BDD-based SAT solvers can generate polynomial-time unsatisfiability proofs for the pigeonhole problem in direct encoding when bucket elimination uses different variable orderings for the BDDs and the buckets. Notes on "Bounds on BDD-Based Bucket Elimination"

[5] The same 2023 note reports experimental scaling of approximately O(n^5) for those proofs and confirms exponential scaling when the same variable ordering is used for both BDDs and buckets. Notes on "Bounds on BDD-Based Bucket Elimination"