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)
| Score | Total Solved | SAT Solved | UNSAT Verified | (UNSAT Claimed: proofFailed / dratFailed) | Solver Name | Note |
|---|---|---|---|---|---|---|
| 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)
| Score | Total Solved | SAT Solved | UNSAT Verified | (UNSAT Claimed: proofFailed / dratFailed) | Solver Name | Note |
|---|---|---|---|---|---|---|
| 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)
| Score | Total Solved | SAT Solved | UNSAT Solved | Solver Name | Note |
|---|---|---|---|---|---|
| 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)
| Score | Total Solved | SAT Solved | UNSAT Solved | Solver 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)
| Score | Total Solved | SAT Solved | UNSAT Solved | Solver Name | Note |
|---|---|---|---|---|---|
| 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 | 241 | 153 | 88 | cms55-parallel,12core | |
| 1797550.98 | 238 | 140 | 98 | cbpenelope,default | |
| 1835313.84 | 236 | 138 | 98 | ccspenelope,default | |
| 1962633.10 | 224 | 132 | 92 | syrup,24threads | |
| 2006302.17 | 212 | 135 | 77 | penelope_MDLC,default | |
| 2058429.92 | 212 | 127 | 85 | treengeling,default | |
| 2062025.69 | 206 | 129 | 77 | scalope,default | |
| 2100147.24 | 206 | 121 | 85 | ManyGlucose4.1-2,24threads | |
| 2115484.83 | 202 | 122 | 80 | painless,sym | |
| 2177525.14 | 198 | 121 | 77 | syrup,48threads | |
| 2222058.45 | 193 | 117 | 76 | ManyGlucose4.1-2,48threads | |
| 2283973.56 | 232 | 159 | 73 | ReasonLS,default | disqualified* |
| 2284589.34 | 186 | 128 | 58 | satUZK-ddc,default | |
| 2370226.91 | 179 | 125 | 54 | 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.