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.