Next: Competition steps
Up: The rules
Previous: Input and output formats
Let us notice a tricky
consideration about buggy solvers. If SAT was claimed on a
satisfiable instance, but the certificate was not correct, then
unknown (and not buggy) was assumed as an
answer. Each SAT result is thus certified, and we did not consider as
buggy a solver that gave a wrong certificate (this can be
due for instance to a CPUs exceed while printing the certificate or to
a data structure problem if the certificate is displayed on a single
line). As a matter of fact, we only considered as ``buggy'' all
solvers that answered incorrectly, UNSAT on a SAT instance
(previously known SAT or proved by any other solver during the
competition).
In addition, solvers are by essence incomplete, because of memory
and CPU limitation. Thus, if a solver crashed during the competition
(which can be due or not to bugs), we did not consider it as
buggy. We only considered that its answer was
``unknown''.
Each time a buggy solver was found, it was tagged
hors-concours and discarded from the awards (results were
still available ``unofficially'').
Next: Competition steps
Up: The rules
Previous: Input and output formats
LE BERRE Daniel
2002-09-16