Miguel F. Anjos Assistant Professor
Department of Management Sciences
University of Waterloo, Canada

Recent Progress in Applying Semidefinite Optimization to the Satisfiability Problem

Semidefinite optimization, commonly referred to as semidefinite programming, is currently one of the most active areas of research in optimization and has attracted researchers from a variety of areas because of its theoretical power, algorithmic elegance and wide applicability. Semidefinite programming refers to the class of optimization problems where a linear function of a symmetric matrix variable is maximized (or minimized) subject to linear constraints on the elements of the matrix, and the additional constraint that the matrix be positive semidefinite. We present new semidefinite optimization relaxations for the satisfiability problem. These relaxations arise from a recently introduced paradigm of higher semidefinite liftings for discrete optimization problems. Theoretical and computational results show that these relaxations have a number of favourable properties, particularly as a means to prove that a given formula is unsatisfiable, and that this approach compares favourably with existing techniques for satisfiability.

See: http://cheetah.vlsi.uwaterloo.ca/~anjos/homepage.html