Tree decision diagrams transformed efficiently into ordered binary forms
Restructuring Tree Decision Diagrams
Computational Complexity
Summary
Tree Decision Diagrams (TDDs) are a way to represent logical decisions in a structured form. The authors showed that any TDD can be turned into an Ordered Binary Decision Diagram (OBDD) without the size becoming too large, proving a previously open question. They also found that TDDs can be rearranged according to different structures quickly, which helps check if two TDDs are effectively the same. This makes working with TDDs more flexible and efficient.
What this means in practice
- •For knowledge compilation engineers: Use the polynomial-time transformation between TDDs and OBDDs to optimize logical circuit representations and equivalence checks efficiently.
- •For hardware verification teams: Employ the canonical TDD restructuring to simplify and verify logic designs under different configurations without exponential size increase.
A theory result. No direct application yet.
Authors
Christoph Berkholz, Matthäus Micun, Igor Razgon
Abstract
Tree Decision Diagrams (TDDs) are a data structure recently introduced by Capelli et al. (SAT 2026). They are structured along a vtree and the size of their canonical form lies between Ordered Binary Decision Diagrams (OBDDs) and deterministic structured DNNF circuits (d-SDNNFs). While the succinctness gap between TDD and d-SDNNF is exponential, only a quasipolynomial separation between OBDD and TDD has been shown and it was left as open question whether this is optimal. We answer this question affirmatively by showing that every TDD can be transformed to an equivalent OBDD of quasipolynomial size. Although this might be seen as a weakness, our second result shows that TDDs share another desirable property with OBDDs that is not known to hold for d-SDNNF: Given a TDD and another target vtree, it is possible to construct the minimal and canonical TDD respecting the new vtree in time polynomial in the input and output. As a result we also obtain that the equivalence test between TDDs over different vtrees can be done in polynomial time.