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!

• Poster (pdf).
• Presentation (pdf).
• Benchmarks
• Max-SAT (tgz).
• Weigthed Max-SAT (tgz).
• Partial Max-SAT (tgz).
• Weigthed Partial Max-SAT (tgz).

Important dates

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:

• Max-SAT category: The input formula will be a CNF formula.
• Weigthed Max-SAT category: The input formula will be a CNF formula in which each clause has a weight.
• Partial Max-SAT category: The input formula will be a CNF formula with hard and soft clauses.
• Weigthed Partial Max-SAT category: The input formula will be a CNF formula with hard and weigthed soft clauses.

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 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 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:

• Operating System: Rocks Cluster 4.0.0 Linux 2.6.9
• Processor: AMD Opteron 248 Processor, 2 GHz
• Memory: 1 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, University of Lleida, Spain
Jordi Planes, University of Lleida, Spain

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