Universitat de Lleida
    • English
    • català
    • español
  • English 
    • English
    • català
    • español
  • Login
Repositori Obert UdL
View Item 
  •   Home
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • View Item
  •   Home
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Analyzing the instances of the MaxSAT evaluation

Thumbnail
View/Open
Postprint (21.19Kb)
Issue date
2011
Author
Argelich Romà, Josep
Li, Chu-Min
Manyà Serres, Felip
Planes Cid, Jordi
Suggested citation
Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi; . (2011) . Analyzing the instances of the MaxSAT evaluation. Lecture Notes in Computer Science, 2011, vol. 6695, p. 360-361. https://doi.org/10.1007/978-3-642-21581-0_29.
Impact


Web of Science logo    citations in Web of Science

Scopus logo    citations in Scopus

Google Scholar logo  Google Scholar
Share
Export to Mendeley
Metadata
Show full item record
Abstract
The 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.
URI
http://hdl.handle.net/10459.1/56665
DOI
https://doi.org/10.1007/978-3-642-21581-0_29
Is part of
Lecture Notes in Computer Science, 2011, vol. 6695, p. 360-361
European research projects
Collections
  • Articles publicats (Informàtica i Enginyeria Industrial) [990]

Contact Us | Send Feedback | Legal Notice
© 2023 BiD. Universitat de Lleida
Metadata subjected to 
 

 

Browse

All of the repositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

Statistics

View Usage Statistics

D'interès

Política institucional d'accés obertDiposita les teves publicacionsDiposita dades de recercaSuport a la recerca

Contact Us | Send Feedback | Legal Notice
© 2023 BiD. Universitat de Lleida
Metadata subjected to