Improving MUC extraction thanks to local search

TL;DR

This paper introduces a local search method to improve the extraction of Minimal Unsatisfiable Cores (MUCs) from constraint networks, outperforming existing techniques and enhancing state-of-the-art MUC extractors.

Contribution

The paper presents a novel local search approach that enhances MUC extraction by identifying additional transition constraints, improving performance over existing methods.

Findings

Local search can extract more transition constraints per iteration.

The approach outperforms model rotation techniques in experiments.

Enhanced methods boost the performance of state-of-the-art MUC extractors.

Abstract

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.