Does this set of clauses overlap with at least one MUS ?

International audienceThis paper is concerned with the problem of checking whether a given subset Γ of an unsatisfiable Boolean CNF formula Σ takes part in the basic causes of the inconsistency of Σ . More precisely, an original approach is intro- duced to check whether Γ overlaps with at least one minimally unsatisfiable sub- set (MUS) of Σ . In the positive case, it intends to compute and deliver one such MUS. The approach re-expresses the problem within an evolving coarser-grained framework where clusters of clauses of Σ are formed and examined according to their levels of mutual conflicts when they are interpreted as basic interacting enti- ties. It then progressively refines the framework and the solution by splitting most promising clusters and pruning the useless ones until either some maximal pre- set computational resources are exhausted, or a final solution is discovered. The viability and the usefulness of the approach are illustrated through benchmarks experimentations