Supplemental materials

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

ManySAT 2.0 with non-det
- Results of 4 threads
- Results of 64 threads
Glucose syrup (corresponding to Fig.1)
- Results of 4 threads
- Results of 64 threads
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.
  - Results on the 4-threads environment

The following graphs contain the results of every solver (corresponding to Fig.2 and Fig.7).

Real time version (corresponding to Fig.3)
- Results of ManySAT and ManyGlucose.
Normalized time version (corresponding to Fig. 5)
- Results of ManySAT and ManyGlucose.

Results of 64 threads (corresponding to Fig.4)
The estimated regression coefficients are written in the source code (in the function initPeriodCoeffs() in parallel/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 in core/Solver.cc and performs promoting a unary watched conflicting clause to the two watched clause.

The following graphs contain the results of every solver (corresponding to Fig.6).

The following graphs correspond to Fig.9.