Table 3 Statistics on proof production and checking given in seconds
From: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
# | Min | p10 | Med | Mean | p90 | Max | |
|---|---|---|---|---|---|---|---|
DRAT check | 81 | 24.564 | 161.947 | 636.053 | 1025.771 | 2675.848 | 3399.476 |
Seq. assembly | 139 | 6.141 | 37.998 | 158.011 | 277.023 | 747.614 | 1571.190 |
Seq. postprocessing | 139 | 0.120 | 1.695 | 13.776 | 31.376 | 87.583 | 231.958 |
Seq. checking | 139 | 0.716 | 7.627 | 60.587 | 140.934 | 368.082 | 1200.319 |
Seq. asm+post+chk | 139 | 7.924 | 62.542 | 242.040 | 449.334 | 1208.350 | 2831.480 |
Par. assembly | 135 | 2.196 | 10.763 | 41.781 | 96.167 | 231.383 | 1054.070 |
Par. postprocessing | 135 | 0.202 | 1.552 | 16.708 | 34.587 | 82.215 | 338.245 |
Par. checking | 135 | 0.867 | 5.157 | 59.240 | 148.206 | 377.040 | 1469.763 |
Par. asm+post+chk | 135 | 3.406 | 18.492 | 113.739 | 278.960 | 697.353 | 2862.080 |
Cld. assembly | 157 | 1.474 | 11.008 | 61.019 | 108.122 | 277.119 | 848.708 |
Cld. postprocessing | 157 | 0.249 | 2.944 | 31.703 | 87.176 | 266.439 | 690.279 |
Cld. checking | 157 | 1.141 | 9.564 | 130.755 | 347.430 | 1006.636 | 2626.983 |
Cld. asm+post+chk | 157 | 3.626 | 36.400 | 217.736 | 542.728 | 1526.270 | 4165.970 |