[4F3-OS-8b] AIと制約プログラミング(2/2)

[4F3-OS-8b-02] A Study on a Framework for Constructing Deterministic Parallel SAT Solvers

〇Tsubasa Fukiage¹, Yuto Obitsu¹, Hidetomo Nabeshima², Xiao-Nan Lu² (1. Department of Computer Science and Engineering,Faculty of Enginnering,University of Yamanashi, 2. Graduate Faculty of Interdisciplinary Research,University of Yamanashi)

Keywords:deterministic parallel SAT solvers, portfolio parallel SAT solvers, general purpose framework

The widespread use of multi-core CPUs has led to the development of parallel SAT solvers, but most of them are nondeterministic. In addition, existing deterministic parallel SAT solvers such as ManyGlucose requires high development cost. In this study, we propose a framework to easily develop a deterministic parallel SAT solver, and show that homogeneous parallel SAT solvers based on this framework achieve the comparable performance with specialized one. Next, we attempted to reduce the latency for synchronization in heterogenous parallel SAT solvers. Our strategies achieve the performance improvement but did not lead to significant reductions in latency in the current stage.