Improving MUC extraction thanks to local search
This work addresses the challenge of efficiently identifying unsatisfiability causes in constraint networks for re-engineering, but it is incremental as it builds on existing MUC-finding approaches.
The paper tackled the problem of extracting Minimal Unsatisfiable Cores (MUCs) from constraint networks to understand causes of unsatisfiability, and the result was that using local search to find additional transition constraints outperformed a model rotation technique and boosted state-of-the-art MUC extractors.
ExtractingMUCs(MinimalUnsatisfiableCores)fromanunsatisfiable constraint network is a useful process when causes of unsatisfiability must be understood so that the network can be re-engineered and relaxed to become sat- isfiable. Despite bad worst-case computational complexity results, various MUC- finding approaches that appear tractable for many real-life instances have been proposed. Many of them are based on the successive identification of so-called transition constraints. In this respect, we show how local search can be used to possibly extract additional transition constraints at each main iteration step. The approach is shown to outperform a technique based on a form of model rotation imported from the SAT-related technology and that also exhibits additional transi- tion constraints. Our extensive computational experimentations show that this en- hancement also boosts the performance of state-of-the-art DC(WCORE)-like MUC extractors.