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.
Monadic second order logic (MSO2) plays an important role in parameterized complexity due to the Courcelle's theorem. This theorem states that the problem of checking if a given graph has a property specified by a given MSO2 formula can be solved by a parameterized linear time algorithm with respect to the treewidth of the graph and the size of the formula. We extend this result by showing that models of MSO2 formula with free variables can be represented with a decision diagram whose size is parameterized linear in the above mentioned parameter. In particular, we show a parameterized linear upper bound on the size of a sentential decision diagram (SDD) when treewidth is considered and a parameterized linear upper bound on the size of an ordered binary decision diagram (OBDD) when considering the pathwidth in the parameter. In addition, building on a lower bound on the size of OBDD by Razgon (2014), we show that there is an MSO2 formula and a class of graphs with bounded treewidth which do not admit an OBDD with the size parameterized by the treewidth. Our result offers a new perspective on the Courcelle's theorem and connects it to the area of knowledge representation.
Petr Kučera, Petr Martinek
Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic
Chain of Thought (CoT) lifts the expressive ceiling of bounded-depth Transformers, with characterizations tying the number of CoT steps to circuit complexity classes. What remains largely missing are concrete instantiations with explicit, depth-bounded constructions, and the traversal procedures such characterizations presuppose. We close this gap for branching complexity. We give CoT realizations of depth-first search (DFS) and of Dijkstra algorithm, the latter subsuming breadth-first search, by unique hard-attention decoders of at most two layers, and use them as a shared computational substrate: reusing the DFS decoder yields the Strahler number of an n-vertex tree in 2n−1 steps with four layers, and reusing the Dijkstra decoder yields its width in n−1 steps with three. Since computing the Strahler number of a binary tree given as a term is NC\textsuperscript{1}-complete, and our constructions handle arbitrary n-ary trees without layer normalization or positional encodings, this is a non-trivial witness for the linear-step regime of the CoT hierarchy. Exploiting the classical bijection between ordered trees and Dyck paths, itself realized by our DFS construction, which emits the path as it traverses, we give independent constructions for both measures on the path representation.
Debanjan Dutta, Anish Chakrabarty, Swagatam Das
Indian Statistical Institute Kolkata, India · LTCI, Télécom Paris Palaiseau, France
In this paper, we investigate preprocessing techniques aimed at improving the efficiency of accessing models of propositional formulas represented in conjunctive normal form (CNF). We focus on three fundamental tasks: uniform sampling, direct model access, and model enumeration. Our analysis reveals that most state-of-the-art preprocessors, when they do not preserve formula equivalence, are generally unsuitable for these tasks. In contrast, we demonstrate that preprocessors which preserve model counts can be effectively leveraged, provided relevant preprocessing information is maintained. To validate our approach, we perform extensive experiments on a diverse suite of benchmarks from multiple domains. The experimental results show that our preprocessing methods are both efficient and robust, yielding significant performance improvements for model access queries when CNF formulas are compiled into d-DNNF representations.