Supplemental materials
Table of Contents
This page provides the supplemental materials of the following paper:
Hidetomo Nabeshima and Katsumi Inoue: Reproducible Efficient Parallel SAT Solving, SAT 2020, to appear.
In the following, we provide the source code of ManyGlucose and the interactive version of graphs in our paper.
1 Source code of ManyGlucose
2 Comparison of the best and worst results
- ManySAT 2.0 with non-det
- Glucose syrup (corresponding to Fig.1)
- ManyGlucose (corresponding to Fig.8)
- Results of 4 threads
- Results of 64 threads
- Log files of above experiments:
- Glucose simp 4.1
- To show the runtime variance in the 4-threads environment (4-core Intel Core i5-6600 (3.3 GHz) machine), we executed Glucose simp v4.1 (a single-threaded deterministic SAT solver) three times.
The number of solved instances is as follows:
Solver # of solved instances Glucose simp 4.1 417 (229 + 188) Glucose simp 4.1 417 (229 + 188) Glucose simp 4.1 416 (228 + 188) - Comparison of runtimes of the best and worst results of Glucoses imp for each instance.
3 Waiting time ratio
The following graphs contain the results of every solver (corresponding to Fig.2 and Fig.7).
4 Distribution of period execution time
- Real time version (corresponding to Fig.3)
- Results of ManySAT and ManyGlucose.
- Normalized time version (corresponding to Fig. 5)
- Results of ManySAT and ManyGlucose.
5 Predicted time of thread execution time
- Results of 64 threads (corresponding to Fig.4)
- The estimated regression coefficients are written in the source
code (in the function
initPeriodCoeffs()
inparallel/ParallelSolver.cc
).- 12 coefficients out of 29 code blocks became zero.
- The largest coefficient among the remained 17 code blocks is for
the code block "
UnaryPropConfClauseLoopCount
" which is located at line 1494-1521 incore/Solver.cc
and performs promoting a unary watched conflicting clause to the two watched clause.
6 Cactus plots of solved instances
The following graphs contain the results of every solver (corresponding to Fig.6).
7 Clause exchanging time
The following graphs correspond to Fig.9.