Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM.

Autor: Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, Näher, Stefan, Wagner, Dorothea, Iwama, Kazuo, Kawai, Daisuke, Miyazaki, Shuichi, Okabe, Yasuo, Umemoto, Jun
Zdroj: Algorithm Engineering; 2001, p123-134, 12p
Abstrakt: The purpose of this paper is to speed up the local search algorithm for the CNF Satisfiability problem. Our basic strategys to run some 105 independent search paths simultaneously usingPVM on a vector supercomputer VPP800, which consists of 40 vector processors. Usingthe above parallelization and vectorization together with some improvement of data structure, we obtained 600-times speedup in terms of the number of flips the local search can make per second compared to the original GSAT by Selman and Kautz. We run our parallel GSAT for benchmark instances and compared the runningtime with those of existingSAT programs. We could observe an apparent benefit of parallelization: Especially, we were able to solve two instances that have never been solved before this paper. We also tested parallel local search for the SAT encodingof the class schedulingproblem. Again we were able to get almost the best answer in reasonable time. [ABSTRACT FROM AUTHOR]
Databáze: Supplemental Index