A canonical generalization of OBDD
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Augmenting Ordered Binary Decision Diagrams with Conjunctive Decomposition
This paper augments OBDD with conjunctive decomposition to propose a generalization called OBDD[$\wedge$]. By imposing reducedness and the finest $\wedge$-decomposition bounded by integer $i$ ($\wedge_{\widehat{i}}$-deco…
Canonical Decision Diagrams Modulo Theories
Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.…
Belief Revision in Sentential Decision Diagrams
Belief revision is the task of modifying a knowledge base when new information becomes available, while also respecting a number of desirable properties. Classical belief revision schemes have been already specialised to…
Variable Shift SDD: A More Succinct Sentential Decision Diagram
The Sentential Decision Diagram (SDD) is a tractable representation of Boolean functions that subsumes the famous Ordered Binary Decision Diagram (OBDD) as a strict subset. SDDs are attracting much attention because they…
On oblivious branching programs with bounded repetition that cannot efficiently compute CNFs of bounded treewidth
In this paper we study complexity of an extension of ordered binary decision diagrams (OBDDs) called $c$-OBDDs on CNFs of bounded (primal graph) treewidth. In particular, we show that for each $k$ there is a class of CNF…