18
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 3
    $\begingroup$ Planar max-cut is a special case of max-cut, which is (in a sense) a special case of max-2-sat. $\endgroup$
    – Jukka Suomela
    Jan 31, 2014 at 19:19

2 Answers 2

Reset to default
6
$\begingroup$

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

Szeider showed that Satisfiability is fixed-parameter tractable when parameterized by the treewidth of the incidence graph. Samer and Szeider gave an efficient dynamic programming algorithm.

References

S. Szeider. On fixed-parameter tractable parameterizations of SAT. In Proc. 6th International Conference on Theory and Applications of Satisfiability (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, Artificial 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 Satisfiability, part 1, chapter 13. IOS Press

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Martin Vatshelle
    Jan 31, 2014 at 20:22
0
$\begingroup$

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.

see:http://arxiv.org/abs/1402.6485

Are there any other such properties known?

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.