# Polynomial time solvable instances of Max-Sat

The problem Max-Sat ask you to find an assignment of a CNF formula which satisfy as many clauses as possible.

For the simpler problem SAT there are many known special cases which can be solved in polynomial time, e.g. we can solve 2-SAT in polynomial time.

For Max-Sat the situation is different since Max-Sat is NP-hard even for 2-CNF formulas (each clause contains only 2 variables).

Is there any interesting special inputs for which Max-Sat is polynomial?

In particular I would be interested in a standard reference for solving Max-Sat when the incedence graph has bounded treewidth.

• Planar max-cut is a special case of max-cut, which is (in a sense) a special case of max-2-sat. – Jukka Suomela Jan 31 '14 at 19:19

This does not answer directly your Max-SAT problem but the references may guide you to the complete answer.

Szeider showed that Satisfiability is ﬁxed-parameter tractable when parameterized by the treewidth of the incidence graph. Samer and Szeider gave an eﬃcient dynamic programming algorithm.

References

S. Szeider. On ﬁxed-parameter tractable parameterizations of SAT. In Proc. 6th International Conference on Theory and Applications of Satisﬁability (SAT’03), Selected and Revised Papers, vol. 2919 of LNCS, pages 188–202. Springer-Verlag, 2004.

M. Samer and S. Szeider. Algorithms for propositional model counting. In Proc. 14th Internationial Conference on Logic for Programming, Artiﬁcial Intelligence and Reasoning (LPAR’07), vol. 4790 of LNCS, pages 484–498. Springer-Verlag, 2007.

Samer and Szeider, Fixed-parameter tractability. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisﬁability, part 1, chapter 13. IOS Press

• I know some of Stefan Szeiders work, a more recent paper shows that #SAT is polynomial when the incedence graph has bounded clique-width which also imlies bounded tree-width (although here we have XP runtime instead of FPT). Friedrich Slivovsky and Stefan Szeider, Model Counting for Formulas of Bounded Clique-Width, Algorithms and Computation, vol. 8283,p. 677-687, LNCS,2013 I know that these type of results often would translate into MAX-SAT, but it would be much easier have a reference where this is already done instead of doing it myself. – Martin Vatshelle Jan 31 '14 at 20:22

We found one kind of such property:

For a formula $F$ , 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. Then we can solve MAX-SAT in polynomial time.

Are there any other such properties known?