SE547: BDDs: Binary Decision Diagrams [12/22] Previous pageContentsNext page

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:

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

Previous pageContentsNext page