An Explicit Semidefinite Characterization of Satisfiability for Tseitin Instances
Miguel F. Anjos (anjosstanfordalumni.org)
Abstract: 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 the size of the Tseitin instance, and prove that it characterizes the satisfiability of these instances, thus providing an explicit certificate of satisfiability or unsatisfiability in polynomial-time.
Keywords: Satisfiability problem, Semidefinite Programming, Combinatorial Optimization, Discrete Optimization, Global Optimization
Category 1: Linear, Cone and Semidefinite Programming (Semi-definite Programming )
Category 2: Integer Programming (0-1 Programming )
Category 3: Applications -- Science and Engineering (Basic Sciences Applications )
Citation: Annals of Mathematics and Artificial Intelligence, Vol. 47 (3-4), 2006, 1-14.
Entry Submitted: 05/28/2005
Modify/Update this entry
|Visitors||Authors||More about us||Links|
Search, Browse the Repository
Give us feedback
|Optimization Journals, Sites, Societies|