Community structure inspired algorithms for SAT and \#SAT

DOI10.1007/978-3-319-24318-4_17MaRDI QIDQ3453228zbMATH OpenOpenAlexFDO

Authors Robert Ganian, Stefan Szeider

Publication date 20 November 2015

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

Full work available at URL https://doi.org/10.1007/978-3-319-24318-4_17

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Parameterized complexity, tractability and kernelization (68Q27) Computational aspects of satisfiability (68R07) Graph theory (including graph drawing) in computer science (68R10) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Nonnumerical algorithms (68W05)

Recommendations

• New width parameters for SAT and \#SAT
• The community structure of SAT formulas
• Community structure in industrial SAT instances
• On the hardness of SAT with community structure
• Model counting for CNF formulas of bounded modular treewidth

Cites work

• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• Algorithms for propositional model counting
• Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width
• CNF-Satisfiability Test by Counting and Polynomial Average Time
• Community structure in social and biological networks
• Graph minors. II. Algorithmic aspects of tree-width
• Graph theory
• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• Impact of Community Structure on SAT Solver Performance
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On simple characterizations of k-trees
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic
• On the structure of some classes of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Satisfiable formulas closed under replacement
• Solving \#SAT and Bayesian inference with backtracking search
• Solving \#SAT using vertex covers
• The complexity of valued constraint satisfaction problems
• The fractal dimension of SAT formulas
• The Structure and Function of Complex Networks
• Theory and Applications of Satisfiability Testing
• Treewidth. Computations and approximations

Cited in

(7)

• The complexity landscape of decompositional parameters for ILP
• New width parameters for SAT and \#SAT
• On the hardness of SAT with community structure
• Generating SAT instances with community structure
• Impact of Community Structure on SAT Solver Performance
• Community-Based Partitioning for MaxSAT Solving
• Backdoor DNFs

Describes a project that uses

Uses Software

• JBool

This page was built for publication: Community structure inspired algorithms for SAT and \#SAT

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