University of Limerick Institutional Repository

MaxSAT-based MCS enumeration

DSpace Repository

Show simple item record Morgado, Antonio Liffiton, Mark Marques-Silva, Joao 2013-02-19T12:46:01Z 2013-02-19T12:46:01Z 2012
dc.description peer-reviewed en_US
dc.description.abstract Enumeration of Minimal Correction Sets (MCS) finds a wide range of practical applications, including the identification of Minimal Unsatisfiable Subsets (MUS) used in verifying the complex control logic of microprocessor designs (e.g. in the CEGAR loop of RevealTM [1,2]). Current state of the art MCS enumeration exploits core-guided MaxSAT algorithms, namely the so-called MSU3 [16] MaxSAT algorithm. Observe that a MaxSAT solution corresponds to a minimum sized MCS, but a formula may contain MCSes larger than those reported by a MaxSAT solution. These are obtained by enumerating all MaxSAT solutions. This paper proposes novel approaches for MCS enumeration, in the context of SMT, that exploit MaxSAT algorithms other than the MSU3 algorithm. Among other contributions, the paper proposes new blocking techniques that can be applied to different MCS enumeration algorithms. In addition, the paper conducts a comprehensive experimental evaluation of MCS enumeration algorithms, including both the existing and the novel algorithms. Problem instances from hardware verification, the SMT-LIB, and the MaxSAT Evaluation are considered in the experiments. en_US
dc.language.iso eng en_US
dc.relation.ispartofseries Eighth Haifa Verification Conference (HVC 2012);
dc.subject AllMaxSAT en_US
dc.subject AllMaxSMT en_US
dc.subject mcs en_US
dc.title MaxSAT-based MCS enumeration en_US
dc.type info:eu-repo/semantics/conferenceObject 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.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