Tree Decision Diagrams: A New Canonical Model for Boolean Functions

A team of researchers from multiple institutions has introduced Tree Decision Diagrams (TDDs), a new canonical model for Boolean functions that generalizes Ordered Binary Decision Diagrams (OBDDs) while overcoming several of their limitations.

TDDs can be viewed as a restriction of structured d-DNNF (deterministic Decomposable Negation Normal Form) that respects a vtree structure. This relationship to existing formalisms is crucial because it means TDDs inherit the tractability properties that make OBDDs valuable for practical applications - including model counting, enumeration, conditioning, and the apply operation - while offering greater succinctness.

The key breakthrough is that TDDs can represent CNF formulas of treewidth k using fixed-parameter tractable (FPT) size representations. This is significant because it's known to be impossible for standard OBDDs. Treewidth is a fundamental graph parameter that measures how "tree-like" a graph is, and many real-world problems have bounded treewidth, making this capability practically relevant.

The researchers also studied the complexity of compiling CNF formulas into deterministic TDDs using bottom-up compilation approaches. They connected this compilation complexity to the notion of factor width, a concept introduced by Bova and Szeider in previous work. This connection helps establish theoretical bounds on when and how efficiently TDDs can be constructed from arbitrary Boolean formulas.

From a practical standpoint, this work could impact areas where OBDDs are already used, such as formal verification, model checking, and knowledge compilation. The ability to handle formulas with bounded treewidth more efficiently could make TDDs particularly useful for applications in AI planning, probabilistic reasoning, and constraint satisfaction problems where such structures naturally arise.

The canonical nature of TDDs - meaning that equivalent Boolean functions have identical representations - preserves one of the most valuable properties of OBDDs for applications requiring canonicity, such as equivalence checking and symbolic model checking.

This research represents a significant advance in the theory of Boolean function representation, bridging the gap between the practical utility of OBDDs and the need to handle more complex formula structures efficiently.