Title: Towards an SDP-based Algorithm for the Satisfiability Problem

The satisfiability (SAT) problem is a central problem in mathematical logic, computing theory, and artificial intelligence. We consider instances of SAT specified by a set of boolean variables and a propositional formula in conjunctive normal form. Given such an instance, the SAT problem asks whether there is a truth assignment to the variables such that the formula is satisfied. It is well known that SAT is in general NP-complete, although several important special cases can be solved in polynomial time.
Extending the work of de Klerk, Warners and van Maaren, we present new semidefinite programming (SDP) relaxations arising from the recently introduced paradigm of higher semidefinite liftings for discrete optimization problems. These relaxations yield truth assignments satisfying the SAT instance if a feasible matrix of sufficiently low rank is computed. The sufficient rank values differ between relaxations and can be viewed as a measure of the relative strength of each relaxation. The new SDP relaxations also have the ability to prove that a given SAT formula is unsatisfiable. Computational results on instances from the recent SAT Competition 2003 show that the SDP approach has the potential to complement existing techniques for SAT.