Model Counting for Formulas of Bounded Clique-Width

TL;DR

This paper proves that counting solutions (#SAT) for certain CNF formulas is efficiently solvable when their incidence graphs have bounded symmetric clique-width, extending previous tractability results to more general classes.

Contribution

It establishes polynomial-time algorithms for #SAT on formulas with incidence graphs of bounded symmetric clique-width, generalizing prior results based on modular treewidth and signed clique-width.

Findings

#SAT is polynomial-time solvable for formulas with bounded symmetric clique-width.

This generalizes previous tractability results for formulas with bounded clique-width or modular treewidth.

The result broadens the class of formulas for which #SAT can be efficiently computed.

Abstract

We show that #SAT is polynomial-time tractable for classes of CNF formulas whose incidence graphs have bounded symmetric clique-width (or bounded clique-width, or bounded rank-width). This result strictly generalizes polynomial-time tractability results for classes of formulas with signed incidence graphs of bounded clique-width and classes of formulas with incidence graphs of bounded modular treewidth, which were the most general results of this kind known so far.