Solving #SAT using vertex covers |
| |
Authors: | Naomi Nishimura Prabhakar Ragde Stefan Szeider |
| |
Affiliation: | 1. School of Computer Science, University of Waterloo, Waterloo, ON, N2L 3G1, Canada 2. Department of Computer Science, Durham University, Durham, DH1 3LE, UK
|
| |
Abstract: | We propose an exact algorithm for counting the models of propositional formulas in conjunctive normal form. Our algorithm is based on the detection of strong backdoor sets of bounded size; each instantiation of the variables of a strong backdoor set puts the given formula into a class of formulas for which models can be counted in polynomial time. For the backdoor set detection we utilize an efficient vertex cover algorithm applied to a certain “obstruction graph” that we associate with the given formula. This approach gives rise to a new hardness index for formulas, the clustering-width. Our algorithm runs in uniform polynomial time on formulas with bounded clustering-width. It is known that the number of models of formulas with bounded clique-width, bounded treewidth, or bounded branchwidth can be computed in polynomial time; these graph parameters are applied to formulas via certain (hyper)graphs associated with formulas. We show that clustering-width and the other parameters mentioned are incomparable: there are formulas with bounded clustering-width and arbitrarily large clique-width, treewidth, and branchwidth. Conversely, there are formulas with arbitrarily large clustering-width and bounded clique-width, treewidth, and branchwidth. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|