On exact selection of minimally unsatisfiable subformulae |
| |
Authors: | Renato Bruni |
| |
Affiliation: | (1) Dipartimento di Informatica e Sistemistica, Università; di Roma La Sapienza , Via Buonarroti 12, 00185 Roma, Italy |
| |
Abstract: | A minimally unsatisfiable subformula (MUS) is a subset of clauses of a given CNF formula which is unsatisfiable but becomes satisfiable as soon as any of its clauses is removed. The selection of a MUS is of great relevance in many practical applications. This expecially holds when the propositional formula encoding the application is required to have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). While selection of a MUS is a hard problem in general, we show classes of formulae where this problem can be solved efficiently. This is done by using a variant of Farkas lemma and solving a linear programming problem. Successful results on real-world contradiction detection problems are presented. |
| |
Keywords: | infeasibility analysis MUS selection (Un)Satisfiability |
本文献已被 SpringerLink 等数据库收录! |