Qualification

Each registered solver will have to successfully participate in a qualification round in order to be accredited for SAT-Race.

Requirements

We check the following requirements:

• Conformance to I/O specification. Solvers have to respect the I/O requirements (CNF, AIG). In particular, for CNF-based solvers, the output must contain a solution line (starting with "s ") and—in case of a satisfiable instance—at least one values line (starting with "v "). Exit codes also must be set correctly (10 for satisfiable, 20 for unsatisfiable, 0 for unknown).
• Correctness of results. The solvers are not allowed to produce wrong answers (e.g. 'satisfiable' for an unsatisfiable instance, but of course they may time-out).
• Sufficient performance. Solvers must meet some minimal speed requirements.

Cheating (e.g. pre-computing results) is, of course, not allowed. We will check all solvers on additional instances, and fraudulent solvers will be disqualified.

The final decision which solvers are allowed to participate in SAT-Race will be made by the organizing committee.

Dates

The dead-line for submitting a solver to the qualification round is April 30.

Results of the Qualification Round

The qualification round has taken place on and after April 30. Each solver had to tackle 100 instances. The run-time limit was set to 15 minutes per solver and instance. Solvers which were able to solve at least 70 instances (Main Track and Special Track I) or 50 instances (Special Track II) are qualified for SAT-Race 2010. These solvers are: