Shannon expansion and BDD construction. Represent Boolean functions as canonical directed acyclic graphs and manipulate them with efficient apply and restrict algorithms.
Part of Decision Procedures for Hardware Formal Verification on formal.org.