Algorithms for propositional model counting

DOI10.1016/j.jda.2009.06.002zbMath1214.05166MaRDI 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 satisfiability; parameterized algorithms; model counting

Mathematics Subject Classification ID

05C85: Graph algorithms (graph-theoretic aspects)

Related Items

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

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