R. Ganian, S. Szeider:

"Community Structure Inspired Algorithms for SAT and #SAT";

Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Austin, Texas; 2015-09-24 - 2015-09-27; in: "Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing", LNCS / Springer, 9340 (2015), ISBN: 978-3-319-24317-7; 223 - 238.

We introduce h-modularity, a structural parameter of CNF

formulas, and present algorithms that render the decision problem SAT

and the model counting problem #SAT fixed-parameter tractable when

parameterized by h-modularity. The new parameter is defined in terms

of a partition of clauses of the given CNF formula into strongly interconnected

communities which are sparsely interconnected with each other.

Each community forms a hitting formula, whereas the interconnections

between communities form a graph of small treewidth. Our algorithms

first identify the community structure and then use it for an efficient solution

of SAT and #SAT, respectively. We further show that h-modularity

is incomparable with known parameters under which SAT or #SAT is

fixed-parameter tractable.

http://publik.tuwien.ac.at/files/PubDat_247925.pdf

Created from the Publication Database of the Vienna University of Technology.