Analyzing the instances of the MaxSAT evaluation

View/ Open
Issue date
2011Suggested 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.
Metadata
Show full item recordAbstract
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.