# Solving MaxSAT and #SAT on structured CNF formulas

arXiv: https://arxiv.org/abs/1402.6485 · HTML: https://mlsanity.com/paper/1402.6485/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Feb 2014.

## Built on by (most cited first, 1 of 1)

- [A canonical generalization of OBDD](https://mlsanity.com/paper/2604.05537/) (2026)

## Abstract (arXiv)

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(m2(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.