Binary Decision Diagram Reduction

A graph-based technique for representing Boolean functions as directed acyclic graphs (binary decision diagrams, BDDs) together with reduction rules (merge isomorphic subgraphs and eliminate redundant tests) that can produce a canonical, reduced ordered BDD (ROBDD) for a fixed variable ordering, enabling efficient equivalence and satisfiability checks.