Sparkle SAT Challenge 2018

Leaderboard

Last Updated: 15 April 2018, 23:59 (UTC-12)

Note: This was the last update of the leader board. The results below are based on all solver submissions and resubmissions received before the end of 14 April 2018. The final results, which are based on all solvers (including solver submissions and resubmissions received on 15 April 2018) and evaluatated on training set and testing set will be announced at at the 2018 SAT Conference.


Results for Leaderboard

Contributions to the actual portfolio selector

Rank Solver rel. marginal contribution abs. marginal contribution Note
1 Lingeling 32.1080% 0.113551
2 CaDiCaL 16.2058% 0.057312
- abcdsat_n18sparkle (closed source) 15.1061% 0.053423 hors concours
3 BreakIDGlucoseSEL 7.5631% 0.026747
- MapleCOMSPS_LRB_VSIDS_2_no_drup_sparkle 4.9770% 0.017601 hors concours
4 glucose-3.0_PADC 3.8976% 0.013784
- smallsatsparkle (closed source) 2.6237% 0.009279 hors concours
- glu_mixSparkle (closed source) 2.6231% 0.009277 hors concours
5 Riss7 2.4075% 0.008514
6 UPLS 2.1503% 0.007605
7 Riss7-no-preprocessor 1.7517% 0.006195
8 gluHack 1.6993% 0.006010
- COMiniSatPS_Pulsar_sparkle 1.5063% 0.005327 hors concours
9 CryptoMiniSatv5.5 1.4485% 0.005123
10 Dimetheus 1.4341% 0.005072
11 Minisat-v2.2.0-68-g37dc6c6 1.0921% 0.003862
- Maple_LCM_Dist_sparkle 0.5894% 0.002085 hors concours
12 ReasonLS 0.3652% 0.001292
13 minisat-2.2.0_PADC 0.2936% 0.001038
14 YalSAT 0.1576% 0.000557


Contributions to the perfect portfolio selector

Rank Solver rel. marginal contribution abs. marginal contribution Note
1 CaDiCaL 17.8656% 0.042192
2 Lingeling 16.7664% 0.039596
- abcdsat_n18sparkle (closed source) 10.2843% 0.024288 hors concours
- smallsatsparkle (closed source) 8.4101% 0.019862 hors concours
3 BreakIDGlucoseSEL 7.7239% 0.018241
4 Riss7 6.5220% 0.015403
5 UPLS 5.8924% 0.013916
- MapleCOMSPS_LRB_VSIDS_2_no_drup_sparkle 4.7366% 0.011186 hors concours
6 glucose-3.0_PADC 3.6603% 0.008644
- glu_mixSparkle (closed source) 3.5019% 0.008270 hors concours
7 CryptoMiniSatv5.5 2.7308% 0.006449
8 Minisat-v2.2.0-68-g37dc6c6 2.2945% 0.005419
9 minisat-2.2.0_PADC 2.2897% 0.005407
- COMiniSatPS_Pulsar_sparkle 2.1532% 0.005085 hors concours
- Maple_LCM_Dist_sparkle 1.6150% 0.003814 hors concours
10 gluHack 1.2620% 0.002980
11 YalSAT 1.0875% 0.002568
12 Riss7-no-preprocessor 0.8453% 0.001996
13 ReasonLS 0.3577% 0.000845
14 Dimetheus 0.0006% 0.000001

Note: Official results will be determined based on relative marginal contribution to the actual portfolio selector on the same testing set as used in the Main Track of the 2018 SAT Competition.


About Marginal Contribution

Since the primary goal of Sparkle SAT Challenge 2018 is to analyse the contribution of each solver to the real state of the art, the Sparkle challenge utilises the concept of marginal contribution to measure each solver's contribution to the actual portfolio selector and the perfect portfolio selector, also known as Virtual Best Solver (VBS).

Assume that we have a set of solvers $S$ and a portfolio $P$ constructed based on $S$. Let $par2(P)$ denote the PAR2 value achieved by leveraging the complementary strenghts of the solvers in $P$.

The absolute marginal contribution (amc) for solver $s$ is calculated as: \begin{equation} amc(s)=\left\{ \begin{array}{ccl} log_{10}{\frac{par2(P\verb|\|\{s\})}{par2(P)}} & & par2(P\verb|\|\{s\})> par2(P) \\ & & \\ 0 & & \text{else} \end{array} \right. \end{equation}

The relative marginal contribution (rmc) for solver $s$ is calculated as: \begin{equation} rmc(s)=\frac{amc(s)}{\sum_{s' \in S}{amc(s')}} \end{equation}

Note: Results for Leaderboard are ranked by preferring greater relative marginal contribution.


About the Training Set

The traning set used in the Sparkle SAT Challenge 2018 consists of all solved instances (including both satisfiable and unsatisfiable ones) from the Main, Application, Crafted/Hard-Combinatorial Tracks from the 2014-2017 SAT Competitions as well as the 2015 SAT Race.