Max-SAT 2008

Third Max-SAT Evaluation

Rules

As in the previous evaluations, 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).

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.