Vectorized Local Search for CNF Satisfiability

摘要

The purpose of this paper is to speed up the local search algorithm for CNF Satisfiability problem by implementation techniques and parallelization. We selected GSAT by Selman and Kautz and attempted speedup by the following techniques: (i) An improvement of the data structure of Selman and Kautz's implementation. (ii) Vectorization on a parallel vector super- computer. (iii) Parallelization using Parallel Virtual Machine (PVM). By these attempts, we achieved 600-times speedup in total.