SAT2004 Competition: Call for Solvers

SAT Competition 2004

February - May, 2004

Last modification: January 30 2004.

Changes compared to the previous competition rules are highlighted in green

A new SAT competition is going to start on February 2004 and continue until May 2004. The results of the competition will be given at the SAT 2004 conference (May 10-13, 2004, Vancouver, Canada). That competition follows the SAT Competition 2002 that ran during the SAT 2002 Symposium (May 6-9, 2002, Cincinatti, Ohio, USA) and the SAT Competition 2003 that ran during the SAT 2003 conference (May 5-8, 2003, S. Margherita Ligure - Portofino, Italy).


Who can submit?

Everyone except Laurent Simon.

What can be submitted?

Any program that solves (some) instances of the Boolean satisfiability problem. I.e., a complete or incomplete, deterministic or randomized SAT solver. The program must confirm the requirements concerning input/output format. The submission will be either in source compilable using the make command or as a precompiled binary on one of the competition computer. In order to avoid running blackboxes during the competition, we do require a technical report explaining in details the underlying principles of the solver (or a reference to a published work). If that information is not available at the moment of the solver submission, the authors are asked to submit it within one month after the solver deadline submission. A solver without description (a so called blackbox) will automatically be discarded from the competition. Another way for a solver to be elligible to the competition is to provide a public access to its source code.

There are no restrictions concerning whether this solver is new or old, published or not, took part in other competitions or not. Note that up to three variants (same algorithm, same authors, different parameters) of the same solver can be submitted to the competition but only the best one will be considered for the qualification to the final stage. The solvers awarded at the previous competition will be automatically submitted to the competition in their awarding category.

How to submit?

Go to the submission page!

Laurent Simon and Daniel Le Berre (and possibly system administrators: this is unavoidable!) will be the only person who will have an access to the solvers.

What are the benchmarks?

The solvers will be run on benchmarks chosen from the pool of submitted benchmarks plus the pool of benchmarks remained unsolved during the previous SAT competition. The solvers will run on each original benchmark plus two shuffled versions of that benchmark: The variables and the clauses will be permuted randomly (but in the same way for all solvers). There will be three categories of benchmarks: random uniform k-SAT, crafted and application (see Call for Benchmarks for their description). Each of the categories will be split into several series of similar benchmarks.

How the competition will proceed?

Unlike previous competitions, there won't be any input/output compliance stage this year. Solvers not compliant with the competition input/output framework will simply be excluded from the competition. A set of tools is available to allow you to check that your solver is compliant with our input/output requirement.

We will first run each solver on each applicable benchmark (i.e., we will not run incomplete solvers on the benchmarks known to be unsatisfiable); smaller benchmarks come earlier. If a solver does not answer within time limit (to be determined when we know the number of submissions), it is interrupted. Randomized solvers will be started only one time, but the time out will be given as an environment variable and as a parameter. Thus, submitters of randomized solvers are able to restart their solver as many times they want, but within the same time limit as non randomized solvers.

For the next stage of the competition the competition judges select top N solvers (determined from the first stage by the same method as will be used for determining the winners after the second stage, considering only the best variant of a given solver) in each of the 6 categories and run them on the M smallest unsolved benchmarks (again, separately in each category), smaller benchmarks come earlier. The number of solvers and benchmarks selected in each category may vary.

Who are the winners?

There will be three categories of solvers: the ones able to answer SAT, the ones able to answer UNSAT, and the ones able to answer SAT and UNSAT. (Clearly, a complete solver can take part in the competition in the three categories). There will be also three categories of benchmarks. Thus, there will be a total of 3*3=9 winners, the same amount of second place winners etc.

All solvers that fall within 1 sec. * number of benchmarks of the winner are also declared winners.

However, if a solver solves no (zero) benchmarks for given category, it cannot be declared a winner under any circumstances. Furthermore, if the winner in a category was already awarded for that category in the previous competition, then there will be no award given for that category.

What are the awards?

A beautiful certificate, unless some people are willing to provide prizes to motivate the competition (then please contact the organizers).

Winners in each categories will be invited to submit a detailled description of their solver to a journal (to be defined yet) quickly after the end of the competition. For people not willing to do so, the technical report or the source code that was submitted together with the solver will be made available on the competition web site.

Important dates

Organizing Committee

Laurent Simon ( and Daniel Le Berre (


Competition homepage

[SAT Competition 2004] [ SAT 2004 Conference ] [ SAT-Ex] [ SATLIB] [ SAT Live!]