6  Examples

6.1  Programming the negation

The following function implements the Boolean negation. Indeed, using this function is quite ineffective, since the built-in not operator does the same thing in constant time, but this simple algorithm shows the genaral structure of any unary bdd-based operator.

negation(a) :=
   if compare(a, true) then false
   else if compare(a, false) then true
   else ite( root(a), negation(high(a)), negation(low(a)));

In order to understand this algorithm, remain that any bdd a is either:

• true, i.e. the always true formula,
• false, i.e. the always false formula,
• a ternary "expression" of the form ite(root(a), high(a), low(a)), where root(a) is an argument ¹, and high(a) and low(a) are two formulas not depending in root(a).

The algorithm first treat the basic cases, by comparing the parameter to the constants true and false, and after the genaral case, where the parameter still depends on some argument. In this case, the function is recursively called on the corresponding high and low parts, and the results are combined under a test of the root argument.

6.2  Finding an implicant in a bdd

This is another example of unary function, that builds, if it exists, an monomial that implies a :

path(a) :=
  if compare(a, true) then true
  else if compare(a, false) then false
  else if compare(high(a), false) then (not root(a) and path(low(a)))
  else (root(a) and path(high(a)))
;

6.3  Programming the union

The following function implements the Boolean or. The only interest is in showing how to build a binary operator. We first treat the basic cases, where either a, b are constants. Then, we treat the case where both a and b are "binary" bdds. In this last case, we use the binary extension of the root operator to get the "minimal" argument between root(a) and root(b), and call it min_root. Then, the recursive calls are made by decomposing both parameters according to min_root.

union(a, b) :=
   if (compare(a, true) or compare(b, false)) then a
   else if (compare(b, true) or compare(a, false)) then b
   else let min_root := root(a, b) in
      ite(min_root,
          union(constrain(a, min_root), constrain(b, min_root)),
          union(constrain(a, not min_root), constrain(b, not min_root))
      );

The use of the generalized cofactor in the recursive calls may seem a little bit tricky. It is justified by the fact that (for instance) either constrain(a, min_root) = a if min_root ≠ root(a), or constrain(a, min_root) = high(a) if min_root = root(a).