Sums of squares based approximation algorithms for MAX-SAT

We investigate the Semidefinite Programming based Sums of squares (SOS) decomposition method, designed for global optimization of polynomials, in the context of the (Maximum) Satisfiability problem. To be specific, we examine the potential of this theory for providing tests for unsatisfiability and providing MAX-SAT upper bounds. We compare the SOS approach with existing upper bound and rounding techniques for the MAX-2-SAT case of Goemans and Williamson [12] and Feige and Goemans [10] and the MAX-3-SAT case of Karloff and Zwick [14], which are based on Semidefinite Programming as well. We prove that for each of these algorithms there is a SOS-based counterpart which provides upper bounds at least as tight, but observably tighter in particular cases. Also, we propose a new randomized rounding technique based on the optimal solution of the SOS Semidefinite Program which we experimentally compare with the appropriate existing rounding techniques. Further we investigate the implications ...

• Type: Journal
• Year: 2008
• Where: DAM
• Authors: Hans van Maaren, Linda van Norden, M. J. H. Heule
• Keywords: DAM 2008, Rounding Techniques, Semidefinite Programming, Upper Bounds