\#SAT: projected model counting

DOI10.1007/978-3-319-24318-4_10MaRDI QIDQ3453218zbMATH OpenOpenAlexFDO

Authors Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, Peter J. Stuckey

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.07648

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07)

Abstract: Model counting is the task of computing the number of assignments to variables V that satisfy a given propositional theory F. Model counting is an essential tool in probabilistic reasoning. In this paper, we introduce the problem of model counting projected on a subset P of original variables that we call 'priority' variables. The task is to compute the number of assignments to P such that there exists an extension to 'non-priority' variables VP that satisfies F. Projected model counting arises when some parts of the model are irrelevant to the counts, in particular when we require additional variables to model the problem we are counting in SAT. We discuss three different approaches to projected model counting (two of which are novel), and compare their performance on different benchmark problems. To appear in 18th International Conference on Theory and Applications of Satisfiability Testing, September 24-27, 2015, Austin, Texas, USA

Recommendations

• Projected model counting: beyond independent support
• Theory and Applications of Satisfiability Testing
• Two approximate algorithms for model counting
• Model counting: a new stategy for obtaining good bounds
• Algorithms for propositional model counting

Cites work

• A machine program for theorem-proving
• Conflict-Driven Answer Set Enumeration
• Conflict-driven answer set solving: from theory to practice
• Decomposable negation normal form
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• Quantifier elimination by dependency sequents
• Solution Enumeration for Projected Boolean Search Problems
• Solving \#SAT and Bayesian inference with backtracking search
• Theory and Applications of Satisfiability Testing

Cited in

(16)

• Exploiting treewidth for projected model counting and its limits
• ProCount: weighted projected model counting with graded project-join trees
• The joy of probabilistic answer set programming: semantics, complexity, expressivity, inference
• Definability for model counting
• Solving projected model counting by utilizing treewidth and its limits
• \(T_{\mathcal{P}}\)-compilation for inference in probabilistic logic programs
• A study of symmetry breaking predicates and model counting
• Counting of Teams in First-Order Team Logics
• OuterCount: a first-level solution-counter for quantified Boolean formulas
• Projected model counting: beyond independent support
• On the benefits of knowledge compilation for feature-model analyses
• On enumerating short projected models
• Dynamic blocked clause elimination for projected model counting
• Entailment vs. verification for partial-assignment satisfiability and enumeration
• Counting of teams in first-order team logics
• On CNF conversion for SAT and SMT enumeration

Describes a project that uses

Uses Software

• sharpSAT
• Chaff

This page was built for publication: \(\#{\exists}\mathrm{SAT}\): projected model counting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453218)