ProCount: weighted projected model counting with graded project-join trees

DOI10.1007/978-3-030-80223-3_11OpenAlexW3184163263MaRDI QIDQ2118296

Jeffrey M. Dudek, Moshe Y. Vardi, Vu H. N. Phan

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_11

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Related Items (2)

Generating random instances of weighted model counting. An empirical analysis with varying primal treewidth ⋮ Solving projected model counting by utilizing treewidth and its limits

Uses Software

• SATzilla
• DRAT-trim
• PMTK
• htd
• Sylvan
• GANAK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic techniques in satisfiability solving
• Random generation of combinatorial structures from a uniform distribution
• Graph minors. X: Obstructions to tree-decomposition
• Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
• Which problems have strongly exponential complexity?
• Exploiting treewidth for projected model counting and its limits
• Bucket elimination: A unifying framework for reasoning
• Algorithms for propositional model counting
• Positive-instance driven dynamic programming for treewidth
• Taming high treewidth with abstraction, nested dynamic programming, and database technology
• Exploiting structure in quantified formulas
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• DYNAMIC PROGRAMMING AND A NEW FORMALISM IN THE THEORY OF INTEGRAL EQUATIONS
• Simple Linear-Time Algorithms to Test Chordality of Graphs, Test Acyclicity of Hypergraphs, and Selectively Reduce Acyclic Hypergraphs
• $$\#\exists $$ SAT: Projected Model Counting
• Graph-Based Algorithms for Boolean Function Manipulation
• Graph Bisection with Pareto Optimization
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• Expansion-based QBF Solving on Tree Decompositions*

This page was built for publication: ProCount: weighted projected model counting with graded project-join trees