Relaxations of the satisfiability problem using semidefinite programming
We derive a semidefinite relaxation of the satisfiability (SAT) problem and discuss its strength. We give both the primal and dual formulation of the relaxation. The primal formulation is an eigenvalue optimization problem, while the dual formulation is a semidefinite feasibility problem. It is shown that using the relaxation, the notorious pigeon hole and mutilated chessboard problems are solved in polynomial time. As a byproduct we find a new `sandwich' theorem that is similar to Lov'asz' famous $vartheta$-function. Furthermore, using the semidefinite relaxation 2SAT problems are solved. By adding an objective function to the dual formulation, a specific class of polynomially solvable 3SAT instances can be identified. We conclude with discussing how the relaxation can be used to solve more general SAT problems and some empirical observations.
|ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY (acm F.2), DISCRETE MATHEMATICS (acm G.2)|
|Classical propositional logic (msc 03B05), Mathematical programming methods (msc 65K05), Theorem proving (deduction, resolution, etc.) (msc 68T15), Problem solving (heuristics, search strategies, etc.) (msc 68T20), Combinatorial optimization (msc 90C27), Nonlinear programming (msc 90C30)|
|Software Engineering [SEN]|
de Klerk, E, van Maaren, H, & Warners, J.P. (1999). Relaxations of the satisfiability problem using semidefinite programming. Software Engineering [SEN]. CWI.