Boosting a Complete Technique to Find MSS and MUS Thanks to a Local Search Oracle
Proceedings of the Twentieth International Joint Conference on Artificial Intelligence. Pages 2300-2304.
Abstract
In this paper, a new complete technique to compute Maximal Satisfiable Subsets (MSS) and Minimally Unsatisfiable Subformulas (MUS) of sets of Boolean clauses is introduced. The approach improves the currently most efficient complete technique in several ways. It makes use of the powerful concept of critical clause and of a computationally inexpensive local search oracle to boost an exhaustive algorithm proposed by Liffiton and Sakallah. These features can allow exponential efficiency gains to be obtained. Accordingly, experimental studies show that this new approach outperforms the best current existing exhaustive ones.
@inproceedings{ijcai2007p370,
title = {Boosting a Complete Technique to Find MSS and MUS Thanks to a Local Search Oracle},
author = {Grégoire, Éric and Mazure, Bertrand and Piette, Cédric},
booktitle = {Proceedings of the Twentieth International Joint Conference on
Artificial Intelligence, {IJCAI-07}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ramon López de Mántaras},
pages = {2300--2304},
year = {2007},
url = {https://ijcai.org/proceedings/2007/370},
}
TY - CPAPER TI - Boosting a Complete Technique to Find MSS and MUS Thanks to a Local Search Oracle AU - Grégoire, Éric AU - Mazure, Bertrand AU - Piette, Cédric T2 - Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI-07 PB - International Joint Conferences on Artificial Intelligence PY - 2007 SP - 2300 EP - 2304 UR - https://ijcai.org/proceedings/2007/370 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
