Sums of Squares, Satisfiability and Maximum Satisfiability

Hans van Maaren (joint work with Linda van Norden)

Recently the Mathematical Programming community showed a renewed interest in Hilbert's Positivstellensatz. The reason for this is that global optimization of polynomials in R[x1, ...,xn] is NP-hard, while the question whether a polynomial can be written as a sum of squares has tractable aspects. This is due to the fact that Semidefinite Programming can be used to decide in polynomial time whether a polynomial can be rewritten as a sum of squares of linear combinations of monomials coming from a specified set. We investigate this approach in the context of Satisfiability: To a given CNF formula a polynomial can be associated which global minimum exactly determines how many clauses can be maximally satisfied. Thus an approximation of this minimum gives an approximation of the so called max-sat solution to this formula. We examine the potential of the theory for providing tests for unsatisfiability and providing max-sat upper bounds. We compare the SOS (Sums Of Squares) approach with existing upper bound techniques (for the max 2-sat case) of Goemans and Williamson and Feige and Goemans, which are based on Semidefinite Programming as well. We advocate that the SOS approach gives more accurate upper bounds.

A short introduction to Satisfiability theory and testing (and its applications) will be given first.

back to TU/e Combinatorial Theory Seminar announcements