Results

This page presents the results of SAT-Race 2008. The winners in the three tracks (Main, Special 1, Special 2) are:

TrackFirst PlaceSecond PlaceThird Place
Main Track (CNF sequential)MiniSat 2.1pMiniSatBarcelogic
Special Track 1 (CNF parallel)ManySatpMiniSatMiraXT
Special Track 2 (AIG sequential)MiniSat++ 1.0picoaigersatMiniCirc

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.

MiniSat 2.1pMiniSat*BarcelogicRsatMXCpreSATCMUSATkwpicosatEureka
#solved:81797776747272707069
#solved SAT/UNSAT:43/3839/4035/4236/4040/3438/3440/3232/3840/3029/40
rank by solved:12345668810
speed points:7.265.615.105.044.794.734.725.195.165.44
rank by speed:12678910453
total score:88.2684.6182.1081.0478.7976.7376.7275.1975.1674.44
rank:12345678910

ManySat*LocalMinisatMiraXT*SATzillaeSATSpearTinisatclaspSAT4J
#solved:686463606060565449
#solved SAT/UNSAT:30/3832/3237/2630/3029/3130/3028/2823/3126/23
rank by solved:111213141414171819
speed points:3.993.684.264.183.813.323.083.192.43
rank by speed:131511121416181719
total score:71.9967.6867.2664.1863.8163.3259.0857.1951.43
rank:111213141516171819

*Note: pMiniSat, ManySat and MiraXT are parallel solvers, which were run in sequential mode.

Detailed results including runtimes for all solvers and instances can be viewed in HTML or downloaded in MS-Excel format.

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.

ManySatpMiniSatMiraXT
#solved:908573
#solved SAT/UNSAT:45/4544/4143/30
#solved in all runs:798466
#solved in ≤900s CPU time:697253
rank:123

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.

MiniSat++pico-aigersatMiniCircCMUSAT-AIGkw_aigerNFLSAT
#solved:746970706260
#solved SAT/UNSAT:31/4333/3628/4233/3726/3630/30
rank by solved:142256
speed points:12.9813.8012.2911.859.189.34
rank by speed:213465
total score:86.9882.8092.2981.8571.1869.34
rank:123456

Detailed results including runtimes for all solvers and instances can be viewed in HTML or downloaded in MS-Excel format.