TDD扩展了OBDD，能更紧凑表示高树宽公式，支持高效推理。
A canonical generalization of OBDD
- 基于有向树结构的决策图，是结构化d-DNNF的特例
- 树宽为k的CNF可被大小为固定参数可追踪的TDD表示
- 适合处理高树宽逻辑公式的压缩与快速计算
我们提出树决策图（TDD）作为布尔函数的模型，它推广了OBDD。TDD可视为满足特定变量树（vtree）结构的结构化d-DNNF。我们证明TDD具备与OBDD相同的可计算性特性，如计数、枚举、条件化和合并操作，并且表示更紧凑。特别地，我们展示了树宽为k的CNF公式可被大小为固定参数可追踪（FPT）的TDD表示，而这是不可能用OBDD实现的。我们研究了通过自底向上编译将CNF公式转化为确定性TDD的复杂度，并将其与Bova和Szeider提出的因子宽度概念相联系。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。