First Evaluation of Max-SAT Solvers (MaxSAT-2006)

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

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.

Evaluation Results New!

• Report (coming soon)
• Poster (pdf)
• Presentation (pdf)
• Benchmarks (tgz)

Important dates

Benchmarks and Solvers

In the first evaluation we will focus the attention on exact solvers. We plan to allow non-exact solvers in future evaluations.

There will be two categories:

• Max-SAT category: The input formula will be a CNF formula without repeated clauses.
• Weigthed Max-SAT category: The input formula will be a CNF formula in which each clause has a weight.

Benchmark instances should be submitted in DIMACS CNF format and weighted CNF format (see details), and submitted solvers should be able to read that format (see details). Submissions should be sent by e-mail to maxsat06@iiia.csic.es.

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.

Experimentation

Only one version of the same solver will be accepted for each category. For each instance and solver there will be a time limit between 15 and 30 minutes, depending on the number of submitted solvers. 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:

• Operating System: Rocks Cluster 4.0.0 Linux 2.6.9
• Processor: AMD Opteron 248 Processor, 2 GHz
• Memory: 2 GB
• Cache: 1024 KB
• Compilers: GCC 3.4.3, javac JDK 1.5.0

Organizing Committee

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

To reach the organizers, send an e-mail to maxsat06@iiia.csic.es.