Table 6 Solver performance within 300 s of running time in terms of solved instances, PAR-2 score, and geom. mean speedup over KissatMABHyWalk w.r.t. commonly solved instances
From: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
Nodes | Solver | # | # SAT | # UNSAT | PAR-2 | Speedup |
|---|---|---|---|---|---|---|
seq. | KissatMABHyWalk | 169 | 101 | 68 | 390.8 | 1.0 |
1 | Gimsatul 38-core | 238 | 128 | 110 | 275.8 | 6.6 |
Gimsatul 76-core | 241 | 132 | 109 | 268.6 | 7.4 | |
Proof | 281 | 144 | 137 | 216.8 | 8.4 | |
Proof-like | 287 | 147 | 140 | 207.7 | 8.7 | |
Best | 293 | 149 | 144 | 194.9 | 10.8 | |
20 | Proof | 318 | 156 | 162 | 152.2 | 17.5 |
Proof-like | 321 | 157 | 164 | 146.8 | 20.3 | |
Best | 331 | 162 | 169 | 126.9 | 26.9 |