Model counting for CNF formulas of bounded modular treewidth

DOI10.1007/s00453-015-0030-xzbMath1353.68137OpenAlexW2309930662MaRDI QIDQ334935

Daniël Paulusma, Stefan Szeider, Friedrich Slivovsky

Publication date: 1 November 2016

Published in: Algorithmica (Search for Journal in Brave)

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2013/3922/

zbMATH Keywords

algorithmspropositional satisfiabilitymodel counting

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (11)

Sum-of-Products with Default Values: Algorithms and Complexity Results ⋮ The use of a pruned modular decomposition for \textsc{maximum matching} algorithms on some graph classes ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Finer Tight Bounds for Coloring on Clique-Width ⋮ On efficiently solvable cases of quantum \(k\)-SAT ⋮ Counting linear extensions: parameterizations by treewidth ⋮ New width parameters for SAT and \#SAT ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability of acyclic and almost acyclic CNF formulas
• A survey of the algorithmic aspects of modular decomposition
• The complexity of computing the permanent
• Graph minors. X: Obstructions to tree-decomposition
• Treewidth. Computations and approximations
• The monadic second-order logic of graphs. XIV: Uniformly sparse graphs and edge set quantifica\-tions.
• On the parameterized complexity of the fixed alphabet shortest common supersequence and longest common subsequence problems
• Linear time solvable optimization problems on graphs of bounded clique-width
• Upper bounds to the clique width of graphs
• Algorithms for propositional model counting
• Handle-rewriting hypergraph grammars
• Counting truth assignments of formulas of bounded tree-width or clique-width
• Approximating clique-width and branch-width
• On the hardness of approximate reasoning
• Hypergraphs in Model Checking: Acyclicity and Hypertree-Width versus Clique-Width
• Homomorphic Hashing for Sparse Coefficient Extraction
• Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width
• Theory and Applications of Satisfiability Testing
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic

This page was built for publication: Model counting for CNF formulas of bounded modular treewidth