Contributions to Proceedings:
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,
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-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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.