[Back]

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; 09-24-2015 - 09-27-2015; 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