Second Evaluation of Max-SAT Solvers (MaxSAT-2007)

The Second Evaluation of Max-SAT Solvers (MaxSAT-2007) is organized as an affiliated event of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-2007).

The objective of the evaluation is assessing the state of the art in the field of Max-SAT solvers, as well as creating a collection of publicly available Max-SAT benchmark instances.

JSAT will publish a special issue on the SAT 2007 competitions and evaluations.

Evaluation Results New!

Important dates

Submission of benchmarksFebruary 20th, 2007
First submission of solversFebruary 20th, 2007
Testing and bug fixingMarch 1st-31st, 2007
Submission of definitive solversApril 1st, 2007
ExperimentationApril-May, 2007
Results of the evaluationMay 28th-31st, 2007

Benchmarks and Solvers

As in the first evaluation, we will focus the attention on exact solvers. Solvers requiring a commercial software license will not be considered.

There will be four categories:

Benchmark instances should be submitted in an extended DIMACS CNF format (see details), and submitted solvers should be able to read that format (see details). Submissions should be sent by e-mail to

Benchmarks should be submitted in a tar.gz file along with a short description of the instances. Instances used in the evaluation will be selected among the instances submitted, and will not be published in advance.

In the first submission of solvers, you should send a description of the solver and the affiliation of the authors, but not the solver itself. A few days after the submission, you will receive a sample of the submitted instances that will allow you to test your solver and fix possible bugs.

In the submission of definitive solvers, you should send an executable, statically linked, version of your solver.


Only one version of the same solver will be accepted for each category. For each instance and solver there will be a time limit of 30 minutes. Assessment of solvers will be based on the number of successfully solved instances and the time needed to solve them.

Solvers will run on machines with the following specification:

Organizing Committee

Josep Argelich, University of Lleida, Spain
Chu Min Li, University of Picardie, France
Felip Manya, University of Lleida, Spain
Jordi Planes, University of Lleida, Spain

To reach the organizers, send an e-mail to