On semidefinite least squares and minimal unsatisfiability

详细信息    查看全文

• 作者：Miguel F. Anjos^a ; ^{anjos@stanfordalumni.org} ; Manuel V.C. Vieira^b ; ^{mvcv@fct.unl.pt}
• 关键词：Semidefinite programming ; Satisfiability ; Minimal unsatisfiability ; Farkas&rsquo ; Lemma ; Semidefinite least squares
• 刊名：Discrete Applied Mathematics
• 出版年：2017
• 出版时间：30 January 2017
• 年：2017
• 卷：217
• 期：part_P2
• 页码：79-96
• 全文大小：502 K
• 卷排序：217

文摘

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.