New width parameters for SAT and #SAT

摘要

We study the parameterized complexity of the propositional 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.