# 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.