Structured d-DNNF Is Not Closed Under Negation
Both structured d-DNNF and SDD can be exponentially more succinct than OBDD. Moreover, SDD is essentially as tractable as OBDD. But this has left two important open questions. Firstly, does OBDD support more tractable transformations than structured d-DNNF? And secondly, is structured d-DNNF more succinct than SDD? In this paper, we answer both questions in the affirmative. For the first question we show that, unlike OBDD, structured d-DNNF does not support polytime negation, disjunction, or existential quantification operations. As a corollary, we deduce that there are functions with an equivalent polynomial-sized structured d-DNNF but with no such representation as an SDD, thus answering the second question. We also lift this second result to arithmetic circuits (AC) to show a succinctness gap between PSDD and the monotone AC analogue to structured d-DNNF.
Code (0)
등록된 구현이 없습니다.
Tasks
NegationSimilar Papers 제목 키워드 기반
On the relation between structured $d$-DNNFs and SDDs
Structured $d$-DNNFs and SDDs are restricted negation normal form circuits used in knowledge compilation as target languages into which propositional theories are compiled. Structuredness is imposed by so-called vtrees. …
NegationRelationA Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Sever…
NegationEfficient Explanations for Knowledge Compilation Languages
Knowledge compilation (KC) languages find a growing number of practical uses, including in Constraint Programming (CP) and in Machine Learning (ML). In most applications, one natural question is how to explain the decisi…
NegationLower Bounds for Exact Model Counting and Applications in Probabilistic Databases
The best current methods for exactly computing the number of satisfying assignments, or the satisfying probability, of Boolean formulas can be seen, either directly or indirectly, as building 'decision-DNNF' (decision de…
NegationPropagation complete encodings of smooth DNNF theories
We investigate conjunctive normal form (CNF) encodings of a function represented with a decomposable negation normal form (DNNF). Several encodings of DNNFs and decision diagrams were considered by (Abio et al. 2016). Th…
Negation