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 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.