University of Limerick Institutional Repository

On efficient computation of variable MUSes

DSpace Repository

Show simple item record

dc.contributor.author Belov, Anton
dc.contributor.author Ivrii, Alexander
dc.contributor.author Matsliah, Arie
dc.contributor.author Marques-Silva, Joao
dc.date.accessioned 2012-12-20T12:33:43Z
dc.date.available 2012-12-20T12:33:43Z
dc.date.issued 2012
dc.identifier.uri http://hdl.handle.net/10344/2761
dc.description peer-reviewed en_US
dc.description.abstract In this paper we address the following problem: given an unsatisfiable CNF formula F, find a minimal subset of variables of F that constitutes the set of variables in some unsatisfiable core of F. This problem, known as variable MUS (VMUS) computation problem, captures the need to reduce the number of variables that appear in unsatisfiable cores. Previous work on computation of VMUSes proposed a number of algorithms for solving the problem. However, the proposed algorithms lack all of the important optimization techniques that have been recently developed in the context of (clausal) MUS computation. We show that these optimization techniques can be adopted for VMUS computation problem and result in multiple orders magnitude speed-ups on industrial application benchmarks. In addition, we demonstrate that in practice VMUSes can often be computed faster than MUSes, even when state-of-the-art optimizations are used in both contexts. en_US
dc.language.iso eng en_US
dc.publisher Springer-Verlag en_US
dc.relation.ispartofseries The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 298-311
dc.relation.uri http://dx.doi.org/10.1007/978-3-642-31612-8_23
dc.rights The original publication is available at www.springerlink.com en_US
dc.subject artificial intelligence en_US
dc.subject telecommunications en_US
dc.title On efficient computation of variable MUSes 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.contributor.sponsor FCT en_US
dc.relation.projectid BEACON (09/IN.I/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.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


Browse

My Account

Statistics