Updated on March 19 with poll results. The login of the submitters that voted for a given scoring scheme is displayed to allow the submitters to check that their vote has been properly taken into account.
The competitors are expected to vote for the ranking scheme that will be used during the competition. One vote per submitter (i.e. login). A submitter can propose alternative ranking schemes based on the data available in the competition framework. The submitter vote (preferred scoring scheme) is to send by email to organizers at satcompetition dot org.
We have heard at least two criticisms against the scoring scheme used in the previous competitions. First, it aggregates two criteria which are orthogonal, and second, the score of a solver depends on other solvers.
From a practical point of view, a standard user of SAT technology wants to identify the solvers which are the most likely to solve its instances. This corresponds to a notion of robustness. "Best" solvers are the ones which solve the greatest number of instances, preferably in the smallest time.
From a "scientific" point of view, the community would like to award an innovative solver. A solver which solves instances that other solvers don't (SOTAC) is an example of such kind of solvers.
The purse system mixes these two points of view in a single ranking, but not everybody agrees with that.
Especially, the purse system has a the side effect to make the scores (thus the ranking) of two solvers depend on the results of a third solver.
So the idea this year is that the score of a solver should not depend on other solvers. This score should only depend on the chosen benchmarks set, the chosen time and memory limits and the chosen hardware. Hence the name SATSPEC09 to indicate that anybody would be potentially able to compare his solver with the solver submitted to the competition using that score. It would also allow to score additional solvers such as all the winners of the previous competitions without changing the scores of the solvers of this year competition.
There are several criteria which can be used to compare solvers:
One interesting question is if the speed of a faster solver can compensate for its failure to solve an instance. For example, assume solver A can solver 100 instances in 1000s (cumulated time) and solver B can solve the same 100 instances in only 100s. At this point, solver B is clearly better than solver A. Now assume solver A can solve one more instance than B. Which solver is the best? The answer is probably not unique and certainly depends on the user's applications and expectations.
The competition framework generates the following data:
Since the first edition of the SAT Race, we have seen in many papers and presentations experiments made on the SAT Race benchmarks sets (100 benchmarks each). The tables are usually sorted lexicographically, first on the number of benchmarks solved, then on the cumulative CPU time needed to solve those benchmarks.
It is a simple ranking scheme, easy to reproduce, and that can be easily used by SAT solver developers to see where their solver stands among state-of-the-art SAT solvers by running their own solver of the set of benchmarks on computers similar to the ones used during the Races.
(NBSOLVED, sum ti)
Note: in this scheme, a fast solver cannot compensate for its inability to solve an instance.
Another simple way to rank the solvers is simply to sum up the CPU times of the solver on the set of benchmarks, and to give a penalty when the solver times out or abort early.
sum ti + (NBTOTAL-NBSOLVED)*TIMEOUT*PENALTY
Note: in this scheme, a fast solver can compensate for its inability to solve an instance. The value of PENALTY determines how faster a solver must be to compensate for the loss of an instance.
The idea of that scoring is the same as the preceding one, but based on a log of each CPU time to score closely solvers running in the same order of magnitude.
sum log10(1+ti) + (NBTOTAL-NBSOLVED)*log10((1 + TIMEOUT)*PENALTY)
The motivation for using a log is that human beings are probably more receptive to the log of a value rather than the value itsef (100s and 1000s makes a significant difference, 100s and 200s is not so different). The 1 is introduced to avoid negative score for timings below 1s. Of course, log10((1 + TIMEOUT)*PENALTY) can be rewritten as log10(1 + TIMEOUT)+log10(PENALTY).
Note: in this scheme, a fast solver can compensate for its inability to solve an instance. The value of PENALTY determines how faster a solver must be to compensate for the loss of an instance. For example, if PENALTY equals 100, failing on an instance can be compensated if the solver is 100 times faster on another instance, or if it 10 times faster on 2 instances, and so on. Possible values for PENALTY are 10, 100, 1000, 10000.
Proposed by Marijn Heule
The rationale of that scoring scheme is that a robust solver, i.e. a solver able to solve a wide range of benchmarks, (it could also be called multi-purpose), should be better ranked than a solver very good on very specific benchmarks. To do so, we add a new penalty for each series (kind of benchmark) for which the solver has not been able to solve any member.
sum ti + (NBTOTAL-NBSOLVED)*TIMEOUT*PENALTY + NBUNSOLVEDSERIES*SERIESPENALTY
Note: we could also use a log scale on those numbers.
See Allen's scoring poster or the SAT competition 2007 rules for details
Note that the purse based system does not obey the SATSPEC09 spirit, since it is dependent of the set of solvers to be evaluated.
Note: the advantage (and disadvantage) of this scoring is that it agregates several criteria.
Rank | Solver | Version | Number of solved instances |
Cumulated CPU time on solved instances |
sum(time), penalty=10 | sum(time), penalty=100 | sum(time), penalty=1000 | sum(time), penalty=10000 | sum(log(time)), penalty=10 | sum(log(time)), penalty=100 | sum(log(time)), penalty=1000 | sum(log(time)), penalty=10000 | Purse score |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
1 | minisat | SAT 2007 | 71 | 13105.00 | 1573105.00 | 15613105.00 | 156013105.00 | 1560013105.00 | 1172.96 | 1302.96 | 1432.96 | 1562.96 | 24601 |
2 | minisat | SAT 2007 (with assertions) | 71 | 13567.60 | 1573567.60 | 15613567.60 | 156013567.60 | 1560013567.60 | 1174.43 | 1304.43 | 1434.43 | 1564.43 | |
3 | SATzilla | FULL | 69 | 11673.72 | 1595673.72 | 15851673.72 | 158411673.72 | 1584011673.72 | 1168.11 | 1300.11 | 1432.11 | 1564.11 | |
4 | SATzilla | CRAFTED | 69 | 12281.44 | 1596281.44 | 15852281.44 | 158412281.44 | 1584012281.44 | 1172.40 | 1304.40 | 1436.40 | 1568.40 | 30336 |
5 | minimarch | 2007-04-26 (fixed) | 67 | 16433.82 | 1624433.82 | 16096433.82 | 160816433.82 | 1608016433.82 | 1205.41 | 1339.41 | 1473.41 | 1607.41 | |
6 | MiraXT | v3 | 57 | 13929.06 | 1741929.06 | 17293929.06 | 172813929.06 | 1728013929.06 | 1267.47 | 1411.47 | 1555.47 | 1699.47 | 14737 |
7 | MiraXT | v2 | 55 | 13445.05 | 1765445.05 | 17533445.05 | 175213445.05 | 1752013445.05 | 1281.04 | 1427.04 | 1573.04 | 1719.04 | 10923 |
8 | MiraXT | v1 | 55 | 14146.51 | 1766146.51 | 17534146.51 | 175214146.51 | 1752014146.51 | 1281.90 | 1427.90 | 1573.90 | 1719.90 | 13792 |
9 | MXC | 2007-02-08 | 53 | 16084.61 | 1792084.61 | 17776084.61 | 177616084.61 | 1776016084.61 | 1311.03 | 1459.03 | 1607.03 | 1755.03 | 15503 |
10 | CMUSAT | 2007-02-08 | 52 | 9361.42 | 1797361.42 | 17889361.42 | 178809361.42 | 1788009361.42 | 1293.17 | 1442.17 | 1591.17 | 1740.17 | 13726 |
11 | picosat | 535 | 46 | 12383.00 | 1872383.00 | 18612383.00 | 186012383.00 | 1860012383.00 | 1337.23 | 1492.23 | 1647.23 | 1802.23 | 10512 |
12 | SAT7 | 2007-02-08 | 46 | 14162.30 | 1874162.30 | 18614162.30 | 186014162.30 | 1860014162.30 | 1353.44 | 1508.44 | 1663.44 | 1818.44 | 7352 |
13 | SATzilla | RANDOM | 44 | 8865.79 | 1892865.79 | 18848865.79 | 188408865.79 | 1884008865.79 | 1330.24 | 1487.24 | 1644.24 | 1801.24 | 13112 |
14 | Barcelogic Fixed | 2007-04-13 | 40 | 8704.21 | 1940704.21 | 19328704.21 | 193208704.21 | 1932008704.21 | 1375.83 | 1536.83 | 1697.83 | 1858.83 | |
15 | TTS | 4.0 | 37 | 3347.89 | 1971347.89 | 19683347.89 | 196803347.89 | 1968003347.89 | 1376.51 | 1540.51 | 1704.51 | 1868.51 | 36457 |
16 | CMUSAT BASE | 2007-02-08 | 37 | 9957.74 | 1977957.74 | 19689957.74 | 196809957.74 | 1968009957.74 | 1401.59 | 1565.59 | 1729.59 | 1893.59 | 5275 |
17 | Rsat | 2007-02-08 | 37 | 12315.78 | 1980315.78 | 19692315.78 | 196812315.78 | 1968012315.78 | 1400.37 | 1564.37 | 1728.37 | 1892.37 | 9164 |
18 | March KS | 2007-02-08 | 33 | 6519.65 | 2022519.65 | 20166519.65 | 201606519.65 | 2016006519.65 | 1397.16 | 1565.16 | 1733.16 | 1901.16 | 29133 |
19 | Spear FH | 1.0 | 33 | 12790.81 | 2028790.81 | 20172790.81 | 201612790.81 | 2016012790.81 | 1430.79 | 1598.79 | 1766.79 | 1934.79 | |
20 | Spear FHS | 1.0 | 32 | 11814.40 | 2039814.40 | 20291814.40 | 202811814.40 | 2028011814.40 | 1435.91 | 1604.91 | 1773.91 | 1942.91 | |
21 | SAT4J | SAT 2007 | 32 | 12631.54 | 2040631.54 | 20292631.54 | 202812631.54 | 2028012631.54 | 1439.33 | 1608.33 | 1777.33 | 1946.33 | |
22 | Spear | 2007-02-12 | 31 | 11312.68 | 2051312.68 | 20411312.68 | 204011312.68 | 2040011312.68 | 1442.54 | 1612.54 | 1782.54 | 1952.54 | |
23 | TiniSatELite | 2007-02-08 | 27 | 8026.56 | 2096026.56 | 20888026.56 | 208808026.56 | 2088008026.56 | 1457.05 | 1631.05 | 1805.05 | 1979.05 | 3574 |
24 | tinisat | 2007-02-08 | 25 | 5322.47 | 2117322.47 | 21125322.47 | 211205322.47 | 2112005322.47 | 1472.02 | 1648.02 | 1824.02 | 2000.02 | 3133 |
25 | DEWSATZ 1A | 2007-02-08 | 20 | 5100.84 | 2177100.84 | 21725100.84 | 217205100.84 | 2172005100.84 | 1502.68 | 1683.68 | 1864.68 | 2045.68 | 4609 |
26 | DEWSATZ | 2007-04-26 (fixed) | 15 | 3961.61 | 2235961.61 | 22323961.61 | 223203961.61 | 2232003961.61 | 1532.85 | 1718.85 | 1904.85 | 2090.85 | |
27 | KCNFS | SMP | 15 | 5153.27 | 2237153.27 | 22325153.27 | 223205153.27 | 2232005153.27 | 1534.46 | 1720.46 | 1906.46 | 2092.46 | 2221 |
28 | KCNFS | 2006 | 14 | 3157.38 | 2247157.38 | 22443157.38 | 224403157.38 | 2244003157.38 | 1538.52 | 1725.52 | 1912.52 | 2099.52 | 2142 |
29 | KCNFS | 2004 | 14 | 3274.50 | 2247274.50 | 22443274.50 | 224403274.50 | 2244003274.50 | 1538.70 | 1725.70 | 1912.70 | 2099.70 | 2148 |
30 | ornithorynque | 0.1 alpha | 9 | 3296.36 | 2307296.36 | 23043296.36 | 230403296.36 | 2304003296.36 | 1574.55 | 1766.55 | 1958.55 | 2150.55 | |
31 | Hybrid1 | 2007-02-08 | 8 | 229.51 | 2316229.51 | 23160229.51 | 231600229.51 | 2316000229.51 | 1570.82 | 1763.82 | 1956.82 | 2149.82 | 1274 |
32 | FH | 2007-02-08 | 7 | 261.54 | 2328261.54 | 23280261.54 | 232800261.54 | 2328000261.54 | 1577.75 | 1771.75 | 1965.75 | 2159.75 | 1183 |
33 | adaptg2wsat | 2007-02-08 | 6 | 199.81 | 2340199.81 | 23400199.81 | 234000199.81 | 2340000199.81 | 1585.82 | 1780.82 | 1975.82 | 2170.82 | |
34 | adaptg2wsat+ | 2007-02-08 | 6 | 478.89 | 2340478.89 | 23400478.89 | 234000478.89 | 2340000478.89 | 1586.20 | 1781.20 | 1976.20 | 2171.20 | 761 |
35 | ranov | 2007-02-08 | 6 | 2773.86 | 2342773.86 | 23402773.86 | 234002773.86 | 2340002773.86 | 1592.70 | 1787.70 | 1982.70 | 2177.70 | 578 |
36 | adaptg2wsat0 | 2007-02-08 | 4 | 259.56 | 2364259.56 | 23640259.56 | 236400259.56 | 2364000259.56 | 1599.77 | 1796.77 | 1993.77 | 2190.77 | 568 |
37 | adaptg2wsatp | 2007-02-08 | 4 | 323.17 | 2364323.17 | 23640323.17 | 236400323.17 | 2364000323.17 | 1601.02 | 1798.02 | 1995.02 | 2192.02 | 357 |
38 | UnitMarch | 2007-02-08 | 3 | 421.62 | 2376421.62 | 23760421.62 | 237600421.62 | 2376000421.62 | 1607.22 | 1805.22 | 2003.22 | 2201.22 | 581 |
39 | adaptnovelty | 2007-02-08 | 3 | 1768.33 | 2377768.33 | 23761768.33 | 237601768.33 | 2376001768.33 | 1609.70 | 1807.70 | 2005.70 | 2203.70 | 406 |
40 | Mmisat | 2007-02-08 | 2 | 757.88 | 2388757.88 | 23880757.88 | 238800757.88 | 2388000757.88 | 1615.01 | 1814.01 | 2013.01 | 2212.01 | 239 |
41 | saps | 2007-02-08 | 2 | 1590.70 | 2389590.70 | 23881590.70 | 238801590.70 | 2388001590.70 | 1615.73 | 1814.73 | 2013.73 | 2212.73 | 198 |
42 | gnovelty+ | 2007-02-08 | 1 | 61.94 | 2400061.94 | 24000061.94 | 240000061.94 | 2400000061.94 | 1619.81 | 1819.81 | 2019.81 | 2219.81 | 214 |
43 | sapsrt | 2007-02-08 | 1 | 147.42 | 2400147.42 | 24000147.42 | 240000147.42 | 2400000147.42 | 1620.19 | 1820.19 | 2020.19 | 2220.19 | 158 |
Rank | Solver | Version | Number of solved instances |
Cumulated CPU time on solved instances |
sum(time), penalty=10 | sum(time), penalty=100 | sum(time), penalty=1000 | sum(time), penalty=10000 | sum(log(time)), penalty=10 | sum(log(time)), penalty=100 | sum(log(time)), penalty=1000 | sum(log(time)), penalty=10000 | Purse score |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
1 | Rsat | 2007-02-08 | 106 | 18043.45 | 1554043.45 | 15378043.45 | 153618043.45 | 1536018043.45 | 1216.44 | 1344.44 | 1472.44 | 1600.44 | 44623 |
2 | TiniSatELite | 2007-02-08 | 103 | 22193.27 | 1594193.27 | 15742193.27 | 157222193.27 | 1572022193.27 | 1243.19 | 1374.19 | 1505.19 | 1636.19 | 30301 |
3 | picosat | 535 | 103 | 30610.29 | 1602610.29 | 15750610.29 | 157230610.29 | 1572030610.29 | 1273.05 | 1404.05 | 1535.05 | 1666.05 | 25509 |
4 | Barcelogic Fixed | 2007-04-13 | 99 | 21811.01 | 1641811.01 | 16221811.01 | 162021811.01 | 1620021811.01 | 1269.81 | 1404.81 | 1539.81 | 1674.81 | |
5 | Spear FHS | 1.0 | 99 | 22610.38 | 1642610.38 | 16222610.38 | 162022610.38 | 1620022610.38 | 1278.38 | 1413.38 | 1548.38 | 1683.38 | |
6 | minisat | SAT 2007 | 97 | 20931.03 | 1664931.03 | 16460931.03 | 164420931.03 | 1644020931.03 | 1270.50 | 1407.50 | 1544.50 | 1681.50 | 29714 |
7 | minisat | SAT 2007 (with assertions) | 96 | 20540.63 | 1676540.63 | 16580540.63 | 165620540.63 | 1656020540.63 | 1281.22 | 1419.22 | 1557.22 | 1695.22 | |
8 | Spear FH | 1.0 | 93 | 20041.31 | 1712041.31 | 16940041.31 | 169220041.31 | 1692020041.31 | 1317.36 | 1458.36 | 1599.36 | 1740.36 | |
9 | MiraXT | v1 | 91 | 18849.09 | 1734849.09 | 17178849.09 | 171618849.09 | 1716018849.09 | 1309.36 | 1452.36 | 1595.36 | 1738.36 | 23844 |
10 | tinisat | 2007-02-08 | 90 | 21826.71 | 1749826.71 | 17301826.71 | 172821826.71 | 1728021826.71 | 1334.13 | 1478.13 | 1622.13 | 1766.13 | 20237 |
11 | CMUSAT | 2007-02-08 | 89 | 17871.18 | 1757871.18 | 17417871.18 | 174017871.18 | 1740017871.18 | 1320.43 | 1465.43 | 1610.43 | 1755.43 | 25334 |
12 | MiraXT | v3 | 89 | 20671.20 | 1760671.20 | 17420671.20 | 174020671.20 | 1740020671.20 | 1324.88 | 1469.88 | 1614.88 | 1759.88 | 26590 |
13 | minimarch | 2007-04-26 (fixed) | 88 | 18993.44 | 1770993.44 | 17538993.44 | 175218993.44 | 1752018993.44 | 1328.83 | 1474.83 | 1620.83 | 1766.83 | |
14 | SATzilla | FULL | 88 | 29939.41 | 1781939.41 | 17549939.41 | 175229939.41 | 1752029939.41 | 1382.15 | 1528.15 | 1674.15 | 1820.15 | |
15 | MXC | 2007-02-08 | 84 | 18692.39 | 1818692.39 | 18018692.39 | 180018692.39 | 1800018692.39 | 1372.34 | 1522.34 | 1672.34 | 1822.34 | 19170 |
16 | MiraXT | v2 | 83 | 17916.25 | 1829916.25 | 18137916.25 | 181217916.25 | 1812017916.25 | 1358.72 | 1509.72 | 1660.72 | 1811.72 | 18819 |
17 | Spear | 2007-02-12 | 82 | 15355.45 | 1839355.45 | 18255355.45 | 182415355.45 | 1824015355.45 | 1386.28 | 1538.28 | 1690.28 | 1842.28 | |
18 | SATzilla | CRAFTED | 81 | 26772.70 | 1862772.70 | 18386772.70 | 183626772.70 | 1836026772.70 | 1420.13 | 1573.13 | 1726.13 | 1879.13 | 16722 |
19 | CMUSAT BASE | 2007-02-08 | 80 | 22286.33 | 1870286.33 | 18502286.33 | 184822286.33 | 1848022286.33 | 1407.01 | 1561.01 | 1715.01 | 1869.01 | 18726 |
20 | SAT7 | 2007-02-08 | 69 | 21188.66 | 2001188.66 | 19821188.66 | 198021188.66 | 1980021188.66 | 1475.85 | 1640.85 | 1805.85 | 1970.85 | 11449 |
21 | SATzilla | RANDOM | 66 | 23303.59 | 2039303.59 | 20183303.59 | 201623303.59 | 2016023303.59 | 1508.92 | 1676.92 | 1844.92 | 2012.92 | 14932 |
22 | SAT4J JVM PARAM CHANGED | SAT 2007 | 66 | 23870.23 | 2039870.23 | 20183870.23 | 201623870.23 | 2016023870.23 | 1499.78 | 1667.78 | 1835.78 | 2003.78 | |
23 | SAT4J | SAT 2007 | 57 | 19670.66 | 2143670.66 | 21259670.66 | 212419670.66 | 2124019670.66 | 1549.29 | 1726.29 | 1903.29 | 2080.29 | |
24 | ornithorynque | 0.1 alpha | 33 | 5553.22 | 2417553.22 | 24125553.22 | 241205553.22 | 2412005553.22 | 1682.43 | 1883.43 | 2084.43 | 2285.43 | |
25 | DEWSATZ 1A | 2007-02-08 | 22 | 6010.53 | 2550010.53 | 25446010.53 | 254406010.53 | 2544006010.53 | 1761.92 | 1973.92 | 2185.92 | 2397.92 | 2590 |
26 | DEWSATZ | 2007-04-26 (fixed) | 19 | 5044.84 | 2585044.84 | 25805044.84 | 258005044.84 | 2580005044.84 | 1779.58 | 1994.58 | 2209.58 | 2424.58 | |
27 | KCNFS | 2006 | 16 | 2701.24 | 2618701.24 | 26162701.24 | 261602701.24 | 2616002701.24 | 1790.60 | 2008.60 | 2226.60 | 2444.60 | 3029 |
28 | March KS | 2007-02-08 | 12 | 2977.72 | 2666977.72 | 26642977.72 | 266402977.72 | 2664002977.72 | 1815.36 | 2037.36 | 2259.36 | 2481.36 | 1847 |
29 | KCNFS | SMP | 10 | 1798.24 | 2689798.24 | 26881798.24 | 268801798.24 | 2688001798.24 | 1823.52 | 2047.52 | 2271.52 | 2495.52 | 2876 |
30 | adaptg2wsat+ | 2007-02-08 | 9 | 1458.57 | 2701458.57 | 27001458.57 | 270001458.57 | 2700001458.57 | 1834.81 | 2059.81 | 2284.81 | 2509.81 | 1638 |
31 | adaptg2wsat | 2007-02-08 | 8 | 1288.02 | 2713288.02 | 27121288.02 | 271201288.02 | 2712001288.02 | 1840.70 | 2066.70 | 2292.70 | 2518.70 | |
32 | FH | 2007-02-08 | 8 | 1810.91 | 2713810.91 | 27121810.91 | 271201810.91 | 2712001810.91 | 1842.03 | 2068.03 | 2294.03 | 2520.03 | 1871 |
33 | adaptg2wsat0 | 2007-02-08 | 7 | 681.15 | 2724681.15 | 27240681.15 | 272400681.15 | 2724000681.15 | 1846.37 | 2073.37 | 2300.37 | 2527.37 | 706 |
34 | adaptg2wsatp | 2007-02-08 | 7 | 1145.09 | 2725145.09 | 27241145.09 | 272401145.09 | 2724001145.09 | 1845.92 | 2072.92 | 2299.92 | 2526.92 | 794 |
35 | Hybrid1 | 2007-02-08 | 7 | 1380.60 | 2725380.60 | 27241380.60 | 272401380.60 | 2724001380.60 | 1847.35 | 2074.35 | 2301.35 | 2528.35 | 669 |
36 | ranov | 2007-02-08 | 6 | 2025.90 | 2738025.90 | 27362025.90 | 273602025.90 | 2736002025.90 | 1856.46 | 2084.46 | 2312.46 | 2540.46 | 801 |
37 | UnitMarch | 2007-02-08 | 4 | 1734.50 | 2761734.50 | 27601734.50 | 276001734.50 | 2760001734.50 | 1870.26 | 2100.26 | 2330.26 | 2560.26 | 356 |
38 | TTS | 4.0 | 3 | 13.40 | 2772013.40 | 27720013.40 | 277200013.40 | 2772000013.40 | 1871.02 | 2102.02 | 2333.02 | 2564.02 | 285 |
39 | adaptnovelty | 2007-02-08 | 3 | 1143.10 | 2773143.10 | 27721143.10 | 277201143.10 | 2772001143.10 | 1876.27 | 2107.27 | 2338.27 | 2569.27 | 261 |
40 | KCNFS | 2004 | 2 | 6.57 | 2784006.57 | 27840006.57 | 278400006.57 | 2784000006.57 | 1878.01 | 2110.01 | 2342.01 | 2574.01 | 561 |
41 | gnovelty+ | 2007-02-08 | 2 | 575.18 | 2784575.18 | 27840575.18 | 278400575.18 | 2784000575.18 | 1880.97 | 2112.97 | 2344.97 | 2576.97 | 240 |
42 | saps | 2007-02-08 | 2 | 728.40 | 2784728.40 | 27840728.40 | 278400728.40 | 2784000728.40 | 1881.87 | 2113.87 | 2345.87 | 2577.87 | 215 |
43 | sapsrt | 2007-02-08 | 2 | 1291.78 | 2785291.78 | 27841291.78 | 278401291.78 | 2784001291.78 | 1882.12 | 2114.12 | 2346.12 | 2578.12 | 202 |
44 | Mmisat | 2007-02-08 | 0 | 0.00 | 2808000.00 | 28080000.00 | 280800000.00 | 2808000000.00 | 1893.08 | 2127.08 | 2361.08 | 2595.08 | 0 |
Rank | Solver | Version | Number of solved instances |
Cumulated CPU time on solved instances |
sum(time), penalty=10 | sum(time), penalty=100 | sum(time), penalty=1000 | sum(time), penalty=10000 | sum(log(time)), penalty=10 | sum(log(time)), penalty=100 | sum(log(time)), penalty=1000 | sum(log(time)), penalty=10000 | Purse score |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
1 | adaptg2wsat0 | 2007-02-08 | 231 | 25875.21 | 3385875.21 | 33625875.21 | 336025875.21 | 3360025875.21 | 2478.40 | 2758.40 | 3038.40 | 3318.40 | 68240 |
2 | adaptg2wsat+ | 2007-02-08 | 227 | 22724.01 | 3430724.01 | 34102724.01 | 340822724.01 | 3408022724.01 | 2505.87 | 2789.87 | 3073.87 | 3357.87 | 63729 |
3 | Hybrid1 | 2007-02-08 | 226 | 24345.15 | 3444345.15 | 34224345.15 | 342024345.15 | 3420024345.15 | 2511.29 | 2796.29 | 3081.29 | 3366.29 | 61922 |
4 | adaptg2wsat | 2007-02-08 | 222 | 20570.71 | 3488570.71 | 34700570.71 | 346820570.71 | 3468020570.71 | 2538.35 | 2827.35 | 3116.35 | 3405.35 | |
5 | adaptg2wsatp | 2007-02-08 | 222 | 26237.69 | 3494237.69 | 34706237.69 | 346826237.69 | 3468026237.69 | 2543.44 | 2832.44 | 3121.44 | 3410.44 | 57502 |
6 | FH | 2007-02-08 | 220 | 22428.66 | 3514428.66 | 34942428.66 | 349222428.66 | 3492022428.66 | 2553.08 | 2844.08 | 3135.08 | 3426.08 | 57098 |
7 | adaptnovelty | 2007-02-08 | 218 | 27987.63 | 3543987.63 | 35187987.63 | 351627987.63 | 3516027987.63 | 2577.05 | 2870.05 | 3163.05 | 3456.05 | 59472 |
8 | ranov | 2007-02-08 | 216 | 27044.14 | 3567044.14 | 35427044.14 | 354027044.14 | 3540027044.14 | 2611.27 | 2906.27 | 3201.27 | 3496.27 | 45425 |
9 | SATzilla | RANDOM | 215 | 31979.77 | 3583979.77 | 35551979.77 | 355231979.77 | 3552031979.77 | 2682.94 | 2978.94 | 3274.94 | 3570.94 | 37613 |
10 | March KS | 2007-02-08 | 208 | 36762.87 | 3672762.87 | 36396762.87 | 363636762.87 | 3636036762.87 | 2793.81 | 3096.81 | 3399.81 | 3702.81 | 48842 |
11 | SATzilla | FULL | 205 | 23696.12 | 3695696.12 | 36743696.12 | 367223696.12 | 3672023696.12 | 2731.68 | 3037.68 | 3343.68 | 3649.68 | |
12 | gnovelty+ | 2007-02-08 | 203 | 21409.29 | 3717409.29 | 36981409.29 | 369621409.29 | 3696021409.29 | 2656.19 | 2964.19 | 3272.19 | 3580.19 | 69635 |
13 | KCNFS | 2004 | 191 | 40265.13 | 3880265.13 | 38440265.13 | 384040265.13 | 3840040265.13 | 2915.30 | 3235.30 | 3555.30 | 3875.30 | 40312 |
14 | SATzilla | CRAFTED | 189 | 24417.95 | 3888417.95 | 38664417.95 | 386424417.95 | 3864024417.95 | 2835.54 | 3157.54 | 3479.54 | 3801.54 | 23667 |
15 | KCNFS | 2006 | 189 | 38423.92 | 3902423.92 | 38678423.92 | 386438423.92 | 3864038423.92 | 2929.89 | 3251.89 | 3573.89 | 3895.89 | 38670 |
16 | saps | 2007-02-08 | 169 | 6197.60 | 4110197.60 | 41046197.60 | 410406197.60 | 4104006197.60 | 2855.58 | 3197.58 | 3539.58 | 3881.58 | 32928 |
17 | sapsrt | 2007-02-08 | 167 | 7135.46 | 4135135.46 | 41287135.46 | 412807135.46 | 4128007135.46 | 2865.69 | 3209.69 | 3553.69 | 3897.69 | 37639 |
18 | KCNFS | SMP | 165 | 35051.84 | 4187051.84 | 41555051.84 | 415235051.84 | 4152035051.84 | 3089.13 | 3435.13 | 3781.13 | 4127.13 | 37029 |
19 | DEWSATZ | 2007-04-26 (fixed) | 142 | 38365.15 | 4466365.15 | 44318365.15 | 442838365.15 | 4428038365.15 | 3263.90 | 3632.90 | 4001.90 | 4370.90 | |
20 | minimarch | 2007-04-26 (fixed) | 125 | 36271.09 | 4668271.09 | 46356271.09 | 463236271.09 | 4632036271.09 | 3367.63 | 3753.63 | 4139.63 | 4525.63 | |
21 | MXC | 2007-02-08 | 105 | 28842.42 | 4900842.42 | 48748842.42 | 487228842.42 | 4872028842.42 | 3492.69 | 3898.69 | 4304.69 | 4710.69 | 10478 |
22 | minisat | SAT 2007 | 101 | 27872.79 | 4947872.79 | 49227872.79 | 492027872.79 | 4920027872.79 | 3517.53 | 3927.53 | 4337.53 | 4747.53 | 9724 |
23 | minisat | SAT 2007 (with assertions) | 100 | 27622.24 | 4959622.24 | 49347622.24 | 493227622.24 | 4932027622.24 | 3523.80 | 3934.80 | 4345.80 | 4756.80 | |
24 | SAT7 | 2007-02-08 | 95 | 28423.19 | 5020423.19 | 49948423.19 | 499228423.19 | 4992028423.19 | 3562.23 | 3978.23 | 4394.23 | 4810.23 | 8384 |
25 | DEWSATZ 1A | 2007-02-08 | 84 | 24117.97 | 5148117.97 | 51264117.97 | 512424117.97 | 5124024117.97 | 3629.86 | 4056.86 | 4483.86 | 4910.86 | 8202 |
26 | SAT4J | SAT 2007 | 78 | 19580.72 | 5215580.72 | 51979580.72 | 519619580.72 | 5196019580.72 | 3660.94 | 4093.94 | 4526.94 | 4959.94 | |
27 | MiraXT | v3 | 78 | 25731.14 | 5221731.14 | 51985731.14 | 519625731.14 | 5196025731.14 | 3667.17 | 4100.17 | 4533.17 | 4966.17 | 6659 |
28 | MiraXT | v1 | 74 | 18904.06 | 5262904.06 | 52458904.06 | 524418904.06 | 5244018904.06 | 3680.93 | 4117.93 | 4554.93 | 4991.93 | 6587 |
29 | MiraXT | v2 | 68 | 24496.65 | 5340496.65 | 53184496.65 | 531624496.65 | 5316024496.65 | 3734.36 | 4177.36 | 4620.36 | 5063.36 | 5536 |
30 | picosat | 535 | 67 | 19041.69 | 5347041.69 | 53299041.69 | 532819041.69 | 5328019041.69 | 3723.07 | 4167.07 | 4611.07 | 5055.07 | 5555 |
31 | UnitMarch | 2007-02-08 | 62 | 17324.63 | 5405324.63 | 53897324.63 | 538817324.63 | 5388017324.63 | 3756.27 | 4205.27 | 4654.27 | 5103.27 | 5811 |
32 | CMUSAT BASE | 2007-02-08 | 48 | 9710.38 | 5565710.38 | 55569710.38 | 555609710.38 | 5556009710.38 | 3831.78 | 4294.78 | 4757.78 | 5220.78 | 3922 |
33 | CMUSAT | 2007-02-08 | 46 | 9128.25 | 5589128.25 | 55809128.25 | 558009128.25 | 5580009128.25 | 3844.26 | 4309.26 | 4774.26 | 5239.26 | 3766 |
34 | Rsat | 2007-02-08 | 43 | 7117.74 | 5623117.74 | 56167117.74 | 561607117.74 | 5616007117.74 | 3862.56 | 4330.56 | 4798.56 | 5266.56 | 3603 |
35 | Spear FHS | 1.0 | 40 | 12725.50 | 5664725.50 | 56532725.50 | 565212725.50 | 5652012725.50 | 3892.38 | 4363.38 | 4834.38 | 5305.38 | |
36 | Spear FH | 1.0 | 39 | 12585.65 | 5676585.65 | 56652585.65 | 566412585.65 | 5664012585.65 | 3897.16 | 4369.16 | 4841.16 | 5313.16 | |
37 | Spear | 2007-02-12 | 38 | 7746.95 | 5683746.95 | 56767746.95 | 567607746.95 | 5676007746.95 | 3897.86 | 4370.86 | 4843.86 | 5316.86 | |
38 | TiniSatELite | 2007-02-08 | 32 | 9104.94 | 5757104.94 | 57489104.94 | 574809104.94 | 5748009104.94 | 3933.55 | 4412.55 | 4891.55 | 5370.55 | 2939 |
39 | tinisat | 2007-02-08 | 30 | 5302.66 | 5777302.66 | 57725302.66 | 577205302.66 | 5772005302.66 | 3937.76 | 4418.76 | 4899.76 | 5380.76 | 2884 |
40 | Barcelogic Fixed | 2007-04-13 | 29 | 6332.62 | 5790332.62 | 57846332.62 | 578406332.62 | 5784006332.62 | 3953.36 | 4435.36 | 4917.36 | 5399.36 | |
41 | ornithorynque | 0.1 alpha | 11 | 1459.23 | 6001459.23 | 60001459.23 | 600001459.23 | 6000001459.23 | 4064.36 | 4564.36 | 5064.36 | 5564.36 | |
42 | Mmisat | 2007-02-08 | 1 | 426.37 | 6120426.37 | 61200426.37 | 612000426.37 | 6120000426.37 | 4128.57 | 4638.57 | 5148.57 | 5658.57 | 130 |
43 | TTS | 4.0 | 0 | 0.00 | 6132000.00 | 61320000.00 | 613200000.00 | 6132000000.00 | 4134.03 | 4645.03 | 5156.03 | 5667.03 | 0 |