On semidefinite least squares and minimal unsatisfiability
| Autor: | Manuel V. C. Vieira, Miguel F. Anjos |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Discrete mathematics
Semidefinite embedding Semidefinite programming Quadratically constrained quadratic program Optimization problem Applied Mathematics Mathematics::Optimization and Control 0102 computer and information sciences 02 engineering and technology Computer Science::Artificial Intelligence Computer Science::Computational Complexity 01 natural sciences Satisfiability Combinatorics Propositional formula 010201 computation theory & mathematics Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Discrete Mathematics and Combinatorics 020201 artificial intelligence & image processing Conjunctive normal form Farkas' lemma Mathematics |
| Zdroj: | Anjos, M F & Vieira, M V C 2017, ' On semidefinite least squares and minimal unsatisfiability ', Discrete Applied Mathematics, vol. 217, pp. 79-96 . https://doi.org/10.1016/j.dam.2016.09.008 |
| ISSN: | 0166-218X |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect