An Extended Semidefinite Relaxation for Satisfiability
Miguel F. Anjos · Journal on Satisfiability Boolean Modeling and Computation · 2007
This paper proposes a new semidefinite programming relaxation for the satisfiability problem.This relaxation is an extension of previous relaxations arising from the paradigm of partial semidefinite liftings for 0/1 optimization problems.The construction of the relaxation depends on a choice of permutations of the clauses, and different choices may lead to different relaxations.We then consider the Tseitin instances, a class of instances known to be hard for certain proof systems, and prove that for any choice of permutations, the proposed relaxation is exact for these instances, meaning that a Tseitin instance is unsatisfiable if and only if the corresponding semidefinite programming relaxation is infeasible.