abstract:

Extending the work of de Klerk, Warners and van Maaren, we present a new
semidefinite programming (SDP) relaxation for the satisfiability (SAT)  
problem. The SDP relaxation is a ``partial'' lifting motivated by the
Lasserre hierarchy of SDP relaxations for discrete optimization problems.  
The relaxation yields truth assignments satisfying the SAT instance if a
feasible matrix of sufficiently low rank is computed, and it also has the
ability to prove that a given SAT formula is unsatisfiable. Computational
results on hard instances show that the SDP approach has the potential to
complement existing techniques for SAT.

********************************************************************
Dr Miguel F. Anjos -- Lecturer in Operational Research
School of Mathematics, University of Southampton
http://www.maths.soton.ac.uk/staff/Anjos