On semidefinite least squares and minimal unsatisfiability

Miguel F. Anjos, Manuel V C Vieira

Research output: Contribution to journalArticle

Abstract

This paper provides new results on the application of semidefinite optimization to satisfiability by studying the connection between semidefinite optimization and minimal unsatisfiability. We use a semidefinite least squares problem to assign weights to the clauses of a propositional formula in conjunctive normal form. We then show that these weights are a measure of the necessity of each clause in rendering the formula unsatisfiable, the weight of a necessary clause is strictly greater than the weight of any unnecessary clause. In particular, we show the following results: first, if a formula is minimal unsatisfiable, then all of its clauses have the same weight; second, if a clause does not belong to any minimal unsatisfiable subformula, then its weight is zero. An additional contribution of this paper is a demonstration of how the infeasibility of a semidefinite optimization problem can be tested using a semidefinite least squares problem by extending an earlier result for linear optimization. The connection between the semidefinite least squares problem and Farkas’ Lemma for semidefinite optimization is also discussed.

Original languageEnglish
Pages (from-to)79-96
Number of pages18
JournalDiscrete Applied Mathematics
Volume217
DOIs
Publication statusPublished - 30 Jan 2017

Keywords

  • Farkas’ Lemma
  • Minimal unsatisfiability
  • Satisfiability
  • Semidefinite least squares
  • Semidefinite programming

Fingerprint Dive into the research topics of 'On semidefinite least squares and minimal unsatisfiability'. Together they form a unique fingerprint.

  • Cite this