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

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

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

• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• 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
• 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 Structure and Function of Complex Networks
• The complexity of valued constraint satisfaction problems
• The fractal dimension of SAT formulas
• Theory and Applications of Satisfiability Testing
• Treewidth. Computations and approximations

Cited in

(7)

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

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)