-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathresults.html
202 lines (193 loc) · 17.1 KB
/
results.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>SAT Competition 2020</title>
<link rel="stylesheet" href="main.css" type="text/css">
<link rel="icon" type="image/x-icon" href="doge2.ico">
<script src="sorttable.js"></script>
<script src="https://www.w3schools.com/lib/w3.js"></script>
<style>
a#results { color:#c20114; }
table thead {
background-color:#c7d6d5;
color:#45503b;
font-weight: bold;
cursor: default;
}
table.sortable th:not(.sorttable_sorted):not(.sorttable_sorted_reverse):not(.sorttable_nosort):after {
content: " \25B4\25BE"
}
</style>
</head>
<body>
<div class="main">
<div class="navigation" w3-include-html="navigation.html"></div>
<script>w3.includeHTML();</script>
<div class="content">
<h1>SAT Competition 2020</h1>
<h2>Results</h2>
<h3>Main Track</h3>
<table class="sortable" style="font-size:8pt">
<tr><th class="sorttable_nosort">Solver</th><th class="sorttable_nosort">Configuration</th><th>Score</th><th>Solved</th><th>Score SAT</th><th>Solved SAT</th><th>Score UNSAT</th><th>Solved UNSAT</th><th>Score Planning</th><th>Solved Planning</th></tr>
<tr><td>Kissat-sc2020-sat</td><td>default</td><td>3926</td><td>264</td><td>3127</td><td>146</td><td>4724</td><td>118</td><td>6773</td><td>73</td></tr>
<tr><td>Kissat-sc2020-default</td><td>default</td><td>4083</td><td>260</td><td>3830</td><td>134</td><td>4335</td><td>126</td><td>6774</td><td>73</td></tr>
<tr><td>Relaxed_LCMDCBDL_newTech</td><td>default</td><td>4179</td><td>253</td><td>2997</td><td>150</td><td>5361</td><td>103</td><td>7512</td><td>59</td></tr>
<tr><td>cryptominisat-ccnr-lsids</td><td>default</td><td>4266</td><td>248</td><td>3262</td><td>144</td><td>5270</td><td>104</td><td>6466</td><td>79</td></tr>
<tr><td>cryptominisat-ccnr</td><td>default</td><td>4278</td><td>250</td><td>3317</td><td>145</td><td>5238</td><td>105</td><td>6471</td><td>79</td></tr>
<tr><td>cadical-alluip-trail</td><td>default</td><td>4428</td><td>250</td><td>3908</td><td>135</td><td>4947</td><td>115</td><td>6406</td><td>80</td></tr>
<tr><td>cadical-alluip</td><td>default</td><td>4429</td><td>250</td><td>3909</td><td>135</td><td>4949</td><td>115</td><td>6409</td><td>80</td></tr>
<tr><td>Relaxed_LCMDCBDL</td><td>default</td><td>4436</td><td>245</td><td>3355</td><td>143</td><td>5517</td><td>102</td><td>7366</td><td>64</td></tr>
<tr><td>cryptominisat-walksat</td><td>default</td><td>4501</td><td>243</td><td>3721</td><td>139</td><td>5281</td><td>104</td><td>6472</td><td>79</td></tr>
<tr><td>cadical-trail</td><td>default</td><td>4554</td><td>243</td><td>4265</td><td>126</td><td>4842</td><td>117</td><td>6650</td><td>79</td></tr>
<tr><td>Kissat-sc2020-unsat</td><td>default</td><td>4560</td><td>238</td><td>4804</td><td>114</td><td>4315</td><td>124</td><td>6622</td><td>74</td></tr>
<tr><td>CaDiCaL-sc2020</td><td>default</td><td>4607</td><td>246</td><td>4368</td><td>130</td><td>4846</td><td>116</td><td>7339</td><td>61</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-f2trc</td><td>default</td><td>5159</td><td>220</td><td>5264</td><td>110</td><td>5054</td><td>110</td><td>7213</td><td>66</td></tr>
<tr><td>Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>5170</td><td>215</td><td>5173</td><td>110</td><td>5167</td><td>105</td><td>7312</td><td>62</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL</td><td>5177</td><td>214</td><td>5244</td><td>107</td><td>5110</td><td>107</td><td>7269</td><td>64</td></tr>
<tr><td>MapleLCMDistChronoBT-f2trc</td><td>default</td><td>5197</td><td>215</td><td>5344</td><td>106</td><td>5051</td><td>109</td><td>7269</td><td>64</td></tr>
<tr><td>MapleLCMDistChronoBT-f2trc-s</td><td>default</td><td>5210</td><td>214</td><td>5430</td><td>104</td><td>4991</td><td>110</td><td>7610</td><td>54</td></tr>
<tr><td>DurianSat</td><td>default</td><td>5257</td><td>210</td><td>5372</td><td>104</td><td>5142</td><td>106</td><td>7176</td><td>66</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-v3</td><td>default</td><td>5258</td><td>211</td><td>5388</td><td>104</td><td>5128</td><td>107</td><td>7240</td><td>65</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL_OVAU_Lin</td><td>5277</td><td>211</td><td>5369</td><td>105</td><td>5185</td><td>106</td><td>7280</td><td>63</td></tr>
<tr><td>Maple_simp</td><td>default</td><td>5305</td><td>208</td><td>5484</td><td>101</td><td>5126</td><td>107</td><td>6754</td><td>73</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PSIDS_DL</td><td>5327</td><td>210</td><td>5467</td><td>104</td><td>5188</td><td>106</td><td>7213</td><td>66</td></tr>
<tr><td>SLIME</td><td>default</td><td>5331</td><td>211</td><td>5502</td><td>104</td><td>5160</td><td>107</td><td>7560</td><td>58</td></tr>
<tr><td>Maple_mix</td><td>default</td><td>5360</td><td>208</td><td>5651</td><td>99</td><td>5069</td><td>109</td><td>6712</td><td>75</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL_OVAU_Exp</td><td>5403</td><td>203</td><td>5564</td><td>98</td><td>5242</td><td>105</td><td>7198</td><td>66</td></tr>
<tr><td>MLCMDChronoBT-DL-Scavel</td><td>default</td><td>5404</td><td>210</td><td>5408</td><td>107</td><td>5400</td><td>103</td><td>7467</td><td>60</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-Scavel01</td><td>default</td><td>5489</td><td>208</td><td>5651</td><td>103</td><td>5326</td><td>105</td><td>7440</td><td>61</td></tr>
<tr><td>MapleCOMSPS_LRB_VSIDS_2</td><td>default_drup</td><td>5498</td><td>199</td><td>5679</td><td>96</td><td>5317</td><td>103</td><td>6772</td><td>73</td></tr>
<tr><td>MapleCOMSPS_LRB_VSIDS_2</td><td>LRB_VSIDS_2_init</td><td>5525</td><td>200</td><td>5779</td><td>96</td><td>5270</td><td>104</td><td>6746</td><td>75</td></tr>
<tr><td>exp_V_MLD_CBT_DL</td><td>default</td><td>5531</td><td>202</td><td>5713</td><td>98</td><td>5349</td><td>104</td><td>7319</td><td>65</td></tr>
<tr><td>Maple_CM+dist+sattime2s+-</td><td>default</td><td>5562</td><td>203</td><td>5386</td><td>105</td><td>5738</td><td>98</td><td>7472</td><td>59</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-Scavel02</td><td>default</td><td>5572</td><td>203</td><td>5766</td><td>99</td><td>5377</td><td>104</td><td>7513</td><td>59</td></tr>
<tr><td>Maple-LCM-Dist-alluip-trail</td><td>default</td><td>5588</td><td>201</td><td>5872</td><td>95</td><td>5305</td><td>106</td><td>7699</td><td>54</td></tr>
<tr><td>exp_V_LGB_MLD_CBT_DL</td><td>default</td><td>5685</td><td>194</td><td>5854</td><td>94</td><td>5516</td><td>100</td><td>7376</td><td>64</td></tr>
<tr><td>exp_V_L_MLD_CBT_DL</td><td>default</td><td>5767</td><td>193</td><td>6124</td><td>89</td><td>5410</td><td>104</td><td>7334</td><td>65</td></tr>
<tr><td>Maple_CMused+dist</td><td>default</td><td>5770</td><td>193</td><td>6135</td><td>89</td><td>5404</td><td>104</td><td>7604</td><td>57</td></tr>
<tr><td>exp_L_MLD_CBT_DL</td><td>default</td><td>5777</td><td>192</td><td>6169</td><td>87</td><td>5384</td><td>105</td><td>7357</td><td>64</td></tr>
<tr><td>Maple_CM+dist</td><td>default</td><td>5845</td><td>188</td><td>6172</td><td>88</td><td>5517</td><td>100</td><td>7510</td><td>59</td></tr>
<tr><td>Maple_CM+dist+simp2--</td><td>default</td><td>5890</td><td>187</td><td>6121</td><td>90</td><td>5660</td><td>97</td><td>7527</td><td>58</td></tr>
<tr><td>upGlucose-3.0_PADC</td><td>default</td><td>6630</td><td>155</td><td>7234</td><td>64</td><td>6027</td><td>91</td><td>7025</td><td>68</td></tr>
<tr><td>glucose3.0</td><td>proofs</td><td>6662</td><td>154</td><td>7145</td><td>67</td><td>6179</td><td>87</td><td>7044</td><td>66</td></tr>
<tr><td>ParaFROST_CBT</td><td>default</td><td>6933</td><td>144</td><td>7547</td><td>59</td><td>6320</td><td>85</td><td>7973</td><td>44</td></tr>
<tr><td>Top36-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7022</td><td>138</td><td>7302</td><td>62</td><td>6742</td><td>76</td><td>7601</td><td>57</td></tr>
<tr><td>Top24-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7023</td><td>138</td><td>7302</td><td>62</td><td>6744</td><td>76</td><td>7577</td><td>58</td></tr>
<tr><td>Top16-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7023</td><td>138</td><td>7303</td><td>62</td><td>6742</td><td>76</td><td>7575</td><td>58</td></tr>
<tr><td>ParaFROST</td><td>default</td><td>7073</td><td>137</td><td>7526</td><td>59</td><td>6621</td><td>78</td><td>8001</td><td>43</td></tr>
<tr><td>PauSat_noproof</td><td>default</td><td>9467</td><td>24</td><td>9355</td><td>15</td><td>9580</td><td>9</td><td>9142</td><td>19</td></tr>
<tr><td>PauSat</td><td>default</td><td>9469</td><td>24</td><td>9357</td><td>15</td><td>9580</td><td>9</td><td>9179</td><td>18</td></tr>
</table>
<h3>Incremental Track</h3>
<table width="100%" style="font-size:10pt">
<thead>
<tr><td></td><th colspan="2">abcdsat-i20</th><th colspan="2">cadicalsc2020</th><th colspan="2">cryptominisat5</th><th colspan="2">Riss-7.1.2</th></tr>
</thead>
<tr><td>bones</td><td> 513 (46) </td><td> 2 </td><td> 631 (43) </td><td> 3 </td><td> <b>390 (46)</b> </td><td> <b>1</b> </td><td> 903 (40) </td><td> 4 </td></tr>
<tr><td>essentials</td><td> 1333 (35) </td><td> 4 </td><td> 1210 (37) </td><td> 2 </td><td> <b>1200 (36)</b> </td><td> <b>1</b> </td><td> 1241 (36) </td><td> 3 </td></tr>
<tr><td>lsp</td><td> 2495 (21) </td><td> 4 </td><td> 1959 (26) </td><td> 3 </td><td> <b>1789 (29)</b> </td><td> <b>1</b> </td><td> 1881 (27) </td><td> 2 </td></tr>
<tr><td>max</td><td> <b>1987 (27)</b> </td><td> <b>1</b> </td><td> 2021 (25) </td><td> 2 </td><td> 2024 (25) </td><td> 3 </td><td> 2021 (25) </td><td> 2 </td></tr>
<tr><td>ijtihad</td><td> 3238 (10) </td><td> 4 </td><td> <b>3002 (13)</b> </td><td> <b>1</b> </td><td> 3079 (12) </td><td> 2 </td><td> 3145 (11) </td><td> 3 </td></tr>
<tr><td>pasar</td><td> 471 (45) </td><td> 2 </td><td> 506 (45) </td><td> 3 </td><td> 969 (38) </td><td> 4 </td><td> <b>386 (46)</b> </td><td> <b>1</b> </td></tr>
<tr><td>final</td><td colspan="2"> 1 </td><td colspan="2"> 1 </td><td colspan="2"> <b>3</b> </td><td colspan="2"> 1 </td></tr>
</table>
<h3>Parallel Track</h3>
<table class="sortable" style="font-size:10pt">
<tr><th class="sorttable_nosort">Solver</th><th>Score</th><th>Solved</th><th>Score SAT</th><th>Solved SAT</th><th>Score UNSAT</th><th>Solved UNSAT</th></tr>
<tr><td>P-MCOMSPS-STR-32</td><td>3316</td><td>283</td><td>2853</td><td>153</td><td>3779</td><td>130</td></tr>
<tr><td>P-MCOMSPS-STR-64</td><td>3714</td><td>271</td><td>3196</td><td>148</td><td>4232</td><td>123</td></tr>
<tr><td>Plingeling</td><td>3743</td><td>269</td><td>3805</td><td>133</td><td>3680</td><td>136</td></tr>
<tr><td>abcd-para-scavel (disqualified)</td><td>3872</td><td>267</td><td>3405</td><td>143</td><td>4338</td><td>124</td></tr>
<tr><td>maplepainlessdc (disqualified)</td><td>3888</td><td>260</td><td>3319</td><td>144</td><td>4457</td><td>116</td></tr>
<tr><td>ManyGlucose-32</td><td>3985</td><td>260</td><td>4076</td><td>130</td><td>3894</td><td>130</td></tr>
<tr><td>painlessmaplevone</td><td>4022</td><td>262</td><td>2913</td><td>154</td><td>5131</td><td>108</td></tr>
<tr><td>ManyGlucose-64</td><td>4036</td><td>258</td><td>4048</td><td>130</td><td>4024</td><td>128</td></tr>
<tr><td>painlessmaplevtwo</td><td>4103</td><td>260</td><td>3082</td><td>151</td><td>5123</td><td>109</td></tr>
<tr><td>syrupscavel</td><td>4433</td><td>243</td><td>4675</td><td>119</td><td>4191</td><td>124</td></tr>
<tr><td>mergesat (disqualified)</td><td>4852</td><td>224</td><td>5043</td><td>109</td><td>4660</td><td>115</td></tr>
<tr><td>mergesatnothp (disqualified)</td><td>4865</td><td>223</td><td>5068</td><td>108</td><td>4661</td><td>115</td></tr>
<tr><td>treengeling</td><td>4903</td><td>225</td><td>4907</td><td>114</td><td>4899</td><td>111</td></tr>
<tr><td>abcdsatptwenty</td><td>5240</td><td>214</td><td>6337</td><td>86</td><td>4142</td><td>128</td></tr>
</table>
<h3>Cloud Track</h3>
<table style="font-size:10pt" width="100%">
<thead>
<tr><th>Solver</th><th>Score</th><th>Solved</th></tr>
</thead>
<tr><td>mallob-mono</td><td>583</td><td>299</td></tr>
<tr><td>TopoSAT2</td><td>706</td><td>278</td></tr>
<tr><td>Slime</td><td>1057</td><td>214</td></tr>
<tr><td>Paracooba</td><td>1440</td><td>133</td></tr>
<tr><td>CTSat</td><td>1499</td><td>111</td></tr>
<tr><td>Paracooba-March</td><td>1708</td><td>63</td></tr>
</table>
<h3>NoLimits Track</h3>
<table style="font-size:10pt" width="100%">
<thead>
<tr><th>Solver</th><th>Configuration</th></th><th>Score</th><th>Solved</th></tr>
</thead>
<tr><td>Kissat-sc2020-sat</td><td>default</td><td>4073</td><td>192</td></tr>
<tr><td>Kissat-sc2020-default</td><td>default</td><td>4394</td><td>185</td></tr>
<tr><td>Relaxed_LCMDCBDL_newTech</td><td>default</td><td>4410</td><td>182</td></tr>
<tr><td>cryptominisat-ccnr-lsids</td><td>default</td><td>4498</td><td>179</td></tr>
<tr><td>cryptominisat-ccnr</td><td>default</td><td>4530</td><td>180</td></tr>
<tr><td>Relaxed_LCMDCBDL</td><td>default</td><td>4629</td><td>177</td></tr>
<tr><td>cryptominisat-ccnr-nolimits</td><td>default</td><td>4675</td><td>175</td></tr>
<tr><td>cryptominisat-ccnr-lsids-nolimits</td><td>default</td><td>4705</td><td>174</td></tr>
<tr><td>cryptominisat-walksat</td><td>default</td><td>4741</td><td>175</td></tr>
<tr><td>cadical-alluip-trail</td><td>default</td><td>4751</td><td>178</td></tr>
<tr><td>cadical-alluip</td><td>default</td><td>4752</td><td>178</td></tr>
<tr><td>cryptominisat-walksat-nolimits</td><td>default</td><td>4760</td><td>176</td></tr>
<tr><td>Kissat-sc2020-unsat</td><td>default</td><td>4854</td><td>169</td></tr>
<tr><td>CaDiCaL-sc2020</td><td>default</td><td>4924</td><td>176</td></tr>
<tr><td>cadical-trail</td><td>default</td><td>5012</td><td>168</td></tr>
<tr><td>Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>5505</td><td>152</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-f2trc</td><td>default</td><td>5513</td><td>156</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL</td><td>5558</td><td>150</td></tr>
<tr><td>abcdsat_n20</td><td>default</td><td>5570</td><td>151</td></tr>
<tr><td>MapleLCMDistChronoBT-f2trc</td><td>default</td><td>5632</td><td>149</td></tr>
<tr><td>MapleLCMDistChronoBT-f2trc-s</td><td>default</td><td>5643</td><td>148</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-v3</td><td>default</td><td>5647</td><td>147</td></tr>
<tr><td>DurianSat</td><td>default</td><td>5668</td><td>146</td></tr>
<tr><td>SLIME</td><td>default</td><td>5703</td><td>148</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL_OVAU_Lin</td><td>5708</td><td>146</td></tr>
<tr><td>optsat_m20</td><td>default</td><td>5713</td><td>149</td></tr>
<tr><td>Maple_mix</td><td>default</td><td>5728</td><td>146</td></tr>
<tr><td>Maple_simp</td><td>default</td><td>5738</td><td>143</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PSIDS_DL</td><td>5755</td><td>145</td></tr>
<tr><td>MLCMDChronoBT-DL-Scavel</td><td>default</td><td>5759</td><td>148</td></tr>
<tr><td>Painless-ExMapleLCMDistChronoBT</td><td>PADC_DL_OVAU_Exp</td><td>5784</td><td>141</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-Scavel01</td><td>default</td><td>5901</td><td>145</td></tr>
<tr><td>exp_V_MLD_CBT_DL</td><td>default</td><td>5956</td><td>139</td></tr>
<tr><td>MapleCOMSPS_LRB_VSIDS_2</td><td>LRB_VSIDS_2_init</td><td>5974</td><td>137</td></tr>
<tr><td>MapleLCMDistChronoBT-DL-Scavel02</td><td>default</td><td>5986</td><td>141</td></tr>
<tr><td>SLIME</td><td>default-no-drup</td><td>6012</td><td>135</td></tr>
<tr><td>Maple_CM+dist+sattime2s+-</td><td>default</td><td>6043</td><td>138</td></tr>
<tr><td>MapleCOMSPS_LRB_VSIDS_2</td><td>default_drup</td><td>6049</td><td>133</td></tr>
<tr><td>Maple-LCM-Dist-alluip-trail</td><td>default</td><td>6157</td><td>134</td></tr>
<tr><td>exp_V_LGB_MLD_CBT_DL</td><td>default</td><td>6227</td><td>130</td></tr>
<tr><td>exp_V_L_MLD_CBT_DL</td><td>default</td><td>6229</td><td>132</td></tr>
<tr><td>exp_L_MLD_CBT_DL</td><td>default</td><td>6259</td><td>130</td></tr>
<tr><td>Maple_CMused+dist</td><td>default</td><td>6309</td><td>129</td></tr>
<tr><td>Maple_CM+dist+simp2--</td><td>default</td><td>6340</td><td>129</td></tr>
<tr><td>Maple_CM+dist</td><td>default</td><td>6370</td><td>126</td></tr>
<tr><td>Riss-nolimit</td><td>NOLIMIT</td><td>7043</td><td>103</td></tr>
<tr><td>Riss</td><td>default_proof</td><td>7085</td><td>103</td></tr>
<tr><td>upGlucose-3.0_PADC</td><td>default</td><td>7110</td><td>101</td></tr>
<tr><td>glucose3.0</td><td>proofs</td><td>7163</td><td>100</td></tr>
<tr><td>ParaFROST_CBT</td><td>default</td><td>7283</td><td>98</td></tr>
<tr><td>Top16-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7418</td><td>91</td></tr>
<tr><td>Top24-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7418</td><td>91</td></tr>
<tr><td>Top36-Undominated-LC-MapleLCMDiscChronoBT-DL</td><td>default</td><td>7419</td><td>91</td></tr>
<tr><td>ParaFROST</td><td>default</td><td>7478</td><td>90</td></tr>
<tr><td>Riss</td><td>NOUNSAT_proof-fixed</td><td>7504</td><td>92</td></tr>
<tr><td>GlucoseEsbpSel</td><td>default</td><td>7644</td><td>84</td></tr>
<tr><td>glucose-3.0-inprocess</td><td>default</td><td>7769</td><td>80</td></tr>
<tr><td>PauSat_noproof</td><td>default</td><td>9483</td><td>18</td></tr>
<tr><td>PauSat</td><td>default</td><td>9484</td><td>18</td></tr>
</table>
</div>
</div>
</body>
</html>