Exact Selection of Minimal Unsatisfiable Subformulae for Special Classes of Propositional Formulae

A minimal unsatisfiable subformula (MUS) of a given propositional formula is a subset of clauses which is unsatisfiable, but becomes satisfiable as soon as we remove any of its clauses. In several applicative fields, a relevant problem besides solving the satisfiability problem, is to detect a minimal unsatisfiable subformula. This is expecially true when the application is encoded into a propositional formula which should 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 for which such individuation can be performed efficiently.