The satisfiability (SAT) problem is a central problem in mathematical logic, computing theory, and artificial intelligence. An instance of SAT is 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. Semidefinite programming (SDP) refers to the class of optimization problems where a linear function of a matrix variable X is maximized (or minimized) subject to linear constraints on the elements of X and the additional constraint that X be positive semidefinite. We are interested in the application of SDP to satisfiability problems, and in particular in how SDP can be used to detect unsatisfiability. In this paper we introduce a new SDP relaxation for the satisfiability problem. This SDP relaxation arises from the recently introduced paradigm of ``higher liftings'' for constructing semidefinite programming relaxations of discrete optimization problems. To derive the SDP relaxation, we first formulate SAT as an optimization problem involving matrices. Relaxing this formulation yields an SDP which significantly improves on the previous relaxations in the literature. The important characteristics of the SDP relaxation are its ability to prove that a given SAT formula is unsatisfiable independently of the lengths of the clauses in the formula, its potential to yield truth assignments satisfying the SAT instance and the fact that it is more amenable to practical computation than previous SDPs arising from higher liftings. We present theoretical and computational results that support these claims.
Citation
Mathematical Programming 102 (3), 2005, 589-608.