Solving MaxSAT and #SAT on structured CNF formulas

ABSTRACT. In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted {\sc MaxSAT} and {\sc \#SAT} that can be solved in polynomial time. Given a CNF formula we say that a set of clauses is precisely satisfiable if there is some complete assignment satisfying these clauses only. Let the $\mathtt{ps}$-value of the formula be the number of precisely satisfiable sets of clauses. Applying the notion of branch decompositions to CNF formulas and using $\mathtt{ps}$-value as cut function, we define the $\mathtt{ps}$-width of a formula. For a formula given with a decomposition of polynomial $\mathtt{ps}$-width we show dynamic programming algorithms solving weighted {\sc MaxSAT} and {\sc \#SAT} in polynomial time. Combining with results of 'Belmonte and Vatshelle, Graph classes with structured neighborhoods and algorithmic applications, {\sc Theor. Comput. Sci.} 511: 54-65 (2013)' we get polynomial-time algorithms solving weighted {\sc MaxSAT} and {\sc \#SAT} for some classes of structured CNF formulas. For example, we get $\bigoh(n^4)$ algorithms for formulas having a linear ordering of variables and clauses such that for any variable $x$ occurring in clause $C$, if $x$ appears before $C$ then any variable between them also occurs in $C$, and if $C$ appears before $x$ then $x$ occurs also in any clause between them. Note that the class of incidence graphs of such formulas do not have bounded clique-width.