Local-search Extraction of MUSes |
| |
Authors: | Éric Grégoire Bertrand Mazure Cédric Piette |
| |
Affiliation: | (1) CRIL-CNRS & IRCICA, Université d’Artois, rue Jean Souvraz SP18, F-62307 Lens Cedex, France |
| |
Abstract: | SAT is probably one of the most-studied constraint satisfaction problems. In this paper, a new hybrid technique based on local
search is introduced in order to approximate and extract minimally unsatisfiable subformulas (in short, MUSes) of unsatisfiable
SAT instances. It is based on an original counting heuristic grafted to a local search algorithm, which explores the neighborhood
of the current interpretation in an original manner, making use of a critical clause concept. Intuitively, a critical clause
is a falsified clause that becomes true thanks to a local search flip only when some other clauses become false at the same time. In the paper, the critical clause concept is investigated. It is shown to be the cornerstone of the efficiency
of our approach, which outperforms competing ones to compute MUSes, inconsistent covers and sets of MUSes, most of the time. |
| |
Keywords: | SAT Local search Minimally unsatisfiable subformulas |
本文献已被 SpringerLink 等数据库收录! |
|