SAT Competition 2018

Results

The slides used at the 2018 SAT Conference.

The Proceedings of the SAT Competition 2018: Solver and Benchmark Descriptions is now available.

Main Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT Verified(UNSAT Claimed: proofFailed / dratFailed)Solver NameNote
1857321.82182 231 135 96 0 / 6 MapleLCMDistChronoBT, default
1872489.47761 228 134 94 0 / 4 Maple_LCM_Scavel_fix2, default
1908304.62009 224 125 99 0 / 1 Maple_CM, default
1931478.76194 226 133 93 0 / 4 cms55-main-all4fixed, otherconf
1934450.23573 224 125 99 0 / 1 Maple_CM_ordUIP, default
1936290.64566 221 123 98 0 / 1 Maple_CM_Dist, default
1946689.68345 224 130 94 0 / 4 cms55-main-all4fixed, glubreak
1947025.44071 222 123 99 0 / 2 Maple_CM_ordUIP+, default
1961567.26229 217 126 91 0 / 7 Maple_LCM_Scavel_200_fix2, default
1964101.07399 223 128 95 0 / 4 cms55-main-all4fixed, main
1978764.14146 218 120 98 0 / 2 Maple_LCM+BCrestart_M1, default
1982469.86645 218 120 98 0 / 1 Maple_LCM+BCrestart, default
1986048.68308 227 120 107 0 / 2 CaDiCaL, DONTUNZIP-fixed
1987577.26975 216 125 91 0 / 3 expMC_LRB_VSIDS_Switch_2500, default
1996387.35293 215 116 99 0 / 2 Maple_LCM_M1, default
2007124.34123 214 119 95 0 / 1 COMiniSatPS_Pulsar_drup, drup
2009069.02781 213 122 91 0 / 1 MapleCOMSPS_LRB_VSIDS_2_fix, LRB_VSIDS_2_drup
2015965.37161 213 125 88 0 / 0 expMC_LRB_VSIDS_Switch, default
2050552.6515 211 119 92 0 / 1 MapleCOMSPS_LRB_VSIDS_drup, LRB_VSIDS_drup
2088022.62186 221 127 94 0 / 1 expMC_VSIDS_LRB_Switch_2500, default
2108529.4996 205 116 89 0 / 3 smallsat, default
2141050.27624 203 115 88 0 / 2 cms55-main-all4fixed, autotune
2193453.55381 197 107 90 0 / 0 MapleCOMSPS_CHB_VSIDS_drup, CHB_VSIDS_drup
2205133.64405 196 105 91 0 / 3 GHackCOMSPS_drup, ghack_drup
2246060.45603 194 110 84 0 / 2 inIDGlucose, default
2262847.55035 192 106 86 0 / 6 glu_mix, default
2277597.14766 190 96 94 0 / 3 glucose 4.2.1, default
2289953.6573 190 102 88 0 / 1 Lingeling, default
2299295.28232 193 106 87 0 / 0 expGlucose, default
2313009.94072 182 116 66 0 / 4 abcdsat_r18, default
2379070.32971 181 96 85 0 / 3 glucose-3.0_PADC_10, default
2425018.33481 176 86 90 0 / 1 Glucose_Hack_Kiel_fastBVE, default
2444829.85477 174 85 89 0 / 0 glucose3.0, proofs hors concours*
2449972.5373 173 105 68 0 / 10 Minisat-v2.2.0-106-ge2dd095, simp_proof hors concours*
2480558.00634 172 105 67 0 / 11 varisat, default
2489038.43442 169 95 74 0 / 8 glucose-3.0_PADC_3, default
2604759.45877 157 91 66 17 / 0 Sparrow2Riss-2018-fixfix, MAIN
2629564.94631 155 89 66 17 / 0 Riss7.1-fix, BVE_DRAT
2933160.0123 116 98 18 60 / 0 gluHack, default
2964351.0149 116 95 21 41 / 0 Candy, default
3472985.68118 54 54 0 0 / 0 YalSAT, default

Detailed results and benchmarks avaliable here.

* Submitted for comparison purposes only.

Glucose Hack Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT Verified(UNSAT Claimed: proofFailed / dratFailed)Solver NameNote
2205133.64405 196 105 91 0 / 3 GHackCOMSPS_drup, ghack_drup
2246060.45603 194 110 84 0 / 2 inIDGlucose, default
2262847.55035 192 106 86 0 / 6 glu_mix, default
2379070.32971 181 96 85 0 / 3 glucose-3.0_PADC_10, default
2425018.33481 176 86 90 0 / 1 Glucose_Hack_Kiel_fastBVE, default
2444829.85477 174 85 89 0 / 0 glucose3.0, proofs hors concours*
2489038.43442 169 95 74 0 / 8 glucose-3.0_PADC_3, default
2933160.0123 116 98 18 60 / 0 gluHack, default

This is a subset view of the Main track results.

* The ``trivial'' hack; submitted for comparison purposes only.

NoLimit Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver NameNote
1875448.52541 229 129 100 ReasonLS, default_nodrup
1890452.09502 227 127 100 Maple_CM, default
1915985.6432 230 130 100 cms55-nolimits-otherconf-v20, default
1935934.47016 226 126 100 cms55-nolimits-v19, default
1943354.25038 223 122 101 Maple_CM_ordUIP+, default
1943988.38765 220 120 100 Maple_CM_Dist, default
1946595.93187 222 122 100 Maple_CM_ordUIP, default
1958979.03266 230 122 108 CaDiCaL, default
1959258.27265 231 140 91 Sparrow2Riss-2018, NOLIMIT
1960117.16421 222 123 99 cms55-nolimits-autotune-v19, default
1967312.66635 221 123 98 cms55-nolimits-gluebreak-v19, default
1986412.61296 216 123 93 MapleCOMSPS_LRB_VSIDS_2_no_drup_fix, LRB_VSIDS_2_no_drup
2016132.77409 214 118 96 COMiniSatPS_Pulsar_no_drup, no_drup
2079101.72129 210 117 93 MapleCOMSPS_LRB_VSIDS_no_drup, LRB_VSIDS_no_drup
2090919.37266 208 116 92 smallsat, default
2119859.43611 204 113 91 Riss7.1, NOLIMIT
2161032.28202 205 140 65 ReasonLS_h, default
2190352.78081 197 104 93 GHackCOMSPS_no_drup, ghack_no_drup
2198739.8236 200 109 91 Lingeling, default
2219261.93232 195 116 79 abcdsat_n18, default disqualified*
2219800.05364 200 95 105 BreakIDGlucoseSEL, default
2234355.96437 195 104 91 glu_mix, default
2234507.49894 197 101 96 BreakIDGlucose, default
2254609.45222 190 101 89 MapleCOMSPS_CHB_VSIDS_no_drup, CHB_VSIDS_no_drup
2263465.09369 188 116 72 abcdsat_r18, nolimit
2313770.87061 190 105 85 expGlucoseSilent, default
2358379.50698 183 96 87 glucose-3.0_PADC_10_NoDRUP, default
2398640.55494 180 96 84 glucose-3.0_PADC_3_NoDRUP, default
2399746.60568 176 98 78 gluHack, default
2412486.96725 178 86 92 Glucose_Hack_Kiel_fastBVE, default
2561199.74888 163 97 66 Candy, agile
2580746.99334 160 96 64 Candy, default
3314984.25793 70 70 0 CPSparrow, default
3473447.49597 54 54 0 YalSAT, default

Detailed results and benchmarks avaliable here.

* This solver produced an incorrect answer.

Random Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver Name
687420.739685 188 188 0 Sparrow2Riss-2018, NOLIMIT
901550.62826 165 165 0 gluHack, default
902011.584756 165 165 0 glucose-3.0_PADC_10_NoDRUP, default
902244.096104 165 165 0 glucose-3.0_PADC_3_NoDRUP, default
904236.016896 165 165 0 expGlucoseSilent, default
946811.518613 163 163 0 CPSparrow, default
1035064.06005 155 155 0 dimetheus, randomsat
1198881.99539 138 138 0 probSAT, RANDOM
1280179.53597 129 129 0 YalSAT, default
1747096.14835 81 81 0 lawa, default

Detailed results and benchmarks avaliable here.

Parallel Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver NameNote
1252833.28 289 164 125 TopoSAT,plain disqualified*
1304789.70 284 159 125 TopoSAT,lazy disqualified*
1397524.67 275 153 122 painless,default
1410158.33 275 157 118 plingeling,default
1736011.66 241 148 93 abcdsat,default
1755049.35 276 171 105 cms55-parallel,12core
1797550.98 238 140 98 cbpenelope,default
1835313.84 236 138 98 ccspenelope,default
1962633.10 261 152 109 syrup,24threads
2006302.17 212 135 77 penelope_MDLC,default
2058429.92 230 135 95 treengeling,default
2062025.69 206 129 77 scalope,default
2100147.24 246 141 105 ManyGlucose4.1-2,24threads
2115484.83 237 143 94 painless,sym
2177525.14 236 147 89 syrup,48threads
2222058.45 228 140 88 ManyGlucose4.1-2,48threads
2283973.56 232 159 73 ReasonLS,default disqualified*
2284589.34 211 141 70 satUZK-ddc,default
2370226.91 198 134 64 satUZK-ddc,ddist
3023808.42 99 80 19 cms55-parallel,24core
3071955.61 89 40 49 hordesat,default

Detailed results and benchmarks avaliable here.

* This solver produced an incorrect answer.