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 linearly sized semidefinite programming (SDP)
relaxations arising from a 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 SDP relaxations also have the
ability to prove that a given SAT formula is unsatisfiable. Computational
results on hard instances from the SAT Competition 2003 show that the SDP
approach has the potential to complement existing techniques for SAT.