 | The ACM Journal of Experimental Algorithmics |
Volume 7, Article 2, 2002
Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM
by
and
and
and
and
http://www.jea.acm.org/2002/IwamaSatisfiability/
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
105 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.
- Sources:
- The LaTeX version of the article;
this is a Unix file that contains the LaTeX source;
note that you must be a subscriber (institutional or individual) to access this file.
- The Postscript
version or PDF
version of the article;
note that you must be a subscriber (institutional or individual) to access
these files.
- The HTML version of the article;
note that you must be a subscriber (institutional or individual) to access
this file.
- The software suite accompanying the
article; this is a small Unix tar file, which includes the source code,
a Makefile, and the test files used in the article.
- The bibliography given in the article.
Received
|
Accepted
|
Final Revision
|
Published
|
|
|
|
|
Last updated and validated May 11, 2002, by editor@jea.acm.org