SE547: BDDs: Binary Decision Diagrams [12/22]

Reduced, Ordered BDDs have the following very nice property:

t u is a tautology     just when     t = u

that is syntactic equality is the same as semantic equality.

In particular, for ROBDDs:

• The only tautology is 1.
• The only unsatisfiable formula is 0.

This makes checking for satisfiability pretty easy! (But remember that satisfiability is NP-complete; where did the hard work go?)