Solving MaxSAT and #SAT on structured CNF formulas

TL;DR

This paper introduces a new structural parameter called ps-width for CNF formulas, enabling polynomial-time algorithms for weighted MaxSAT and #SAT on formulas with bounded ps-width, expanding tractable classes.

Contribution

The paper defines ps-width based on precisely satisfiable clause sets and develops dynamic programming algorithms for formulas with bounded ps-width, extending tractability results to new structured CNF classes.

Findings

Polynomial-time algorithms for weighted MaxSAT and #SAT on formulas with bounded ps-width.

Identification of a new class of structured CNF formulas solvable efficiently.

Extension of previous graph class results to formulas with specific variable-clause orderings.

Abstract

In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted MaxSAT and #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 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 ps-value as cut function, we define the ps-width of a formula. For a formula given with a decomposition of polynomial ps-width we show dynamic programming algorithms solving weighted MaxSAT and #SAT in polynomial time. Combining with results of 'Belmonte and Vatshelle, Graph classes with structured neighborhoods and algorithmic applications, Theor. Comput. Sci. 511: 54-65 (2013)' we get polynomial-time algorithms solving weighted MaxSAT and #SAT for some classes of structured CNF formulas. For example, we get $O(m^2(m + n)s)$ algorithms for formulas $F$ of $m$ clauses and $n$ variables and size $s$, if $F$ has a linear ordering of the 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.