Analyzing the instances of the MaxSAT evaluation
MetadataShow full item record
The MaxSAT Evaluation  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.
Is part ofLecture Notes in Computer Science, 2011, vol. 6695, p. 360-361
European research projects
Showing items related by title, author, creator and subject.
Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (IOS Press, 2008)We describe the organization and report on the results of the First and Second Max-SAT Evaluations, which were organized as affiliated events of the 2006 and 2007 editions of the International Conference on Theory and ...
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Association for the Advancement of Artificial Intelligence, 2007)Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability ...
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2005)One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensure optimality, ...