Show simple item record

dc.contributor.authorArgelich Romà, Josep
dc.contributor.authorLi, Chu-Min
dc.contributor.authorManyà Serres, Felip
dc.contributor.authorPlanes Cid, Jordi
dc.date.accessioned2016-03-01T12:41:42Z
dc.date.available2016-03-01T12:41:42Z
dc.date.issued2011
dc.identifier.issn0302-9743
dc.identifier.urihttp://hdl.handle.net/10459.1/56665
dc.description.abstractThe MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: MaxSAT, Weighted MaxSAT (WMaxSAT), Partial MaxSAT (PMaxSAT), and Weighted Partial MaxSAT (WPMaxSAT). The objective of this paper is to analyze the instances of the 2010 MaxSAT Evaluation in order to gain new insights into their computational hardness, answer some questions that have been asked to us as organizers, and evaluate how appropriate are the current settings of parameters such as timeout and available RAM memory. To this end, we conducted a number of experiments, which were performed on a cluster with 160 2 GHz AMD Opteron 248 Processors with 1 GB of RAM memory. In the experiments, we considered the 2,675 instances of the 2010 MaxSAT Evaluation: 544 MaxSAT instances, 349 WMaxSAT instances, 1,122 PMaxSAT instances, and 660 WPMaxSAT instances. Instances were assigned to one of the following three categories: random, crafted and industrial. We used the 17 solvers that participated in MaxSAT-2010. They can be classified into three main types: branch and bound (B&B) solvers, satisfiability-based (sat-based) and unsatisfiability-based (unsat-based) solvers. In the first type, we find 10 solvers: akmaxsat, akmaxsat ls, IncMaxSatz, IncWMaxSatz, Maxsat Power, LS Power, WMaxsat Power, LSW Power, WMaxSatz-2009, and WMaxSatz+. In the second type, we find 2 solvers: SAT4J-Maxsat,and QMaxSAT. In the third type, we find 5 solvers: WPM1, PM2, WPM2, wbo 1.4a, and wbo 1.4b.ca_ES
dc.description.sponsorshipResearch supported by Generalitat de Catalunya (2009-SGR-1434), Ministerio de Ciencia e Innovación (CONSOLIDER CSD2007-0022, INGENIO 2010, Accion Integrada HA2008- ´ 0017, TIN2009-14704-C03-01, and TIN2010-20967-C04-01/03), and the Secretaría General de Universidades del Ministerio de Educacion: Programa Nacional de Movilidad de Recursos ´ Humanos.ca_ES
dc.language.isoengca_ES
dc.publisherSpringer Verlagca_ES
dc.relation.isformatofReproducció del document publicat a https://doi.org/10.1007/978-3-642-21581-0_29ca_ES
dc.relation.ispartofLecture Notes in Computer Science, 2011, vol. 6695, p. 360-361ca_ES
dc.rights(c) Springer Verlag, 2011ca_ES
dc.titleAnalyzing the instances of the MaxSAT evaluationca_ES
dc.typearticleca_ES
dc.identifier.idgrec017678
dc.type.versionacceptedVersionca_ES
dc.rights.accessRightsinfo:eu-repo/semantics/openAccessca_ES
dc.identifier.doihttps://doi.org/10.1007/978-3-642-21581-0_29


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record