Solving #SAT Using Vertex CoversActa Informatica, vol. 44, no. 7-8, pp. 509-523, 2007. A preliminary version appeared in the Proceedings of SAT 2006, Ninth International Conference on Theory and Applications of Satisfiability Testing, August 12-15, 2006, Seattle, Washington, USA, Lecture Notes in Computer Science 4121, pp. 396—409, 2006. Download: [paper ps] [paper pdf] Abstract:We propose an exact algorithm for counting the models of propositional formulas in conjunctive normal form (CNF). 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. [back to Stefan Szeider's homepage] |