Efficient Combination of Decision Procedures for MUS Computation

In recent years, the problem of extracting a MUS (Minimal Unsatisfiable Subformula) from an unsatisfiable CNF has received much attention. Indeed, when a Boolean formula is proved unsatisfiable, it does not necessarily mean that all its clauses take part to the inconsistency; a small subset of them can be conflicting and make the whole set without any solution. Localizing a MUS can thus be extremely valuable, since it enables to circumscribe a minimal set of constraints that represents a cause for the infeasibility of the CNF. In this paper, we introduce a novel, original framework for computing a MUS. Whereas most of the existing approaches are based on complete algorithms, we propose an approach that makes use of both local and complete searches. Our combination is empirically evaluated against the current best techniques on a large set of benchmarks.

• Type: Conference
• Year: 2009
• Where: FROCOS
• Authors: Cédric Piette, Youssef Hamadi, Lakhdar Sais
• Keywords: Boolean Formula, Control Systems, FROCOS 2009, Minimal Unsatisfiable Subformula, Small Subset