[Zurück]

R. Ganian, S. Szeider:
"New Width Parameters for Model Counting";
in: "Theory and Applications of Satisfiability Testing - SAT 2017", International Conference on Theory and Applications of Satisfiability Testing, 2017, ISBN: 978-3-319-66262-6, S. 38 - 52.

We study the parameterized complexity of the propositional model counting problem #SAT for CNF formulas. As the parameter we consider 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 for the treewidth of the consensus graph but W[1]-hard for the treewidth of the conflict graph. We also compare the new parameters with known parameters under which #SAT is fixed-parameter tractable.

Supported by the Austrian Science Fund (FWF), project P26696. Robert Ganian is also affiliated with FI MU, Brno, Czech Republic.

http://dx.doi.org/10.1007/978-3-319-66263-3_3

https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3