### 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 language | English |
---|---|

Pages (from-to) | 79-96 |

Number of pages | 18 |

Journal | Discrete Applied Mathematics |

Volume | 217 |

DOIs | |

Publication status | Published - 30 Jan 2017 |

### Fingerprint

### Keywords

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

### Cite this

*Discrete Applied Mathematics*,

*217*, 79-96. https://doi.org/10.1016/j.dam.2016.09.008

}

*Discrete Applied Mathematics*, vol. 217, pp. 79-96. https://doi.org/10.1016/j.dam.2016.09.008

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

Research output: Contribution to journal › Article

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 -