This page presents the results of SAT-Race 2008. The winners in the three tracks (Main, Special 1, Special 2) are:
The prize for the best student solver goes to pMiniSat.
Detailed results on each track are given below.
Main Track (CNF sequential)
The table below shows the number of instances solved by each SAT solver (out of 100 instances in total; also split up into successfully processed SAT and UNSAT instances); the rank according to number of solved instances; number of speed-points assigned to solver (see the Rules page for a description of speed-points); the rank according to speed-points; the total score; and the final ranking based on the total score. The time-out for each solver and each instance was 900 seconds.
*Note: pMiniSat, ManySat and MiraXT are parallel solvers, which were run in sequential mode.
We have also run the best three solvers of 2007's SAT-Competition (Industrial Track, SAT+UNSAT Category) on the 100 instances of SAT-Race 2008. The results are available in both HTML and MS-Excel format.
Special Track 1 (CNF parallel)
In the parallel track, each solver could use four cores (two Dual-Core Intel Xeon CPUs). As runtimes are highly deviating for parallel SAT solvers, each solver was run three times on each instance. An instances was considered solved, if it could be solved in at least one of the three runs of a solver.
The table below gives the number of solved instances (also separated by SAT and UNSAT instances), as well as the number of instances that could be solved in all three runs, and the number of instances that could be solved in less than 900 seconds of CPU time.
Detailed results including runtimes for all solvers and instances can be viewed in HTML or downloaded in MS-Excel format. The runtimes in these tables are median wall-clock times avaraged over all successful runs. Additionally, for each instance and solver, the number of successful runs (between 0 and 3) is given.
Special Track 2 (AIG sequential)
The table below summarizes the results of the AIG track. The reported numbers have the same interpretation as in the Main Track.