next up previous
Next: Conclusions Up: Difficulties and future competitions Previous: Some lessons

About the next competition

Because any of the SOTA contributors is important for SAT research, we are thinking about delivering a SOTA contributor certificate for the next competition. But, to adopt the SOTA system for awarding solvers, we need a better classification of available SAT benchmarks as in TPTP. Let us emphasize some differences between the CASC competition (where SOTA ranking is the rule) and the SAT2002 competition. Differences are essentially due to the different level of maturity of these competitions:

  1. In the CASC competition, most instances are part of the TPTP library, so they are well known and classified. This is not the case for the SAT competition since we received a lot of completely new benchmarks for running the competition.
  2. The ranking proposed above is made on Specialist Problem Classes, whose granularity is finer than our simple (Industrial, Handmade, Randomly generated) partition (for instance, the pigeon-hole problem may occur as an industrial problem... How can we classify such a benchmark?).
  3. We used a heuristic to save CPU time, so not all systems were run on all instances.

Many other improvements are possible for the next competition. Still it seems like human action is unavoidable. To make it more fair and less time-consuming for the organizers, we propose to appoint a board of judges similarly to CASC. When the competition rules do not give an explicit answer, it is up to the judges to decide what to do. They can also play a role for instance in the partition of benchmarks.

For the future competitions we propose the following:

Some other points, more or less prospective, are possible:

The final point is to run the next competition only before the SAT Symposium (only publishing results and giving awards at the meeting)...


next up previous
Next: Conclusions Up: Difficulties and future competitions Previous: Some lessons
LE BERRE Daniel 2002-09-16