The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Medal standings division as of Fri Jun 27 16:49:23 EDT 2014
The gold and silver medal winners are the first and second place measured by absence of errors and the most solved problems, measured by a weighted, non-linear metric across divisions.
| Solver | % Complete | Weighted Errors |
Weighted Solved |
|---|---|---|---|
| veriT | 100% | 0.000 | 25.325 |
| SMTInterpol | 100% | 0.000 | 22.831 |
| CVC3 | 100% | 0.000 | 9.618 |
| SONOLAR | 100% | 0.000 | 5.978 |
| AProVE | 100% | 0.000 | 3.776 |
| Boolector (justification) | 100% | 0.000 | 3.758 |
| Boolector (dual propagation) | 100% | 0.000 | 3.755 |
| OpenSMT2 | 100% | 0.000 | 3.582 |
| Boolector | 100% | 0.000 | 3.058 |
| STP-CryptoMiniSat4 | 100% | 0.000 | 2.859 |
| 4Simp | 100% | 0.000 | 2.468 |
| raSAT | 100% | 0.000 | 0.000 |
| Yices2 | 100% | 3.810 | 38.624 |
| CVC4 | 100% | 7.283 | 54.152 |
| abziz_min_features | 100% | 30.563 | 2.548 |
| abziz_all_features | 100% | 30.563 | 2.403 |
| Kleaver-STP | 100% | 213.362 | 3.103 |
| Kleaver-portfolio | 100% | 346.713 | 3.073 |
The bronze medal is awarded to the winner of the QF_BV division.
The organizers also considered a different metric for gold/silver medals. We officially adopted the one above, as expressed in the competition rules, since it emphasizes soundness of solvers (a solver with an error in any division scores lower than solvers with no errors, even when they compete in fewer divisions). In the alternate metric, a division without errors contributes the squared fraction of solved instances weighted by the log10 of the number of benchmarks in the division; a division with errors contributes the negative of the division’s weight times the number of errors. For comparative information only, the table below shows rankings using this metric.
| Solver | % Complete | Alternate Metric |
|---|---|---|
| CVC4 | 100% | 43.509 |
| Yices2 | 100% | 31.059 |
| veriT | 100% | 25.325 |
| SMTInterpol | 100% | 22.831 |
| CVC3 | 100% | 9.618 |
| SONOLAR | 100% | 5.978 |
| AProVE | 100% | 3.776 |
| Boolector (justification) | 100% | 3.758 |
| Boolector (dual propagation) | 100% | 3.755 |
| OpenSMT2 | 100% | 3.582 |
| Boolector | 100% | 3.058 |
| STP-CryptoMiniSat4 | 100% | 2.859 |
| 4Simp | 100% | 2.468 |
| raSAT | 100% | 0.000 |
| abziz_min_features | 100% | -30.563 |
| abziz_all_features | 100% | -30.563 |
| Kleaver-STP | 100% | -213.362 |
| Kleaver-portfolio | 100% | -346.713 |