DPS: A Framework for Deterministic Parallel SAT Solvers
Table of Contents
This page provides the supplemental materials of the following paper:
Hidetomo Nabeshima, Tsubasa Fukiage, Yuto Obitsu, Xiao-Nan Lu and Katsumi Inoue: DPS: A Framework for Deterministic Parallel SAT Solvers, to be appeared in POS-2022.
# of Solved Instances
The following results correspond to Table 1 in the paper, with some additional results.
| Solver | 2019 | 2020 | 2021 | Total | PAR-2 |
|---|---|---|---|---|---|
| 148 + 98 | 104 + 112 | 130 + 146 | 738 (382 + 356) | 5235522 | |
| Glucose-syrup | 145 + 95 | 104 + 113 | 132 + 141 | 730 (381 + 349) | 5286075 |
| 145 + 96 | 109 + 112 | 130 + 136 | 728 (384 + 344) | 5283988 | |
| 156 + 107 | 118 + 124 | 134 + 166 | 805 (408 + 397) | 4604576 | |
| P-MCOMSPS | 152 + 105 | 115 + 123 | 131 + 168 | 794 (398 + 396) | 4697998 |
| 155 + 107 | 107 + 124 | 134 + 167 | 794 (396 + 398) | 4707163 | |
| 149 + 84 | 118 + 108 | 133 + 132 | 724 (400 + 324) | 5337198 | |
| NPS-MiniSAT (added) | 152 + 84 | 113 + 111 | 131 + 130 | 721 (396 + 325) | 5363882 |
| 149 + 85 | 116 + 110 | 132 + 129 | 721 (397 + 324) | 5336954 | |
| 145 + 107 | 109 + 125 | 130 + 164 | 780 (384 + 396) | 4785702 | |
| NPS-Glucose (added) | 144 + 106 | 108 + 124 | 133 + 165 | 780 (385 + 395) | 4792622 |
| 141 + 106 | 106 + 123 | 129 + 164 | 769 (376 + 393) | 4872116 | |
| 160 + 105 | 135 + 123 | 139 + 168 | 830 (434 + 396) | 4386010 | |
| NPS-MCOMSPS | 159 + 104 | 140 + 121 | 137 + 168 | 829 (436 + 393) | 4352294 |
| 163 + 105 | 126 + 122 | 138 + 167 | 821 (427 + 394) | 4451212 | |
| 175 + 114 | 178 + 134 | 154 + 168 | 923 (507 + 416) | 3245708 | |
| NPS-Kissat | 173 + 114 | 175 + 134 | 155 + 168 | 919 (503 + 416) | 3266045 |
| 170 + 115 | 175 + 134 | 155 + 168 | 917 (500 + 417) | 3296766 | |
| NPS-Kissat no-exchange (added) | 171 + 69 | 173 + 100 | 152 + 128 | 793 (496 + 297) | 4646767 |
| ManySAT | 136 + 79 | 95 + 106 | 119 + 119 | 654 (350 + 304) | 6053978 |
| ManyGlucose-lit | 146 + 107 | 110 + 120 | 130 + 143 | 756 (386 + 370) | 5084256 |
| ManyGlucose-blk | 149 + 108 | 117 + 121 | 132 + 149 | 776 (398 + 378) | 4935944 |
| DPS-MiniSAT | 145 + 74 | 109 + 107 | 124 + 121 | 680 (378 + 302) | 5783256 |
| DPS-Glucose | 142 + 103 | 104 + 122 | 130 + 157 | 758 (376 + 382) | 5018397 |
| DPS-MCOMSPS | 156 + 101 | 129 + 119 | 137 + 166 | 808 (422 + 386) | 4636427 |
| 168 + 112 | 170 + 130 | 157 + 167 | 904 (495 + 409) | 3451073 | |
| DPS-Kissat | 168 + 112 | 170 + 130 | 157 + 167 | 904 (495 + 409) | 3451074 |
| 168 + 112 | 170 + 130 | 157 + 167 | 904 (495 + 409) | 3451445 | |
| DPS-Kissat no-exchange (added) | 168 + 64 | 168 + 95 | 150 + 115 | 760 (486 + 274) | 4924475 |
| DPS-Kissat no-elim (added) | 166 + 113 | 176 + 131 | 153 + 167 | 906 (495 + 411) | 3417151 |
| DPS-Kissat elim (added) | 168 + 111 | 173 + 131 | 153 + 161 | 897 (494 + 403) | 3524412 |
| VBS | 181 + 120 | 187 + 140 | 159 + 176 | 963 (527 + 436) | 2713047 |
- NPS-MiniSAT and NPS-Glucose results have been added.
- NPS and DPS-Kissat no-exchange are the result of disabling clause exchange. Clause exchange is very effective for unsatisfiable instances, and a bit effective for satisfiable instances.
- In DPS-Kissat, half of the workers disabled the Kissat elimination technique by default. We have added the results when all workers used the elimination (DPS-Kissat-elim) and when it was not used (DPS-Kissat-no-elim). The effect of the elimination technique depends on the given instances. See DPS-Kissat-elim vs. DPS-Kissat-no-elim.
The following CSV file contains all results summarized in the above Table.
Waiting time ratio
The following results correspond to Table 2 in the paper, with some additional results.
| Solver | Waiting time ratio |
|---|---|
| ManySAT | 41.1% |
| ManyGlucose-lit | 21.7% |
| ManyGlucose-blk | 10.3% |
| DPS-MiniSAT | 10.4% |
| DPS-Glucose | 9.9% |
| DPS-MCOMSPS | 12.4% |
| DPS-Kissat | 15.0% |
| DPS-Kissat no-exchange | 12.3% |
| DPS-Kissat no-elim | 13.1% |
| DPS-Kissat elim | 15.8% |
- Waiting time ratio (Fig.4)
Exchanging time ratio
The following results show the clause exchaning time ratio.
| Solver | Exchaning time ratio |
|---|---|
| ManySAT | 1.8% |
| ManyGlucose-lit | 0.7% |
| ManyGlucose-blk | 0.7% |
| DPS-MiniSAT | 0.3% |
| DPS-Glucose | 0.4% |
| DPS-MCOMSPS | 0.3% |
| DPS-Kissat | 0.3% |
| DPS-Kissat no-elim | 0.6% |
| DPS-Kissat elim | 0.5% |
CDF Plots
The followings are interactive graphs described in the paper, with some additional graphs.
Runtime (Fig.3)
Propagation speed
The following graph shows the propagation speed (number of literals propagated per second; averaged for each worker per instance) in our parallel SAT solvers.
Period speed
The following graph shows the period speed (number of periods per second; averaged for each worker per instance) in our parallel SAT solvers.
Comparison of two solvers
- ManySAT vs. DPS-MiniSAT
- Glucose-syrup vs. DPS-Glucose
- ManyGlucose-lit vs. DPS-Glucose
- ManyGlucose-blk vs. DPS-Glucose
- Painless-MapleCOMSPS vs. DPS-MapleCOMSPS
- NPS-Kissat vs. DPS-Kissat (Fig.6)
- DPS-Kissat vs. DPS-Kissat-no-elim
- DPS-Kissat vs. DPS-Kissat-elim
- NPS-Kissat vs. NPS-Kissat-no-exchange
- DPS-Kissat vs. DPS-Kissat-no-exchange
- DPS-Kissat-elim vs. DPS-Kissat-no-elim
Comparison of best and worst cases
- Glucose-syrup-best vs. Glucose-syrup-worst
- Painless-MapleCOMSPS-best vs. Painless-MapleCOMSPS-worst
- NPS-MiniSAT-best vs. NPS-MiniSAT-worst
- NPS-Glucose-best vs. NPS-Glucose-worst
- NPS-MCOMSPS-best vs. NPS-MCOMSPS-worst
- NPS-Kissat-best vs. NPS-Kissat-worst (Fig.5 (a))
- DPS-Kissat-best vs. DPS-Kissat-worst (Fig.5 (b))