OBDD拡張のTree Decision Diagram新手法提案

Florent Capelliら5名の研究者が、ブール関数のモデル表現手法であるOBDD（Ordered Binary Decision Diagram）を一般化したTree Decision Diagrams（TDD）を新たに提案した。この研究論文はarXivに2026年4月7日に投稿され、SAT26会議への提出が予定されている。

TDDは構造化d-DNNFの制限として位置づけられ、vtree構造Tを尊重するd-DNNFの一種として定義される。研究チームは、TDDがOBDDと同等の計算可能性を持ちながら、より簡潔な表現を実現することを示した。具体的には、モデル計数、列挙、条件付け、適用といった基本操作がTDDでも効率的に実行可能であることを証明している。

特に重要な成果として、treewidth kを持つCNF式をFPT（Fixed Parameter Tractable）サイズのTDDで表現できることを示した。これはOBDDでは理論的に不可能とされていた表現能力の大幅な向上を意味する。

さらに、研究では決定論的TDDへのCNF式のボトムアップコンパイルの複雑性を分析し、このアプローチの計算複雑性をBovaとSzeiderが導入したfactor widthの概念と関連付けて説明している。この新しい手法は、人工知能分野における論理推論や知識表現の効率化に寄与する可能性がある。