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