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

Fingerprint

Semidefinite Optimization
Least Squares
Least Squares Problem
Farkas Lemma
Conjunctive Normal Form
Infeasibility
Linear Optimization
Demonstrations
Rendering
Assign
Strictly
Optimization Problem
Necessary
Zero

Keywords

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

Cite this

@article{9a945a5b90934ed889b04b17a7d3f29a,
title = "On semidefinite least squares and minimal unsatisfiability",
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.",
keywords = "Farkas’ Lemma, Minimal unsatisfiability, Satisfiability, Semidefinite least squares, Semidefinite programming",
author = "Anjos, {Miguel F.} and Vieira, {Manuel V C}",
note = "sem pdf conforme despacho. CMA/FCT/UNL - PEst-OE/MAT/U10297/2013.",
year = "2017",
month = "1",
day = "30",
doi = "10.1016/j.dam.2016.09.008",
language = "English",
volume = "217",
pages = "79--96",
journal = "Discrete Applied Mathematics",
issn = "0166-218X",
publisher = "Elsevier Science B.V., Inc",

}

On semidefinite least squares and minimal unsatisfiability. / Anjos, Miguel F.; Vieira, Manuel V C.

In: Discrete Applied Mathematics, Vol. 217, 30.01.2017, p. 79-96.

Research output: Contribution to journalArticle

TY - JOUR

T1 - On semidefinite least squares and minimal unsatisfiability

AU - Anjos, Miguel F.

AU - Vieira, Manuel V C

N1 - sem pdf conforme despacho. CMA/FCT/UNL - PEst-OE/MAT/U10297/2013.

PY - 2017/1/30

Y1 - 2017/1/30

N2 - 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.

AB - 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.

KW - Farkas’ Lemma

KW - Minimal unsatisfiability

KW - Satisfiability

KW - Semidefinite least squares

KW - Semidefinite programming

UR - http://www.scopus.com/inward/record.url?scp=84994501759&partnerID=8YFLogxK

U2 - 10.1016/j.dam.2016.09.008

DO - 10.1016/j.dam.2016.09.008

M3 - Article

VL - 217

SP - 79

EP - 96

JO - Discrete Applied Mathematics

JF - Discrete Applied Mathematics

SN - 0166-218X

ER -