Compilation and Fast Model Counting beyond CNF
Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.
Code (0)
등록된 구현이 없습니다.
Tasks
modelNegationSimilar Papers 제목 키워드 기반
Beyond the Grounding Bottleneck: Datalog Techniques for Inference in Probabilistic Logic Programs (Technical Report)
State-of-the-art inference approaches in probabilistic logic programming typically start by computing the relevant ground program with respect to the queries of interest, and then use this program for probabilistic infer…
Knowledge GraphsTop-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…
NegationEfficient Knowledge Compilation Beyond Weighted Model Counting
Quantitative extensions of logic programming often require the solution of so called second level inference tasks, i.e., problems that involve a third operation, such as maximization or normalization, on top of addition …
modelFast Converging Anytime Model Counting
Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have b…
modelSTSFusing First-order Knowledge Compilation and the Lifted Junction Tree Algorithm
Standard approaches for inference in probabilistic formalisms with first-order constructs include lifted variable elimination (LVE) for single queries as well as first-order knowledge compilation (FOKC) based on weighted…