Complement Edges in BDD

Definition

A Binary Decision Diagram (BDD) is an ordered directed acyclic graph in which each variable is encountered at most once on every root-to-terminal path and the variable order is consistent across all such paths. A BDD is reduced if it contains no isomorphic subgraphs and no redundant nodes. A reduced and ordered BDD (ROBDD) is a canonical representation of a Boolean function.

Complement edges are a shorthand mechanism used when drawing reduced BDDs: instead of explicitly constructing the negated subgraph for a function f, the same node is reused to represent both f and ¬f, with the edge pointing to the node being marked to indicate which polarity is intended. As a direct consequence, a reduced BDD drawn with complement edges only needs to contain the 1-terminal; the 0-terminal is implicit and is reached via the complemented edge of the root.

Example

Consider the function f = x₁x₂ + x₁x₂x₃. When its ROBDD is drawn using complement edges (Figure 3 of the cited source), the same node set simultaneously encodes f and ¬f. The diagram therefore contains only the 1-terminal node, and the complement of any sub-function is obtained by flipping the polarity bit on its incoming edge rather than by an additional NOT node.

Relevance to Constraint Solving and Weighting

Complement edges interact with algorithms that traverse BDDs to extract solutions. In the SCV constraint solver (built on the CUDD package), the characteristic function of every constraint is represented as a BDD and then traversed to enumerate solutions. Because complement edges let one node stand in for both polarities, naive traversal probabilities (e.g., assuming a 50/50 split between the 0-edge and 1-edge of a node) can be skewed. The cited example shows that for f = x₁x₂ + x₁x₂x₃ the intuitive traversal would assign 50% probability to the root's 1-edge, but the correct uniform distribution requires correcting this to 33%.

To obtain a uniform distribution of solutions across the constraint set, the SCV constraint solver runs a special weighting algorithm in a pre-processing step:

Traverse the BDD of all initial constraints.
Recursively compute the weights of the else- and then-children of each node.
Account for nodes that have been removed by BDD reduction rules (including the polarity flips introduced by complement edges).
Assign each node a probability derived from these weights.

During value generation, the pre-computed probabilities replace the naive per-edge probabilities, yielding a uniform distribution across all solutions.

Bit-Operator Constraints and BDD Construction

Because the SCV solver originally lacked bit-operator support, expressions such as a() & b(), a() | b(), ~a(), bit-select a()[i], and slice-select a().range(x,y) were added. Internally, scv_expression stores an expression tree whose leaves are variables/constants and whose interior nodes are operators; the BDD synthesis then applies the appropriate BDD-level operation (e.g., BDD-AND for each bit) for every bit of the operand vectors. The resulting BDD inherits the same complement-edge representation as the underlying CUDD package, so the weighting algorithm described above applies unchanged.

Limitations

The weighting algorithm is invoked once on the initial constraint BDD. If variables are subsequently fixed (e.g., disabled from randomization), the BDD is simplified but the cached probabilities are not updated. This causes the generated solutions to deviate from a uniform distribution, motivating the improvements described in the source paper.