New width parameters for SAT and #SAT

摘要

We study the parameterized complexity of the prepositional satisfiability (SAT) and the more general model counting (#SAT) problems and obtain novel fixed-parameter algorithms that exploit the structural properties of input formulas. In the first part of the paper, we parameterize by the treewidth of the following two graphs associated with CNF formulas: the consensus graph and the conflict graph. Both graphs have as vertices the clauses of the formula; in the consensus graph two clauses are adjacent if they do not contain a complementary pair of literals, while in the conflict graph two clauses are adjacent if they do contain a complementary pair of literals. We show that #SAT is fixed-parameter tractable when parameterized by the treewidth of the former graph, but SAT is W[1]-hard when parameterized by the treewidth of the latter graph. In the second part of the paper, we turn our attention to a novel structural parameter we call h-modularity which is loosely inspired by the well-established notion of community structure. 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 them for an efficient solution of SAT and #SAT, respectively.