We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD. They can be seen as a restriction of structured d-DNNF; that is, d-DNNF that respect a vtree T. We show that TDDs enjoy the same tractability properties as OBDD, such as model counting, enumeration, conditioning, and apply, and are more succinct. In particular, we show that CNF formulas of treewidth k can be represented by TDDs of FPT size, which is known to be impossible for OBDD. We study the complexity of compiling CNF formulas into deterministic TDDs via bottom-up compilation and relate the complexity of this approach with the notion of factor width introduced by Bova and Szeider.
Figures & tables
Figure 1: The primal Prim(F) and incidence Inc(F) graphs of F=C1∧C2∧C3∧C4∧C5∧C6 where C1=(x1∨x2∨x3),C2=(x1∨x4∨x5),C3=(x4∨x6),C4=(¬x5∨x9),C5=(x6∨x7∨x8),C6=(x9∨x10∨x11) .
Figure 2: Tree decompositions for Prim(F) (left) and Inc(F) (right) from Figure 1 .
Figure 3: A vtree, an nTDD respecting it and the corresponding structured DNNF.
Transformation Name
Description
Conditioning (CD)
given a variable x and a∈{0,1} compute representation for f[x/a]
Forgetting (FO)
given a list x1,…,xℓ of variables compute ∃x1…∃xℓf
Singleton Forgetting (SFO)
same as FO, but only for a single variable
Conjunction ( ∧ C)
compute representation for ⋀i∈[ℓ]fi
Bounded Conjunction ( ∧ BC)
same as ∧ C, but only two input representations
Disjunction ( ∨ C)
compute representation for ⋁i∈[ℓ]fi
Figure 4: Overview of the transformations from the knowledge compilation map [ 19 ] that can be performed efficiently on different representation languages. The first table describes the transformations. For all of them, either one input representation of a Boolean function f or a list of representations of such functions f1,…,fℓ is given. Some transformations take additional inputs that are stated explicitly. In the second table, a ✓ means that the operation can be performed in polynomial time on representations from the language, whereas a • means that it takes super-polynomial time. All negative results are unconditionally true. For all transformations, we require that all inputs and outputs have the same vtree, resp. variable order.
Figure 5: An OBDD (left) represented as a TDD (right). The output of the TDD is represented in green and each node t of the vtree is made explicit by a rectangle around t -nodes.