Binary Decision Diagrams

This tool offers the main BDD operations. The inputs are given as propositional formulas and are then converted to BDDs before applying the desired operation. The tool then lists the result and operand BDDs. The arguments of the particular operations are as follows:

• For the binary boolean operations *, the computed BDD is bdd1 * bdd2.
• For Compose, we replace the variable in bdd2 by bdd1.
• For boolean quantification, the bdd1 should be a conjunction of variables that are used to quantify over bdd2.
• For the Constrain and Restrict operations, bdd2 is minimized with care set bdd1.