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


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.


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:

Main Track (Sequential, CNF)
SolverSubmitterAffiliation #Solved
MiniSat Niklas Sörensson Sörensson R&D, Sweden 84
PrecoSATArmin BiereJKU Linz, Austria 84
rclJean-Marie LagniezCRIL-CNRS, France 84
SAT-PowerAbdorrahim BahramiU Isfahan, Iran84
BarcelogicAsín RobertoTU Catalonia, Spain 83
CryptoMiniSatMate SoosINRIA, France 83
LySATSaid JabbourINRIA - Microsoft JC, France 83
SATHYSJean-Marie LagniezCRIL-CNRS, France 82
CircleSATJingchao ChenDonghua U, China 81
glucosERGeorge KarsirelosCRIL-CNRS, France 81
kwJohan AlfredssonOepir, Sweden 81
glucoseGilles AudamardCRIL, France 80
lingelingArmin BiereJKU Linz, Austria 80
SApperloTStephan KottlerU Tübingen, Germany 80
oprailleurOlivier RousselCRIL-CNRS, France 77
borg-sat-10.04.30Bryan SilverthornU Texas, USA 76
rissNorbert MantheyTU Dresden, Germany 71
CirCUsHyojung HanU Boulder, USA 70
PicoSATArmin BiereJKU Linz, Austria 70

Special Track 1 (Parallel, CNF)
SolverSubmitterAffiliation #Solved
plingeling Armin Biere JKU Linz, Austria 93
ManySAT 1.1Said JabbourINRIA - Microsoft JC, France 90
ManySAT 1.5Said JabbourINRIA - Microsoft JC, France89
SArTagnanStephan KottlerU Tübingen, Germany 84
PMiniSatGeoffrey ChuNICTA, Australia 80
antomTobias SchubertU Freiburg, Germany 77

Special Track 2 (Sequential, AIG)
SolverSubmitterAffiliation #Solved
kw_aig Johan Alfredsson Oepir, Sweden 73
MiniSat++Niklas SörenssonSörensson R&D, Sweden 67
NFLSATHimanshu JainCMU, USA64