Results

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

TrackFirst PlaceSecond PlaceThird Place
Main Track (CNF sequential)CryptoMiniSatlingelingSAT-Power
Special Track 1 (CNF parallel)plingelingManySAT 1.5ManySAT 1.1
Special Track 2 (AIG sequential)MiniSat++ 1.1kw_aigNFLSAT

The prize for the best student solver goes to SAT-Power in the Main Track and to SArTagnan in Special Track 1 (CNF parallel).

Click on a solver's name to get a description of that solver.

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 [25 SAT, 65 UNSAT, 10 unknown]; also split up into successfully processed SAT and UNSAT instances); the avarage time (CPU time) per solved instance in seconds; and the final ranking based on the nubmer of solved instances, using the average solving time to break ties. The time-out for each solver and each instance was 900 seconds.

CryptoMiniSatlingelingSAT-PowerPrecoSATMiniSatBarcelogicLySATrclborg-satCircleSAT
#solved:74737169676766656565
#solved SAT/UNSAT:20/5421/5218/5317/5219/4817/5016/5018/4717/4818/47
average time per solved instance:138.3111.4147.697.086.4167.5143.9109.7127.9139.5
rank:12345678910

ManySAT 1.1*SApperloTantom*PicoSATglucoseSATHYSManySAT 1.5*glucosERrissorpailleur
#solved:65646463636362625858
#solved SAT/UNSAT:18/4717/4719/4517/4614/4919/4416/4613/4915/4310/48
average time per solved instance:160.695.8121.485.2127.7131.5128.2137.793.6107.9
rank:11121314151617181920

*Note: ManySAT 1.1, ManySAT 1.5 and antom are parallel solvers, which were run in sequential mode.

Detailed results including runtimes for all solvers and instances can be viewed in HTML.

Special Track 1 (CNF parallel)

In the parallel track, each solver could use eight cores (two Quad-Core Intel Xeon CPUs running at 2.66 GHz). As runtimes can be 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 the first run.

The table below gives the number of solved instances in the first run (also separated by SAT and UNSAT instances), the avarage time (wallclock time) per solved instance in seconds; the number of solved instances in the second and third run; and the number of instances that could be solved in at least one of the three runs.

plingelingManySAT 1.5ManySAT 1.1SArTagnanantom
#solved (in 1st run):7875727067
#solved SAT/UNSAT (in first run):23/5519/5618/5418/5219/48
average time per solved instance:97.7143.9124.086.583.1
#solved in 2nd run:7974737065
#solved in 3rd run:7974717268
#solved in at least one out of three runs:8078767669
rank:12345

Detailed results including runtimes for all solvers and instances can be viewed in HTML (soon available).

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++kw_aigNFLSAT
#solved:585453
#solved SAT/UNSAT:17/4116/3818/35
average time per solved instance:95.9114.5139.6
rank:123

Detailed results including runtimes for all solvers and instances can be viewed in HTML.