Ubdds
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
structurally equal.
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.
Subtopics
- Equal-by-eval-bdds
- Reasoning strategy: reduce equality of ubdds to equality of an
arbitrary evaluation.
- Ubdd-constructors
- Basic functions for constructing UBDDs.
- Eval-bdd
- Sematics of a UBDD.
- Ubddp
- Recognizer for well-formed ubdds.
- Ubdd-fix
- (ubdd-fix x) constructs a valid ubddp that is treated
identically to x under eval-bdd.
- Q-sat
- (q-sat x) finds a satisfying assignment for the UBDD x, if
one exists.
- Bdd-sat-dfs
- (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.
- Eval-bdd-list
- Apply eval-bdd to a list of UBDDs.
- Qcdr
- The "false branch" of a UBDD.
- Qcar
- The "true branch" of a UBDD.
- Q-sat-any
- (q-sat-any a) finds an assignment that satisfies at least one
UBDD in the list of UBDDs x.
- Canonicalize-to-q-ite
- Reasoning strategy: rewrite all BDD-building functions into calls of
q-ite.
- Ubdd-listp
- Recognizer for a list of ubdds.
- Qcons
- Raw construtor for UBDDs.
