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. We show that using the relaxation, a proof of the unsatisfiability of the notorious pigeonhole and mutilated chessboard problems can be computed in polynomial time. As a byproduct we find a new ‘sandwich' theorem that is similar to the sandwich theorem for Lovasz' V-function. Furthermore, the semidefinite relaxation gives a certificate of (un)satisfiability for 2SAT problems in polynomial time. 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 with some empirical observations.