AI 中文总结
本文证明每个树决策图（TDD）可转换为拟多项式大小的有序二元决策图（OBDD），并表明TDD可在多项式时间内重构为任意新vtree的规范形式，从而实现不同vtree间TDD的等价性测试。
AI 中文摘要
树决策图（TDDs）是Capelli等人（SAT 2026）最近引入的一种数据结构。它们沿着一棵vtree进行结构化，其规范形式的大小介于有序二元决策图（OBDDs）和确定性结构化DNNF电路（d-SDNNFs）之间。虽然TDD与d-SDNNF之间的简洁性差距是指数级的，但OBDD与TDD之间仅显示出拟多项式级别的分离，并且这一分离是否最优仍是一个开放问题。我们通过证明每个TDD都可以被转换为一个规模为拟多项式大小的等价OBDD，肯定地回答了这个问题。尽管这可能被视为一个弱点，但我们的第二个结果表明，TDD与OBDD共享另一个已知d-SDNNF不具备的优良性质：给定一个TDD和另一个目标vtree，可以在输入和输出的多项式时间内构造出尊重新vtree的最小且规范的TDD。因此，我们还得到了在不同vtree上的TDD之间的等价性测试可以在多项式时间内完成的结果。
英文摘要
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.
