A Canonical Generalization of OBDD
7 hours ago
- #Computational complexity
- #Decision diagrams
- #Boolean functions
- Tree Decision Diagrams (TDD) are introduced as a generalization of OBDD for modeling Boolean functions, similar to d-DNNF restricted by a vtree.
- TDDs retain tractable operations like model counting, enumeration, conditioning, and applying functions, while being more succinct than OBDDs.
- CNF formulas with treewidth k can be represented by TDDs of fixed-parameter tractable size, which OBDDs cannot achieve.
- The compilation of CNF formulas into deterministic TDDs via bottom-up methods is analyzed, linking its complexity to factor width as defined by Bova and Szeider.