Finding minimal unsatisfiable subformulae in satisfiability instances

A minimal unsatisfiable subformula (MUS) of a given CNF is a set of clauses which is unsatisfiable, but becomes satisfiable as soon as we remove any of its clauses. In practical scenarios it is often useful to know, in addition to the unsolvability of an instance, which parts of the instance cause the unsolvability. An approach is here proposed to the problem of automatic detection of such a subformula, with the double aim of finding quickly a small-sized one. We make use of an adaptive technique in order to rapidly select an unsatisfiable subformula which is a good approximation of a MUS. Hard unsatisfiable instances can be reduced to remarkably smaller problems, and hence efficiently solved, through this approach.