First stage results

The first stage began on March 19 and ended on April 14. One of the new features of the SAT2003 competition was the ability for each competitor to follow his solver via a web page that was updated daily. All the traces were available, and suspicious launchs, detected by us or by the competitors, were reran.

Some solvers did reply UNSAT on proved SAT benchmarks. It is the only case where a solver is not correct: for SAT answers, we ask for a certificate. If the certificate is correct, then the benchmark is proved to be SAT. There is no such proof for UNSAT benchmarks. Furthermore, benchmarks are submitted SAT, UNSAT or UNKNOWN. A solver is not considered incorrect if it answers UNSAT on a claimed SAT benchmark.

The following two solvers were found incorrect during the first stage:

compsat

The solver is using restarts and the version submitted did not clear the unit clauses stack after restart. A one line missing bug...

marchxq

The following tables summarize the results of all solvers for each category.

A table which focus on sat 2002 challenging instances [25] (instances not solved during the first stage of the sat2002 competition) is also provided for each category.