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

Reduced, Ordered BDDs have the following very nice property:

tuis a tautology just whent=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?)