Propagation 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). The authors differentiate between encodings which implement consistency or domain consistency by unit propagation from encodings which are unit refutation complete or propagation complete. The difference is that in the former case we do not care about propagation strength of the encoding with respect to the auxiliary variables while in the latter case we treat all variables (the main and the auxiliary ones) in the same way. The currently known encodings of DNNF theories implement domain consistency. Building on these encodings we generalize the result of (Abio et al. 2016) on a propagation complete encoding of decision diagrams and present a propagation complete encoding of a DNNF and its generalization for variables with finite domains.
Code (0)
등록된 구현이 없습니다.
Tasks
NegationSimilar Papers 제목 키워드 기반
Backdoor Decomposable Monotone Circuits and their Propagation Complete Encodings
We describe a compilation language of backdoor decomposable monotone circuits (BDMCs) which generalizes several concepts appearing in the literature, e.g. DNNFs and backdoor trees. A $\mathcal{C}$-BDMC sentence is a mono…
SentenceA 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…
NegationOn 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. …
NegationRelationPushing the Envelope: From Discrete to Continuous Movements in Multi-Agent Path Finding via Lazy Encodings
Multi-agent path finding in continuous space and time with geometric agents MAPF$^\mathcal{R}$ is addressed in this paper. The task is to navigate agents that move smoothly between predefined positions to their individua…
Multi-Agent Path FindingNavigateTop-Down Knowledge Compilation for Counting Modulo Theories
Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows infe…
Negation