A hons-based, unlabeled Binary Decision
Diagram (bdd) representation of Boolean functions.
UBDDs ("unlabeled bdds") are a concise and efficient
implementation of binary decision diagrams. Unlike most BDD packages, our
internal nodes are not labelled; instead, each node's depth from the root
determines its variable.
The valid UBDDs are recognized by ubddp. Structurally, UBDDs are a
subset of purely Boolean cons-trees, i.e., trees where all the tips are t
or nil. For instance, the valid one-variable UBDDs are:
- t or nil for "var is irrelevant to this decision", or
- (t . nil) for "if var then t else nil, or
- (nil . t) for "if var then nil else t
But (t . t) and (nil . nil) are not permitted—we reduce them
to t and nil, respectively. This restriction leads to a key property
of UBDDs, viz. two UBDDs are semantically equivalent exactly when they are
The semantics of a UBDD are given by the interpreter function eval-bdd. Operations that construct UBDDs, such as q-not and q-and, are proven correct w.r.t. this interpreter. We also provide various
theorems to reason about UBDD operations, including the important theorem equal-by-eval-bdds, and implement some computed-hints for automating
the use of this theorem.
Our UBDD implementation is made efficient via hons-and-memoization.
We construct UBDDs with hons and memoize UBDD constructors such
as q-not and q-and.
- Reasoning strategy: reduce equality of ubdds to equality of an
- Basic functions for constructing UBDDs.
- Sematics of a UBDD.
- Recognizer for well-formed ubdds.
- (ubdd-fix x) constructs a valid ubddp that is treated
identically to x under eval-bdd.
- (q-sat x) finds a satisfying assignment for the UBDD x, if
- (bdd-sat-dfs x) finds a satisfying assignment for the UBDD x, if
one exists. It works even if x is not a well-formed UBDD, but it might be
slow in that case.
- Apply eval-bdd to a list of UBDDs.
- The "false branch" of a UBDD.
- The "true branch" of a UBDD.
- (q-sat-any a) finds an assignment that satisfies at least one
UBDD in the list of UBDDs x.
- Reasoning strategy: rewrite all BDD-building functions into calls of
- Recognizer for a list of ubdds.
- Raw construtor for UBDDs.