Using local search to find MSSes and MUSes

Éric Grégoire, Bertrand Mazure and Cédric Piette

European Journal of Operational Research, 2009, vol. 199, issue 3, 640-646

Abstract: In this paper, a new complete technique to compute Maximal Satisfiable Subsets (MSSes) and Minimally Unsatisfiable Subformulas (MUSes) 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.

Keywords: SAT; MSSes; MUSes; Satisfiability; Hybrid; algorithm (search for similar items in EconPapers)
Date: 2009
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://www.sciencedirect.com/science/article/pii/S0377-2217(08)00361-5
Full text for ScienceDirect subscribers only

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:eee:ejores:v:199:y:2009:i:3:p:640-646

Access Statistics for this article

European Journal of Operational Research is currently edited by Roman Slowinski, Jesus Artalejo, Jean-Charles. Billaut, Robert Dyson and Lorenzo Peccati

More articles in European Journal of Operational Research from Elsevier
Bibliographic data for series maintained by Catherine Liu ().