Questioning the Importance of WCORE-Like Minimization Steps in MUC-Finding Algorithms

When a constraint network is unsatisfiable, it can be of prime importance to provide the network designer with a full-fledged explanation of what causes the absence of any solution to the network. In this respect, minimal unsatisfiable cores (in short, MUCs) form the basis for such an explanation. Efficient MUC extractors are often made of an initial incomplete minimization step that delivers an upper-approximation of a MUC, followed by a refinement step. The first step is assumed crucial for the performance of the whole approach. In this paper, its actual importance is investigated. Especially, it is shown that the first step can be skipped when the refinement process dynamically exploits the information that this latter treatment itself entails.