University of Limerick Institutional Repository

Improvements to core-guided binary search for MaxSAT

DSpace Repository

Show simple item record

dc.contributor.author Morgado, Antonio
dc.contributor.author Heras, Federico
dc.contributor.author Marques-Silva, Joao
dc.date.accessioned 2013-01-02T15:32:51Z
dc.date.available 2013-01-02T15:32:51Z
dc.date.issued 2012
dc.identifier.uri http://hdl.handle.net/10344/2771
dc.description peer-reviewed en_US
dc.description.abstract Maximum Satisfiability (MaxSAT) and its weighted variants are wellknown optimization formulations of Boolean Satisfiability (SAT). Motivated by practical applications, recent years have seen the development of core-guided algorithms for MaxSAT. Among these, core-guided binary search with disjoint cores (BCD) represents a recent robust solution. This paper identifies a number of inefficiencies in the original BCD algorithm, related with the computation of lower and upper bounds during the execution of the algorithm, and develops solutions for them. In addition, the paper proposes two additional novel techniques, which can be implemented on top of core-guided MaxSAT algorithms that maintain both lower and upper bounds. Experimental results, obtained on representative problem instances, indicate that the proposed optimizations yield significant performance gains, and allow solving more problem instances. en_US
dc.language.iso eng en_US
dc.publisher Springer 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. 284-297
dc.relation.uri http://dx.doi.org/10.1007/978-3-642-31612-8_22
dc.rights The original publication is available at www.springerlink.com en_US
dc.subject MaxSAT en_US
dc.subject algorithms en_US
dc.subject software engineering en_US
dc.title Improvements to core-guided binary search for MaxSAT en_US
dc.type info:eu-repo/semantics/lecture 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.1/I2618) en_US
dc.relation.projectid ATTEST (CMU-PT/ELE/0009/2009) en_US
dc.relation.projectid POLARIS (PTDC/EIA-CC0/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