A canonical generalization of OBDD

Florent Capelli; Guy Van den Broeck; Mart\'in Mu\~noz; Stefan Mengel; YooJung Choi

arxiv: 2604.05537 · v1 · submitted 2026-04-07 · 💻 cs.AI · cs.DS

A canonical generalization of OBDD

Florent Capelli , YooJung Choi , Stefan Mengel , Mart\'in Mu\~noz , Guy Van den Broeck This is my paper

Pith reviewed 2026-05-10 20:03 UTC · model grok-4.3

classification 💻 cs.AI cs.DS

keywords Tree Decision DiagramsOBDDknowledge compilationtreewidthCNF formulasd-DNNFmodel countingenumeration

0 comments

The pith

Tree Decision Diagrams generalize OBDDs to support the same tractable operations while representing treewidth-k CNF formulas in fixed-parameter tractable size.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Tree Decision Diagrams (TDDs) as a model for Boolean functions that relaxes the linear ordering of OBDDs to a tree structure. TDDs are defined as a restriction of structured d-DNNF that respect a given vtree. The authors establish that TDDs inherit the efficient operations of OBDDs, including model counting, enumeration, conditioning, and apply. This change yields strictly more succinct representations, in particular allowing CNF formulas of treewidth k to be compiled to TDDs whose size is FPT in k. A reader cares because the result enlarges the set of Boolean functions that admit practical knowledge compilation without losing polynomial-time query support.

Core claim

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.

What carries the argument

Tree Decision Diagram (TDD), a restriction of structured d-DNNF respecting a vtree T that replaces the total order of OBDDs with a tree decomposition while preserving determinism and decomposability.

If this is right

Model counting, enumeration, conditioning, and apply remain polynomial-time operations on TDDs, with runtime linear in the diagram size.
CNF formulas whose treewidth is at most k admit deterministic TDD representations of size f(k) times a polynomial in the formula size.
Bottom-up compilation of a CNF into a deterministic TDD runs in time governed by the factor width of the formula relative to the chosen vtree.
TDDs are strictly more succinct than OBDDs on an infinite family of functions that arise from bounded-treewidth constraints.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Choosing a vtree that minimizes factor width may yield practical compilation algorithms for instances whose treewidth is moderate but whose variable ordering is hard to find.
The same TDD representation could support lifted inference or marginal queries in probabilistic graphical models whose moral graph has small treewidth.
Because TDDs remain canonical under a fixed vtree, they may serve as a normal form for comparing the succinctness of different knowledge-compilation targets.
Extending the bottom-up construction to include dynamic vtree rebalancing could produce adaptive compilers that automatically discover good tree structures during compilation.

Load-bearing premise

The assumption that all tractability results for OBDDs carry over immediately to TDDs simply because TDDs are a syntactic restriction of structured d-DNNF.

What would settle it

A concrete CNF family of treewidth bounded by a constant whose smallest deterministic TDD has size superpolynomial in the input size.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

TDDs give OBDD operations plus FPT succinctness for treewidth-k CNFs, but the size bound needs the proofs to show the vtree determinism does not add hidden blowup.

read the letter

Hi, the main thing to know is that this paper defines TDDs as a vtree-respecting restriction of structured d-DNNF that keeps OBDD tractability while allowing FPT-size representations for treewidth-bounded CNFs, which standard OBDDs cannot do. They introduce the representation, prove that model counting, enumeration, conditioning, and apply remain polynomial-time, and establish the FPT size claim for CNFs of treewidth k. They also tie bottom-up compilation complexity to the factor width notion from Bova and Szeider. This is new because it combines the canonical decision-diagram structure with the succinctness lift over OBDDs in a way not covered in the cited prior work on OBDDs or d-DNNFs. The work does well by giving a precise definition and connecting the compilation result to an existing parameterized measure, which makes the contribution easier to place. The soft spot is around the central FPT claim: the extra determinism and ordering constraints per vtree node in TDDs could in principle require more size than general structured d-DNNF even when the vtree comes from a tree decomposition, and the abstract links it to bottom-up compilation without showing the details here. If the full proofs confirm no extra dependence on the vtree choice, the claim holds; otherwise it is the load-bearing part to check. Citations look clean and point to independent results without circularity. This is for knowledge compilation researchers who want representations that stay tractable yet scale better on structured instances. A reader working on parameterized succinctness for Boolean functions would get direct value from the new class and its bounds. The thinking is clear and engages the literature directly. I would send it for peer review so the size proofs and operation complexities can be verified in detail.

Referee Report

2 major / 1 minor

Summary. The paper introduces Tree Decision Diagrams (TDDs) as a canonical generalization of OBDDs, defined as a restriction of structured d-DNNF that respects a fixed vtree T. It claims that TDDs inherit the tractability properties of OBDDs (model counting, enumeration, conditioning, and apply) while being strictly more succinct, in particular that CNF formulas of treewidth k admit TDD representations of FPT size (impossible for OBDDs). The paper further studies the complexity of bottom-up compilation of CNFs into deterministic TDDs and relates this complexity to the factor width of the input formula.

Significance. If the central claims are established, TDDs would constitute a useful intermediate representation between the canonicity of OBDDs and the succinctness of structured d-DNNF, enabling FPT-size knowledge compilation for bounded-treewidth instances. The explicit connection drawn to factor width supplies a concrete, previously studied parameter for analyzing compilation cost. These features would be of interest to the knowledge-compilation community.

major comments (2)

[Abstract] Abstract: the claim that 'CNF formulas of treewidth k can be represented by TDDs of FPT size' is load-bearing for the succinctness result, yet the abstract supplies no argument showing why the additional ordering and determinism constraints imposed by the TDD definition (per vtree node) preserve an FPT bound that is known to hold for general structured d-DNNF; the transfer is not automatic and must be justified explicitly.
[Abstract] Abstract: the assertion that TDDs 'enjoy the same tractability properties as OBDD' for model counting, enumeration, conditioning, and apply likewise requires a concrete argument or reference to a later section demonstrating that the vtree-respecting restriction does not invalidate the standard OBDD algorithms; the stricter determinism and ordering per node could affect polynomial-time guarantees.

minor comments (1)

The abstract would be clearer if it indicated the sections or theorems in which the tractability proofs and the FPT-size construction are given.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback on our manuscript. We appreciate the recognition of TDDs as a potential intermediate representation between OBDDs and structured d-DNNF. We address the two major comments point by point below.

read point-by-point responses

Referee: [Abstract] Abstract: the claim that 'CNF formulas of treewidth k can be represented by TDDs of FPT size' is load-bearing for the succinctness result, yet the abstract supplies no argument showing why the additional ordering and determinism constraints imposed by the TDD definition (per vtree node) preserve an FPT bound that is known to hold for general structured d-DNNF; the transfer is not automatic and must be justified explicitly.

Authors: We agree that the abstract is concise and omits the justification. The full manuscript (Section 4) contains an explicit FPT construction: given a tree decomposition of width k, we choose a vtree aligned with the decomposition bags and compile the CNF bottom-up into a deterministic TDD whose nodes are bounded by 2^{O(k)} states per bag (via the factor-width connection also studied in the paper). The vtree-respecting and determinism constraints are satisfied by construction without increasing the asymptotic size beyond FPT, because the same state space that works for structured d-DNNF is reused while enforcing canonicity. We will revise the abstract to include a brief reference to this construction and the relevant section. revision: partial
Referee: [Abstract] Abstract: the assertion that TDDs 'enjoy the same tractability properties as OBDD' for model counting, enumeration, conditioning, and apply likewise requires a concrete argument or reference to a later section demonstrating that the vtree-respecting restriction does not invalidate the standard OBDD algorithms; the stricter determinism and ordering per node could affect polynomial-time guarantees.

Authors: The manuscript proves in Section 3 that the standard OBDD algorithms carry over verbatim to TDDs. Because a TDD is defined with respect to a fixed vtree, each subtree has a total variable order, allowing the same bottom-up dynamic-programming procedures (linear-time model counting, linear-time conditioning, etc.) to be applied without modification; determinism guarantees that each node represents a unique function, preserving the polynomial-time bounds. The vtree restriction actually simplifies some operations relative to unstructured d-DNNF. We will add an explicit pointer to Section 3 in the abstract. revision: partial

Circularity Check

0 steps flagged

No circularity: claims are proven results, not reductions to inputs or self-citations

full rationale

The paper introduces TDD as a restriction of structured d-DNNF respecting a vtree T, then states theorems that TDDs inherit OBDD tractability properties (model counting, enumeration, conditioning, apply) and admit FPT-size representations for treewidth-k CNFs. These are presented as results to be shown via compilation and complexity arguments tied to factor width, not as definitional identities or renamings. No equations reduce a 'prediction' to a fitted parameter, no load-bearing uniqueness theorem is imported from self-citation, and no ansatz is smuggled. The central FPT claim is a new succinctness result contrasting with known OBDD lower bounds, making the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

TDD is introduced as a new entity; the work relies on standard domain assumptions from knowledge compilation (properties of vtrees and structured d-DNNF) without new free parameters or ad-hoc axioms.

axioms (1)

domain assumption TDDs are a restriction of structured d-DNNF that respect a given vtree T
Stated in the definition of TDD in the abstract.

invented entities (1)

Tree Decision Diagram (TDD) no independent evidence
purpose: Canonical generalization of OBDD with improved succinctness
New model defined in the paper; no independent evidence provided beyond the claims.

pith-pipeline@v0.9.0 · 5439 in / 1315 out tokens · 78379 ms · 2026-05-10T20:03:41.658823+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages

[1]

23 Hélène Fargier, Stefan Mengel, and Jérôme Mengin

URL: https://www.ijcai.org/proceedings/2024/367. 23 Hélène Fargier, Stefan Mengel, and Jérôme Mengin. An extended knowledge compilation map for conditional preference statements-based and generalized additive utilities-based languages.Ann. Math. Artif. Intell., 92(5):1161–1196, 2024. URL: https://doi.org/10.1007/ s10472-024-09935-9,doi:10.1007/S10472-024-...

work page doi:10.1007/s10472-024-09935-9 2024
[2]

Without loss of generality, assumeg1̸=g′

By determinism, (g1,g 2)̸= (g′ 1,g′ 2). Without loss of generality, assumeg1̸=g′

work page
[3]

In this case,τ|Xt1 is a model of bothg 1 and ofg′

work page
[4]

Henceτis not a model ofg′

But this is not possible by induction. Henceτis not a model ofg′. We now show that there is a unique certificate for every modelτof C. Indeed, we have observed that ifP is a certificate forτthen τ|Xt is a model ofgP t . From what precedes, there is a uniquet-node αt that is satisfied byτ|Xt, henceαt =gP t for everyt, that is,P is unique. ◀ Proof of Theore...

work page
[5]

◀ B Proofs for Section 4 (Tractable Transformations) Elimination of constants.BeforestudyingtransformationsofTDD,weexplainhowonecan remove constant inputs in TDD

Thenτis a model ofg1 and ofg′ 1 which contradicts Theorem 2. ◀ B Proofs for Section 4 (Tractable Transformations) Elimination of constants.BeforestudyingtransformationsofTDD,weexplainhowonecan remove constant inputs in TDD. This is necessary to properly explain some transformations such as conditioning or forgetting where some variables are removed from t...

work page 2016
[6]

Repeat this until the state is closed

Check for closure; if the current state is not closed, then, for thet∈Tin which the test failed, add the witnessing partial assignment toNodest. Repeat this until the state is closed

work page
[7]

if the current state is not left-consistent, then, for the t∈Tin which the test failed, add theτr∈Nodesr(t) that witnesses failure toTestsℓ(t), and go back to step 1

Check for consistency; w.l.o.g. if the current state is not left-consistent, then, for the t∈Tin which the test failed, add theτr∈Nodesr(t) that witnesses failure toTestsℓ(t), and go back to step 1

work page
[8]

The state of the algorithm is now closed and consistent, so we build the TDD from Remark 32 and run an equivalence query. If the query answerstrue, the algorithm ends and we return the TDD; otherwise, we receive a counterexample assignmentτc, and then for each non-leaf nodet∈Twe addτc|Xt toNodes t, and then go back to step 1. This ends the description of ...

work page 2016
[9]

Hence HWBn[a∗]and HWBn[b∗]are distinct subfunctions

But thena∗×cis a model ofHWBn since a∗(xi) = 1but b∗×cis not sinceb∗(xi) = 0. Hence HWBn[a∗]and HWBn[b∗]are distinct subfunctions. In other words, HWBn has at least|A|= (t t/2 ) subfunctions overXI. It remains to show that we can pickc∈2X\XI so that it setsi−N1 variables to1. First, observe thati−N1≥0since by definition,N1≤pand i∈[p;p +ℓ]. We now have to ...

work page 2016

[1] [1]

23 Hélène Fargier, Stefan Mengel, and Jérôme Mengin

URL: https://www.ijcai.org/proceedings/2024/367. 23 Hélène Fargier, Stefan Mengel, and Jérôme Mengin. An extended knowledge compilation map for conditional preference statements-based and generalized additive utilities-based languages.Ann. Math. Artif. Intell., 92(5):1161–1196, 2024. URL: https://doi.org/10.1007/ s10472-024-09935-9,doi:10.1007/S10472-024-...

work page doi:10.1007/s10472-024-09935-9 2024

[2] [2]

Without loss of generality, assumeg1̸=g′

By determinism, (g1,g 2)̸= (g′ 1,g′ 2). Without loss of generality, assumeg1̸=g′

work page

[3] [3]

In this case,τ|Xt1 is a model of bothg 1 and ofg′

work page

[4] [4]

Henceτis not a model ofg′

But this is not possible by induction. Henceτis not a model ofg′. We now show that there is a unique certificate for every modelτof C. Indeed, we have observed that ifP is a certificate forτthen τ|Xt is a model ofgP t . From what precedes, there is a uniquet-node αt that is satisfied byτ|Xt, henceαt =gP t for everyt, that is,P is unique. ◀ Proof of Theore...

work page

[5] [5]

◀ B Proofs for Section 4 (Tractable Transformations) Elimination of constants.BeforestudyingtransformationsofTDD,weexplainhowonecan remove constant inputs in TDD

Thenτis a model ofg1 and ofg′ 1 which contradicts Theorem 2. ◀ B Proofs for Section 4 (Tractable Transformations) Elimination of constants.BeforestudyingtransformationsofTDD,weexplainhowonecan remove constant inputs in TDD. This is necessary to properly explain some transformations such as conditioning or forgetting where some variables are removed from t...

work page 2016

[6] [6]

Repeat this until the state is closed

Check for closure; if the current state is not closed, then, for thet∈Tin which the test failed, add the witnessing partial assignment toNodest. Repeat this until the state is closed

work page

[7] [7]

if the current state is not left-consistent, then, for the t∈Tin which the test failed, add theτr∈Nodesr(t) that witnesses failure toTestsℓ(t), and go back to step 1

Check for consistency; w.l.o.g. if the current state is not left-consistent, then, for the t∈Tin which the test failed, add theτr∈Nodesr(t) that witnesses failure toTestsℓ(t), and go back to step 1

work page

[8] [8]

The state of the algorithm is now closed and consistent, so we build the TDD from Remark 32 and run an equivalence query. If the query answerstrue, the algorithm ends and we return the TDD; otherwise, we receive a counterexample assignmentτc, and then for each non-leaf nodet∈Twe addτc|Xt toNodes t, and then go back to step 1. This ends the description of ...

work page 2016

[9] [9]

Hence HWBn[a∗]and HWBn[b∗]are distinct subfunctions

But thena∗×cis a model ofHWBn since a∗(xi) = 1but b∗×cis not sinceb∗(xi) = 0. Hence HWBn[a∗]and HWBn[b∗]are distinct subfunctions. In other words, HWBn has at least|A|= (t t/2 ) subfunctions overXI. It remains to show that we can pickc∈2X\XI so that it setsi−N1 variables to1. First, observe thati−N1≥0since by definition,N1≤pand i∈[p;p +ℓ]. We now have to ...

work page 2016