Organized in conjunction with the

Eighth International Conference on
Theory and Applications of Satisfiability Testing

June 19th-23rd 2005, St Andrews, Scotland

Last update: July 21, 2005

July 21: Concerning the competition results ...

February 14: Solver and benchmark registration now open! Register now! (Until February 23).

While the I/O requirements and the input format are basically the same since the 2002 competition, conditions to enter the competitions are changing a bit (see for instance the anti-black-box rule last year).

20/01/05: Check out the new rules in details

New this year:

Special track on certified unsat answers

As a side event of the competition, we are organizing a special track on certified unsat answers. Solvers able to certify an unsat answer will compete on some of the unsat benchmarks solved during the competition. Allen Van Gelder proposed an unsat proof format together with a proof checker. Both the unsat proof format and the checker are now available.

Special track for non-clausal problems

Toby Walsh and Fahiem Bacchus are collecting non-clausal examples using an extended Dimacs format for arbitrary logical gates. The final input specification is now available and some examples are also available.

Special track for pseudo-boolean contraints

Vasco Manquinho and Olivier Roussel are organizing a special track for solvers able to manage pseudo-boolean constraints. All the details are available on their web site.

Benchmark booklet?

A 2-pages description of each competitor was available in the 2004 edition. We are thinking about asking for a 2-pages description of the benchmarks too.

Binary version of the solvers?

In order to go further ahead in our requirements in favor to the research community, we are thinking about asking for an authorization to have freely available binary versions of the competing solvers for researchers.
We are trying to have rules similar to the CASC competition tailored for the specificities of the SAT community. One of the basic idea is that everything submitted to the SAT competition should be available to the research community once the competition is over. The judges are helping us to finalize the new rules. Please contact the organizers if you feel they may affect your participation to the competition.

More to come ...

This web page will be updated regularly. Major updates will be announced on SAT Live!

Submission information will be available one month before the deadline.

For further information, please send an email to

Important Date:

Solver and Benchmark Submissions:      February 23, 2005
Special tracks submissions:                     March     23, 2005


Daniel Le Berre, Université d'Artois
Laurent Simon, Université Paris-Sud


Armin Biere, ETH Zürich/ Johannes Kepler University in Linz
Oliver Kullmann, Swansea University
Allen Van Gelder, University of California at Santa Cruz

Last update: 22/9/2005