Groupe d’études et de recherche en analyse des décisions


On semidefinite least squares and minimum unsatisfiable subformulas


This paper provides new results on the application of semidefinite optimization to satisfiability by studying the connection between semidefinite optimization and minimal unsatisfiable subformulas. We use a semidefinite least squares problem to assign weights to the clauses of a propositional formula. We then show that these weights are a measure of the importance of each clause in rendering the formula unsatisfiable. In particular, we show that this approach identifies two important cases: first, if an unsatisfiable formula is a minimal unsatisfiable subformula, 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. The results in this paper establish the basis for a semidefinite optimization-based algorithm to identify minimal unsatisfiable subformulas within a given formula. 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.

, 22 pages