An Explicit Semidefinite Characterization of Satisfiability for Tseitin Instances
This paper is concerned with the application of semidefinite programming to the satisfiability problem, and in particular with using semidefinite liftings to efficiently obtain proofs of unsatisfiability. We focus on the Tseitin satisfiability instances which are known to be hard for many proof systems. We present an explicit semidefinite programming problem with dimension linear in … Read more