SAT Competition 2016

Results

Sat Conference presentation slides.

Sat Competition Proceedings - containing the solver and benchmark descriptions is available on SAT Conference USB Stick and here.

Agile Track

Detailed runtimes for solvers and benchmarks: agile.csv.

Full Ranking:

Total SolvedSAT SolvedUNSAT SolvedSolver
32849602324Riss6,7271,default
31878132374tb_glucose_agile,7233,default
31798452334CHBR_glucose_agile,7231,default
31788452333CHBR_glucose_tuned_agile,7232,default
31628142348tc_glucose_agile,7234,default
31457852360glue_alt,6837,default
30997322367glucosePLE,7052,default
30427882254glucose_hack_kiel_newScript,7138,default
30417872254glucose_hack_kiel_newScript,7138,hack_configuration
30206562364abcdSAT_drup,7066,default
29937412252glucose_hack_kiel_newScript,7138,main_new
29876212366glueminisat-2.2.10-81-agile,7149,agile
29536322321Riss6,7271,noPP
29366782258gulch-agile,7173,default
29125622350MapleCOMSPS_CHB_no_DRUP,7248,CHB_VSIDS_no_drup
28946822212gulch-once,7187,default
28795422337MapleGlucose,7292,default
28775912286Riss6,7271,blackbox
28165742242GHackCOMSPS_no_DRUP,6920,ghack
27934572336MapleCOMSPS_LRB_no_DRUP,7249,LRB_VSIDS_no_drup
27844412343cmsat5_agile2,7144,default
27794692310MapleCOMSPS_no_DRUP,7250,seq_LRB_VSIDS_no_drup
27655192246COMiniSatPS Chandrasekhar no DRUP,7247,no_drup
27433632380splatz,7960,default
27223862336MapleCMS,7283,default
2413412372lingeling,7959,default

NoLimit Track

Detailed runtimes for solvers and benchmarks: nolimit.csv.

Full Ranking:

Total SolvedSAT SolvedUNSAT SolvedSolver
17848130BreakIDCOMiniSatPS,6952,default
16239123Lingeling bbc notrace,7218,default
16149112abcdSAT_lim,6976,default
14646100MapleCMS,7285,default
1323795tc_glucose_agile,7270,default
1315081MapleCOMSPS_no_DRUP,7246,seq_LRB_VSIDS_no_drup
1314289Riss6,7273,noPP
1284682COMiniSatPS Chandrasekhar no DRUP,7243,no_drup
1284385tb_glucose_agile,7269,default
1275176MapleCOMSPS_LRB_no_DRUP,7245,LRB_VSIDS_no_drup
1264581MapleGlucose,7293,default
1264581GHackCOMSPS_no_DRUP,6921,ghack
1264185Riss6,7273,default
1203882Splatz 06v notrace,7257,default
1195168MapleCOMSPS_CHB_no_DRUP,7244,CHB_VSIDS_no_drup
1144173glueminisat-2.2.10-81,7148,default
1074463Riss6,7273,blackbox
1054857CHBR_glucose_tuned_agile,7268,default
1054857CHBR_glucose_agile,7267,default
26260YalSAT 03r,7212,default

Random Track

Detailed runtimes for solvers and benchmarks: random.csv.

Full Ranking:

Total SolvedSAT SolvedUNSAT SolvedSolver
95950dimetheus,6791,randomsat
89890CSCCSat,6796,default
88880DCCAlm,6816,default
84840polypower1.0,7193,default
83830polypower2.0,7304,default
75750YalSAT 03r,7211,default
36360stocBCD,7201,default
24240multi-sat,6772,default
21210cmsat5_agile,7014,default

Main Track

Detailed runtimes for solvers and benchmarks: main.csv, main-craft.csv and main-app.csv.

Full Ranking:

Total SolvedSAT SolvedUNSAT SolvedSolver
20376127MapleCOMSPS_DRUP,seq_LRB_VSIDS_drup,154598
20274128Riss6,noPP_DRAT,154658
20156145Lingeling bbc main,default,154468
19866132glucose_hack_kiel_newScript,main_new,154744
19766131abcdSAT_drup,default,154067
19759138tc_glucose,default,154590
19578117MapleCOMSPS_LRB_DRUP,LRB_VSIDS_drup,154596
19570125Riss6,default_DRAT,154659
19469125Beans And Eggs,default,154732
19467127tb_glucose,default,154588
19370123glucose,default,154473 (CORRECTNESS BUG DETECTED)
19271121COMiniSatPS Chandrasekhar DRUP,drup,154592
19069121GHackCOMSPS_DRUP,ghack_drup,153211
18667119MapleGlucose,default,154710
18567118glue_alt,default,152939
18566119Glucose_nbSat,default,155265
18561124Splatz 06v main,default,154625
18469115glucosePLE,default,153967
18273109MapleCOMSPS_CHB_DRUP,CHB_VSIDS_drup,154594
18164117glueminisat-2.2.10-81-main,maintrack,154247
17768109MapleCMS,default,154687
17574101Riss6,blackbox_DRAT,154660
17571104CHBR_glucose,default,154584
17473101CHBR_glucose_tuned,default,154586
17464110cmsat5_main2,default,154241
17464110cmsat5_autotune2,default,154243
17168103gulch,default,154330
1426676Scavel_SAT,default,154175
33330YalSAT 03r,default,154460

Full Ranking on Application Benchmarks:

Total SolvedSAT SolvedUNSAT SolvedSolver
1547084MapleCOMSPS_LRB_DRUP,LRB_VSIDS_drup,154596
1536885MapleCOMSPS_DRUP,seq_LRB_VSIDS_drup,154598
1516487CHBR_glucose,default,154584
1506684CHBR_glucose_tuned,default,154586
1506486glucose,default,154473
1486187MapleCMS,default,154687
1486088abcdSAT_drup,default,154067
1476978Riss6,noPP_DRAT,154658
1476978Riss6,blackbox_DRAT,154660
1476582Riss6,default_DRAT,154659
1476384Beans And Eggs,default,154732
1475988cmsat5_autotune2,default,154243
1475295Lingeling bbc main,default,154468
1466581COMiniSatPS Chandrasekhar DRUP,drup,154592
1466383glucosePLE,default,153967
1456184tb_glucose,default,154588
1456085Glucose_nbSat,default,155265
1455986cmsat5_main2,default,154241
1446381MapleCOMSPS_CHB_DRUP,CHB_VSIDS_drup,154594
1446183gulch,default,154330
1446183glucose_hack_kiel_newScript,main_new,154744
1436281GHackCOMSPS_DRUP,ghack_drup,153211
1436083glueminisat-2.2.10-81-main,maintrack,154247
1426280MapleGlucose,default,154710
1405684Splatz 06v main,default,154625
1396079glue_alt,default,152939
1395683tc_glucose,default,154590
1176057Scavel_SAT,default,154175
20200YalSAT 03r,default,154460

Full Ranking on Crafted Benchmarks:

Total SolvedSAT SolvedUNSAT SolvedSolver
58355tc_glucose,default,154590
55550Riss6,noPP_DRAT,154658
54549glucose_hack_kiel_newScript,main_new,154744
54450Lingeling bbc main,default,154468
50842MapleCOMSPS_DRUP,seq_LRB_VSIDS_drup,154598
49643tb_glucose,default,154588
49643abcdSAT_drup,default,154067
48543Riss6,default_DRAT,154659
47740GHackCOMSPS_DRUP,ghack_drup,153211
47641Beans And Eggs,default,154732
46739glue_alt,default,152939
46640COMiniSatPS Chandrasekhar DRUP,drup,154592
45540Splatz 06v main,default,154625
44539MapleGlucose,default,154710
43637glucose,default,154473
41833MapleCOMSPS_LRB_DRUP,LRB_VSIDS_drup,154596
40634Glucose_nbSat,default,155265
38632glucosePLE,default,153967
38434glueminisat-2.2.10-81-main,maintrack,154247
381028MapleCOMSPS_CHB_DRUP,CHB_VSIDS_drup,154594
29722MapleCMS,default,154687
29524cmsat5_main2,default,154241
28523Riss6,blackbox_DRAT,154660
27720gulch,default,154330
27522cmsat5_autotune2,default,154243
25619Scavel_SAT,default,154175
24717CHBR_glucose_tuned,default,154586
24717CHBR_glucose,default,154584
13130YalSAT 03r,default,154460

Parallel Track

Detailed runtimes for solvers and benchmarks: parallel.csv.

Full Ranking:

Total SolvedSAT SolvedUNSAT SolvedSolver
315109206treengeling-bbc-sc2016
30288214plingeling-bbc-sc2016
29787210cmsat5_run_parallel
29190201glucose syrup
25094156cbpenelope2016
24492152penelope_for_2015_AICR_24_Pair_BUMP100
24195146ccspenelope2016
23589146penelope_for_2015_AICR_48_Pair_BUMP100
22082138Priss6
20878130tbParaGlueminisat_2016
18070110dissolve
17676100ParaGlueminisat_2016
1628775gluco_par
1395485ampharos-sat-2016

Incremental Track

Detailed runtimes for each solver: HWMCC, Essentials, and PMaxSat

The following table contains the number of solved problems by each solver in each application domain. The different versions of the solver are grouped and a rank is assigned to the group based on the best performance. The best average rank determines the winner.

SolverEssentialsRankHWMCCRankPMaxSATRankAvg. Rank
cominisatps2sun_nopre 857326544.0
cominisatps2sun 757327744.0
cryptominisat4auto 1828228922.0
cryptominisat4 1828228922.0
glucose4 1917328232.3
riss_521 1637125853.0
riss_600 15313126153.0
abcdsat_inc 1245529013.3