You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

An Extended Semidefinite Relaxation for Satisfiability

Article type: Research Article

Authors: Anjos, Miguel F.; *

Affiliations: Department of Management Sciences, Faculty of Engineering, University of Waterloo, Waterloo, Ontario, Canada N2L 3G1. E-mail: [email protected]

Note: [*] Research supported by a Discovery Grant from the Natural Sciences and Engineering Research Council of Canada.

Keywords: satisfiability, semidefinite programming, discrete optimization, global optimization

DOI: 10.3233/SAT190036

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 1, pp. 15-31, 2008

Received 1 August 2007
|
Revision received 1 December 2007
|
Published: 1 December 2007
Get PDF open access

Abstract

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.

Show more