University of Limerick Institutional Repository

Towards efficient MUS extraction

DSpace Repository

Show simple item record Belov, Anton Lynce, Inês Marques-Silva, Joao 2013-01-10T15:15:04Z 2013-01-10T15:15:04Z 2012
dc.description peer-reviewed en_US
dc.description.abstract Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find application in recent Maximum Satisfiability algorithms and in CNF formula redundancy removal. Besides direct applications in Propositional Logic, algorithms for MUS extraction have been applied to more expressive logics. This paper proposes two algorithms for MUS extraction. The first algorithm is optimal in its class, meaning that it requires the smallest number of calls to a SAT solver. The second algorithm extends earlier work, but implements a number of new techniques. Among these, this paper analyzes in detail the technique of recursive model rotation, which provides significant performance gains in practice. Experimental results, obtained on representative practical benchmarks, indicate that the new algorithms achieve significant performance gains with respect to state of the art MUS extraction algorithms. en_US
dc.language.iso eng en_US
dc.publisher IOS Press en_US
dc.relation.ispartofseries AI Communications;25(2), pp. 97-116
dc.rights Reprinted from AI Communications, 25(2) pp. 97-116, Towards Efficient MUS Extraction, Benlov, Anton, Lynce Inês and Marques-Silva, Joao. Copyright (2012), with permission from IOS Press en_US
dc.subject Boolean satisfiability en_US
dc.subject minimally unstatisfiable subformula en_US
dc.title Towards efficient MUS extraction en_US
dc.type info:eu-repo/semantics/article en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor SFI en_US
dc.contributor.sponsor FCT en_US
dc.contributor.sponsor INESC-ID en_US
dc.relation.projectid BEACON 09/IN.1/I2618 en_US
dc.relation.projectid ATTEST CMU-PT/ELE/0009/2009 en_US
dc.relation.projectid POLARIS PTDC /EIA-CCO/123051/2010 en_US
dc.relation.projectid ASPEN PTDC/EIA-CC0/110921/2009 en_US
dc.relation.projectid PIDDAC en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account