This is a draft version of the Call For Participation
to the SAT2003 competition. Last modification: September 25, 2002.

A new SAT competition is going to start on February 2003 and continue until May 2003. The results of the competition will be given at the SAT 2003 conference (Italy). That competition follows the SAT Competition 2002 started on March 10, 2002 and continued until (and during) SAT 2002 Symposium (May 6-9, 2002, Cincinatti, Ohio, USA).

- Who can submit?
- What can be submitted?
- How to submit?
- What are the benchmarks?
- How the competition will proceed?
- Who are the winners?
- What are the
**awards**? - Important dates
- Competition homepage

*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.*

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 . Randomized solvers will be started several times and the median time will be taken into account ("time limit" is charged for the unsuccessful tries).

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, 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. 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.

A special session with a time limit given for solving a sequence of benchmarks
may be organized, depending on the number of people willing to participate
to that session, and provided that we get a satisfying automated framework
to do it.

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.

- For a given category, a winning solver is determined by the total number of "hard" (second stage) benchmarks it was able to solve. If this figure is the same for several solvers, then we look into the first stage results.
- First, the total number of solved series of benchmarks is counted
(we count here series as "solved" if
*at least*one benchmark is solved). - If this figure is the same again, then the total number of solved benchmarks is counted.
- If even this figure is the same, the total elapsed CPU time is counted.

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.

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

- February, 14: deadline for submitting solvers.
- February, 21 (UPDATED): deadline for submitting benchmarks.
- February, 28: buggy solvers returned to the authors.
- March, 7: buggy solvers resubmitted.
- March, 14: 1st stage of the competition starts.
- April, 14 (or earlier): 2nd stage of the competition starts.
- May: results during SAT2003 conference, awards.

Contact: SATcompetition@satlive.org

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