### Parallelizing local search for CNF satisfiability using vectorization and PVMParallelizing local search for CNF satisfiability using vectorization and PVM

Access Restriction
Subscribed

 Author Iwama, Kazuo ♦ Kawai, Daisuke ♦ Miyazaki, Shuichi ♦ Okabe, Yasuo ♦ Umemoto, Jun Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2002 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data Subject Keyword CNF Satisfiability ♦ PVM ♦ Algorithms ♦ Distributed computing ♦ Experimentation ♦ Local search algorithms ♦ Parallelization ♦ Vector supercomputer ♦ Vectorization Abstract The purpose of this paper is to speed up the local search algorithm for the CNF Satisfiability problem. Our basic strategy is to run some $10^{5}$ independent search paths simultaneously using PVM on a vector supercomputer VPP800, which consists of 40 vector processors. Using the 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 ran our parallel GSAT for benchmark instances and compared the running time with those of existing SAT 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 encoding of the class scheduling problem. Again we were able to get almost the best answer in reasonable time. ISSN 10846654 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2002-12-01 Publisher Place New York e-ISSN 10846654 Journal Journal of Experimental Algorithmics (JEA) Volume Number 7 Starting Page 2

#### Open content in new tab

Source: ACM Digital Library