[2M4-OS-11b] OS-11

[2M4-OS-11b-03] A Deterministic Parallel SAT Solver Based on Recorded Order of Clause Exchange

〇Tomoya Anayama¹, Hidetomo Nabeshima¹ (1. University of Yamanashi)

Keywords:Deterministic Parallel SAT Solvers, Portfolio Parallel SAT Solvers

Reproducibility in SAT solvers is important for applications and debugging. However, the implementation of synchronization of clause exchanges is time-consuming when using a parallel SAT solver with reproducibility. To solve this problem, we propose a deterministic parallel SAT solver that can be implemented in a nondeterministic manner for the first solver run and output a file containing the exchange status of learning clauses, and then reproduce the solver from the file for the second and subsequent solvers. As a preliminary experiment, we tested how much the file size differs depending on the file output method. We found that the file size of the method that outputs only the timing of exchanging learning clauses is much smaller than that of the method that outputs only the timing of exchanging learning clauses.