Algorithms for propositional model counting

DOI10.1016/j.jda.2009.06.002zbMath1214.05166OpenAlexW2984546510MaRDI QIDQ2266937

Stefan Szeider, Marko Samer

Publication date: 26 February 2010

Published in: Journal of Discrete Algorithms (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jda.2009.06.002

zbMATH Keywords

propositional satisfiabilityparameterized algorithmsmodel counting

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85)

Related Items (29)

On preprocessing techniques and their impact on propositional model counting ⋮ A Study of Symmetry Breaking Predicates and Model Counting ⋮ Community Structure Inspired Algorithms for SAT and #SAT ⋮ Backdoors to Satisfaction ⋮ Model counting for CNF formulas of bounded modular treewidth ⋮ Sum-of-Products with Default Values: Algorithms and Complexity Results ⋮ Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all? ⋮ Satisfiability of acyclic and almost acyclic CNF formulas ⋮ Exploiting Database Management Systems and Treewidth for Counting ⋮ Solving projected model counting by utilizing treewidth and its limits ⋮ A new probabilistic constraint logic programming language based on a generalised distribution semantics ⋮ SAT backdoors: depth beats size ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the construction of graphs with a planar bipartite double cover from Boolean formulas and its application to counting satisfying solutions ⋮ An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances ⋮ Generating clause sequences of a CNF formula ⋮ On efficiently solvable cases of quantum \(k\)-SAT ⋮ Satisfiability of Acyclic and almost Acyclic CNF Formulas (II) ⋮ New width parameters for SAT and \#SAT ⋮ D-FLAT: Declarative problem solving using tree decompositions and answer-set programming ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Default logic and bounded treewidth ⋮ Parameterised complexity of model checking and satisfiability in propositional dependence logic ⋮ Unnamed Item ⋮ Definability for model counting ⋮ Backdoors to q-Horn ⋮ ProCount: weighted projected model counting with graded project-join trees

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of computing the permanent
• Hypertree decompositions and tractable queries
• A unified theory of structural tractability for constraint satisfaction problems
• Graph minors. X: Obstructions to tree-decomposition
• Treewidth. Computations and approximations
• Memory requirements for table computations in partial \(k\)-tree algorithms
• Conjunctive-query containment and constraint satisfaction
• Fixed-parameter complexity in AI and nonmonotonic reasoning
• Complexity of generalized satisfiability counting problems
• Linear time solvable optimization problems on graphs of bounded clique-width
• Solving \#SAT using vertex covers
• Counting truth assignments of formulas of bounded tree-width or clique-width
• Parametrized complexity theory.
• Fast multiplication of large numbers
• On the hardness of approximate reasoning
• Algorithms for Propositional Model Counting
• Constraint Satisfaction with Bounded Treewidth Revisited
• Constraint solving via fractional edge covers
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• SOFSEM 2005: Theory and Practice of Computer Science
• Finding Branch-Decompositions and Rank-Decompositions
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic

This page was built for publication: Algorithms for propositional model counting