Call for Solvers

SAT Competition 2002

March 10 - May 8, 2002

NEW DEALINE for benchmark submission: 24 MARCH

SAT Competition 2002 is going to start on March 10, 2002 and continue until (and during) SAT 2002 Symposium (May 6-9, 2002, Cincinatti, Ohio, USA).


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. It must be submitted in source compilable by typing "make" under standard Linux/UNIX environment. There are no restrictions concerning whether this solver is new or old, published or not, took part in other competitions or not.

How to submit?

Go to the submission page!

Laurent Simon (and possibly system administrators: this is unavoidable!) will be the only person who will have an access to solver sources and compiled programs. The sources will not be published and will be removed from the competition computers after the competition finishes.

What are the benchmarks?

The solvers will be run on benchmarks chosen from the pool of submitted benchmarks plus the pool of "good old benchmarks", the variables and the clauses will be permuted randomly (but in the same way for all solvers). (During the testing stage, solvers may also be run on other benchmarks.) There will be three categories of benchmarks: randomly generated, handmade and industrial (see Call for Benchmarks for their description). Each of the categories will be split into several series of similar benchmarks scaling from smaller to larger instances.

How the competition will proceed?

Before the actual competition starts, the solvers will be tested for bugs. Buggy solvers will be then returned to their authors who will take their chances to fix the bugs. After possible re-submission, the solvers are checked again, the still-buggy solvers are excluded, and the actual competition starts. (While if a solver is found buggy even at a later stage, it is excluded anyway.)

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 and will not be run against larger benchmarks of the same series. Randomized solvers will be started several times and the median time will be taken into account ("time limit" is charged for the unsuccessful tries); it is not run against larger benchmarks if it failed in all its tries on a smaller benchmark.

For the next stage of the competition we 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) in each of the 6 categories and run them on the M smallest unsolved benchmarks (again, separately in each category), smaller benchmarks come earlier. We suppose N=M=4 now, but Laurent may change it right after the deadline if the number of benchmarks and/or solvers and/or our computers will be far from what we predict. Clearly, at this stage the time limit will be substantially larger.

Who are the winners?

There will be two categories of solvers: complete ones and incomplete ones. (Clearly, a complete solver can take part in the competition in both categories). There will be also three categories of benchmarks. Thus, there will be a total of 2*3=6 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.

What are the awards?

To motivate participation an award of US Dollar 2500 (provided by the computational logic group at Delft) will be allocated to a selection of solvers and benchmarks. Namely, an award of $300 will be given to each winning complete solver and each winning incomplete solver in each category (total of 2*3=6 awards). Only first place winners will be awarded. The allocation of the remaining money is described in the Call for Benchmarks.

If a category has strictly less than three groups authoring solvers (those ones that were not found buggy or were successfully fixed), the award is not given and its pieces will be added to the awards for other categories.

Important dates

Competition homepage

[SAT Competition 2002] [SAT 2002] [SAT-Ex] [SATLIB] [SAT Live!]