generated from satcompetition/template
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathresults.html
180 lines (173 loc) · 12.9 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
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title class='tpl-name'></title>
<link rel="stylesheet" href="main.css" type="text/css">
<link rel="stylesheet" href="template.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 class='tpl-name'></h1>
<h2>Results</h2>
<h3>Main Track</h3>
<table class="sortable" style="font-size:8pt">
<tr><th class="sorttable_nosort">Solver<th>Score</th><th>Solved</th><th>Score SAT</th><th>Solved SAT</th><th>Score UNSAT</th><th>Solved UNSAT</th><th>Score Crypto</th><th>Solved Crypto</th></tr>
<tr style='background-color:#c7d6d5'><td>VBS</td><td>2153</td><td>325</td><td>1360</td><td>157</td><td>596</td><td>168</td><td>2126</td><td>164</td></tr>
<tr><td>Kissat_MAB</td><td>3194</td><td>296</td><td>2222</td><td>148</td><td>1816</td><td>148</td><td>4300</td><td>122</td></tr>
<tr><td>Kissat_sc2021_sweep</td><td>3365</td><td>288</td><td>2683</td><td>137</td><td>1697</td><td>151</td><td>4567</td><td>118</td></tr>
<tr><td>kissat_gb</td><td>3366</td><td>289</td><td>2430</td><td>143</td><td>1952</td><td>146</td><td>4530</td><td>116</td></tr>
<tr><td>kissat_crvr_gb</td><td>3398</td><td>288</td><td>2527</td><td>141</td><td>1919</td><td>147</td><td>4708</td><td>113</td></tr>
<tr><td>Kissat_sc2021_default</td><td>3407</td><td>287</td><td>2709</td><td>137</td><td>1755</td><td>150</td><td>4586</td><td>116</td></tr>
<tr><td>hKis_unsat</td><td>3435</td><td>286</td><td>2977</td><td>133</td><td>1543</td><td>153</td><td>4445</td><td>120</td></tr>
<tr><td>kissat_cf</td><td>3508</td><td>282</td><td>2568</td><td>140</td><td>2097</td><td>142</td><td>4601</td><td>116</td></tr>
<tr><td>hKis</td><td>3535</td><td>282</td><td>2697</td><td>137</td><td>2022</td><td>145</td><td>4735</td><td>112</td></tr>
<tr><td>cadical_watch_sat</td><td>3613</td><td>283</td><td>2961</td><td>136</td><td>1915</td><td>147</td><td>4564</td><td>123</td></tr>
<tr><td>CaDiCaL_PriPro</td><td>3627</td><td>279</td><td>3058</td><td>132</td><td>1847</td><td>147</td><td>4627</td><td>118</td></tr>
<tr><td>CaDiCaL_PriPro_no_bin</td><td>3628</td><td>279</td><td>3058</td><td>132</td><td>1847</td><td>147</td><td>4627</td><td>118</td></tr>
<tr><td>Kissat_sc2021_sat</td><td>3636</td><td>278</td><td>2658</td><td>139</td><td>2265</td><td>139</td><td>4675</td><td>115</td></tr>
<tr><td>lstech_maple</td><td>3646</td><td>277</td><td>2358</td><td>144</td><td>2584</td><td>133</td><td>4127</td><td>125</td></tr>
<tr><td>ParaFROST_NoMDM</td><td>3670</td><td>276</td><td>2905</td><td>133</td><td>2084</td><td>143</td><td>4197</td><td>128</td></tr>
<tr><td>cadical_hack_gb</td><td>3674</td><td>279</td><td>2971</td><td>135</td><td>2027</td><td>144</td><td>4526</td><td>122</td></tr>
<tr><td>ParaFROST</td><td>3677</td><td>278</td><td>3024</td><td>132</td><td>1979</td><td>146</td><td>4206</td><td>126</td></tr>
<tr><td>hCaD</td><td>3715</td><td>273</td><td>2743</td><td>135</td><td>2338</td><td>138</td><td>4789</td><td>116</td></tr>
<tr><td>CaDiCaL_sc2021</td><td>3737</td><td>272</td><td>2985</td><td>133</td><td>2139</td><td>139</td><td>4376</td><td>124</td></tr>
<tr><td>Cadical_SCAVEL01</td><td>3798</td><td>274</td><td>3229</td><td>130</td><td>2016</td><td>144</td><td>4807</td><td>118</td></tr>
<tr><td>CaDiCaL_rp</td><td>3841</td><td>272</td><td>3240</td><td>129</td><td>2092</td><td>143</td><td>4390</td><td>126</td></tr>
<tr><td>Relaxed_LCMDCBDL_SCAVEL01</td><td>3843</td><td>269</td><td>2655</td><td>138</td><td>2682</td><td>131</td><td>3896</td><td>130</td></tr>
<tr><td>SLIME_no_hess_no_rnd</td><td>3875</td><td>270</td><td>2744</td><td>138</td><td>2656</td><td>132</td><td>3792</td><td>135</td></tr>
<tr><td>SLIME_hess_no_rnd</td><td>3896</td><td>270</td><td>2729</td><td>137</td><td>2714</td><td>133</td><td>3906</td><td>131</td></tr>
<tr><td>SLIME_hess_rnd</td><td>3978</td><td>267</td><td>2723</td><td>138</td><td>2883</td><td>129</td><td>4065</td><td>129</td></tr>
<tr><td>Maple_simp21</td><td>3996</td><td>266</td><td>3147</td><td>131</td><td>2495</td><td>135</td><td>4792</td><td>113</td></tr>
<tr><td>Maple_MBDR_Cent_PERM_10K</td><td>4000</td><td>266</td><td>2918</td><td>135</td><td>2732</td><td>131</td><td>4152</td><td>126</td></tr>
<tr><td>optsat_R21</td><td>4021</td><td>264</td><td>3310</td><td>127</td><td>2382</td><td>137</td><td>4596</td><td>118</td></tr>
<tr><td>hCaD_psids</td><td>4028</td><td>265</td><td>3967</td><td>115</td><td>1738</td><td>150</td><td>5409</td><td>104</td></tr>
<tr><td>Maple_MBDR_Cent_PERM_75K</td><td>4047</td><td>264</td><td>2957</td><td>134</td><td>2786</td><td>130</td><td>4207</td><td>124</td></tr>
<tr><td>optsat_m21</td><td>4049</td><td>263</td><td>3332</td><td>126</td><td>2416</td><td>137</td><td>4757</td><td>113</td></tr>
<tr><td>SLIME_no_hess_rnd</td><td>4058</td><td>261</td><td>2819</td><td>135</td><td>2946</td><td>126</td><td>3956</td><td>130</td></tr>
<tr><td>cms_expV_gbL</td><td>4063</td><td>263</td><td>3517</td><td>123</td><td>2258</td><td>140</td><td>4128</td><td>127</td></tr>
<tr><td>Relaxed_LCFTP</td><td>4092</td><td>262</td><td>2873</td><td>137</td><td>2962</td><td>125</td><td>4219</td><td>125</td></tr>
<tr><td>kissat_bonus</td><td>4095</td><td>259</td><td>4289</td><td>107</td><td>1552</td><td>152</td><td>4983</td><td>112</td></tr>
<tr><td>hKis_psids</td><td>4099</td><td>261</td><td>4171</td><td>109</td><td>1676</td><td>152</td><td>4802</td><td>114</td></tr>
<tr><td>Cadical_SCAVEL02</td><td>4136</td><td>263</td><td>3082</td><td>133</td><td>2840</td><td>130</td><td>4456</td><td>124</td></tr>
<tr><td>Relaxed_LCFTP_V3</td><td>4157</td><td>258</td><td>2875</td><td>136</td><td>3088</td><td>122</td><td>4234</td><td>124</td></tr>
<tr><td>Relaxed_LCFTP_V2</td><td>4179</td><td>258</td><td>2951</td><td>134</td><td>3056</td><td>124</td><td>4119</td><td>125</td></tr>
<tr><td>Relaxed_LCMDCBDL_BLB</td><td>4180</td><td>255</td><td>3004</td><td>132</td><td>3006</td><td>123</td><td>4130</td><td>127</td></tr>
<tr><td>Relaxed_LCMDCBDL_SCAVEL02</td><td>4465</td><td>249</td><td>3092</td><td>133</td><td>3489</td><td>116</td><td>4589</td><td>119</td></tr>
<tr><td>MapleSSV</td><td>4611</td><td>242</td><td>4215</td><td>107</td><td>2657</td><td>135</td><td>5210</td><td>105</td></tr>
<tr><td>Maple_MBDR_BJL6_Tier2</td><td>6572</td><td>150</td><td>2745</td><td>139</td><td>8048</td><td>11</td><td>4266</td><td>124</td></tr>
<tr><td>Maple_MBDR_BJL7_Local</td><td>6620</td><td>148</td><td>2797</td><td>138</td><td>8093</td><td>10</td><td>4465</td><td>117</td></tr>
<tr><td>CleanMaple</td><td>7037</td><td>142</td><td>6049</td><td>73</td><td>5675</td><td>69</td><td>6954</td><td>76</td></tr>
<tr><td>CleanMaple_PriPro</td><td>7181</td><td>135</td><td>6157</td><td>70</td><td>5855</td><td>65</td><td>6865</td><td>75</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 style='background-color:#c7d6d5'><td>VBS</td><td>1605</td><td>344</td><td>1095</td><td>167</td><td>466</td><td>177</td></tr>
<tr><td>p-mcomsps</td><td>2386</td><td>320</td><td>2292</td><td>147</td><td>829</td><td>173</td></tr>
<tr><td>mallob-parallel</td><td>2411</td><td>318</td><td>2084</td><td>151</td><td>1088</td><td>167</td></tr>
<tr><td>paKis</td><td>2465</td><td>316</td><td>1758</td><td>155</td><td>1522</td><td>161</td></tr>
<tr><td>p-mcomsps-str-sc</td><td>2590</td><td>312</td><td>2255</td><td>148</td><td>1274</td><td>164</td></tr>
<tr><td>p-mcomsps-com</td><td>2591</td><td>313</td><td>2409</td><td>145</td><td>1123</td><td>168</td></tr>
<tr><td>merge-hordesat-parallel</td><td>2777</td><td>305</td><td>1977</td><td>153</td><td>1927</td><td>152</td></tr>
<tr><td>plingeling</td><td>2819</td><td>310</td><td>2528</td><td>146</td><td>1461</td><td>164</td></tr>
<tr><td>painless-maple</td><td>2870</td><td>307</td><td>2358</td><td>146</td><td>1732</td><td>161</td></tr>
<tr><td>abcdsat (disqualified)</td><td>3325</td><td>285</td><td>2569</td><td>142</td><td>2431</td><td>143</td></tr>
<tr><td>abcdpara-scavel</td><td>6491</td><td>155</td><td>9255</td><td>1</td><td>2076</td><td>154</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 style='background-color:#c7d6d5'><td>VBS</td><td>125</td><td>382</td></tr>
<tr style='background-color:#c7d6d5'><td>mallobhc (hors concours)</td><td>373</td><td>337</td></tr>
<tr><td>mallob</td><td>480</td><td>316</td></tr>
<tr><td>merge-hordesat</td><td>858</td><td>260</td></tr>
<tr><td>slime</td><td>914</td><td>245</td></tr>
<tr><td>p-mcompsps-mpi</td><td>973</td><td>230</td></tr>
<tr><td>p-mcomsps-com-mpi</td><td>1049</td><td>211</td></tr>
<tr><td>paracooba</td><td>1122</td><td>197</td></tr>
</table>
<h3>NoLimits Track</h3>
<table style="font-size:10pt" width="100%">
<thead><tr><th>Solver</th></th><th>Score</th><th>Solved</th></tr></thead>
<tr style='background-color:#c7d6d5'><td>VBS</td><td>2134</td><td>326</td></tr>
<tr><td>Kissat_MAB</td><td>3621</td><td>208</td></tr>
<tr><td>kissat_crvr_gb</td><td>3695</td><td>206</td></tr>
<tr><td>kissat_gb</td><td>3722</td><td>204</td></tr>
<tr><td>Kissat_sc2021_default</td><td>3798</td><td>202</td></tr>
<tr><td>lstech_maple</td><td>3813</td><td>203</td></tr>
<tr><td>Kissat_sc2021_sweep</td><td>3816</td><td>201</td></tr>
<tr><td>Kissat_sc2021_sat</td><td>3831</td><td>201</td></tr>
<tr><td>kissat_cf</td><td>3846</td><td>200</td></tr>
<tr><td>hKis</td><td>3849</td><td>201</td></tr>
<tr><td>hKis_unsat</td><td>3856</td><td>201</td></tr>
<tr><td>cadical_watch_sat</td><td>4027</td><td>199</td></tr>
<tr><td>CaDiCaL_PriPro_no_proof</td><td>4049</td><td>196</td></tr>
<tr><td>CaDiCaL_PriPro_no_bin_no_proof</td><td>4050</td><td>196</td></tr>
<tr><td>CaDiCaL_PriPro_no_bin</td><td>4056</td><td>196</td></tr>
<tr><td>CaDiCaL_PriPro</td><td>4056</td><td>196</td></tr>
<tr><td>hCaD</td><td>4106</td><td>192</td></tr>
<tr><td>ParaFROST</td><td>4117</td><td>195</td></tr>
<tr><td>cadical_hack_gb</td><td>4130</td><td>195</td></tr>
<tr><td>Maple_MBDR_BJL6_Tier2</td><td>4139</td><td>195</td></tr>
<tr><td>ParaFROST_NoMDM</td><td>4141</td><td>192</td></tr>
<tr><td>SLIME_hess_no_rnd</td><td>4147</td><td>194</td></tr>
<tr><td>Relaxed_LCMDCBDL_SCAVEL01</td><td>4156</td><td>191</td></tr>
<tr><td>SLIME_no_hess_no_rnd</td><td>4185</td><td>192</td></tr>
<tr><td>Maple_MBDR_BJL7_Local</td><td>4218</td><td>192</td></tr>
<tr><td>Cadical_SCAVEL01</td><td>4246</td><td>191</td></tr>
<tr><td>CaDiCaL_sc2021</td><td>4263</td><td>187</td></tr>
<tr><td>Maple_MBDR_Cent_PERM_10K</td><td>4281</td><td>191</td></tr>
<tr><td>CaDiCaL_rp</td><td>4292</td><td>190</td></tr>
<tr><td>SLIME_hess_rnd</td><td>4298</td><td>190</td></tr>
<tr><td>Maple_MBDR_Cent_PERM_75K</td><td>4305</td><td>190</td></tr>
<tr><td>Maple_simp21</td><td>4331</td><td>189</td></tr>
<tr><td>Relaxed_LCFTP</td><td>4377</td><td>188</td></tr>
<tr><td>Relaxed_LCFTP_V2</td><td>4420</td><td>186</td></tr>
<tr><td>Relaxed_LCFTP_V3</td><td>4423</td><td>185</td></tr>
<tr><td>SLIME_no_hess_rnd</td><td>4427</td><td>184</td></tr>
<tr><td>optsat_R21</td><td>4438</td><td>184</td></tr>
<tr><td>Relaxed_LCMDCBDL_BLB</td><td>4446</td><td>184</td></tr>
<tr><td>cms_expV_gbL</td><td>4463</td><td>185</td></tr>
<tr><td>optsat_m21</td><td>4507</td><td>182</td></tr>
<tr><td>hCaD_psids</td><td>4525</td><td>183</td></tr>
<tr><td>hKis_psids</td><td>4609</td><td>179</td></tr>
<tr><td>Cadical_SCAVEL02</td><td>4667</td><td>181</td></tr>
<tr><td>kissat_bonus</td><td>4697</td><td>174</td></tr>
<tr><td>Relaxed_LCMDCBDL_SCAVEL02</td><td>4832</td><td>174</td></tr>
<tr><td>MapleSSV</td><td>4935</td><td>171</td></tr>
<tr><td>clasp_336_HC_no_proof_handy</td><td>6107</td><td>132</td></tr>
<tr><td>clasp_336_HC_no_proof_tweety</td><td>6302</td><td>123</td></tr>
<tr><td>clasp_336_HC_no_proof</td><td>6347</td><td>123</td></tr>
<tr><td>clasp_336_HC_no_proof_trendy</td><td>6347</td><td>123</td></tr>
<tr><td>clasp_336_HC_no_proof_many</td><td>6359</td><td>122</td></tr>
<tr><td>clasp_336_HC_no_proof_crafty</td><td>6405</td><td>118</td></tr>
<tr><td>clasp_336_HC_no_proof_frumpy</td><td>6476</td><td>114</td></tr>
<tr><td>clasp_336_HC_no_proof_jumpy</td><td>6552</td><td>114</td></tr>
<tr><td>CleanMaple_no_proof</td><td>7262</td><td>99</td></tr>
<tr><td>CleanMaple</td><td>7278</td><td>98</td></tr>
<tr><td>CleanMaple_PriPro_no_proof</td><td>7321</td><td>96</td></tr>
<tr><td>CleanMaple_PriPro</td><td>7323</td><td>96</td></tr>
</table>
</div>
</div>
</body>
</html>