Publication details
New Width Parameters for Model Counting
| Authors | |
|---|---|
| Year of publication | 2017 |
| Type | Article in Proceedings |
| Conference | Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings |
| MU Faculty or unit | |
| Citation | |
| web | https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3#citeas |
| Doi | http://dx.doi.org/10.1007/978-3-319-66263-3_3 |
| Keywords | Treewidth; Model Counting; SAT; Parameterized Complexity |
| Description | 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. |