Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asahiro, Y., Iwama, K. and Miyano, E.,“Random Generation of Test Instances with Controlled Attributes,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.377–393, 1996.
Cha, B. and Iwama, K.,“Performance test of local search algorithms using new types of random CNF formulas,” Proc.IJCAI-95, pp.304–310, 1995.
Cha, B. and Iwama, K.,“Adding new clauses for faster local search,” Proc.AAAI 96, pp.332–337, 1996.
Cha, B., Iwama, K., Kambayashi, Y. and Miyazaki, S.,“Local search algorithms for Partial MAXSAT,” Proc.AAAI-97, pp.263–268, 1997.
Cheeseman, P., Kanefsky, B. and Taylor W.M.,“Where the really hard problems are,” Proc.IJCAI-91, pp.331–337, 1991.
Dubois, O., Andre, P., Boufkhad, Y. and Carlier, J.“SAT versus UNSAT,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.415–436, 1996.
Geist, A., Berguelin, A., Dongarra, J., Jiang, W., Manchek, R. and Sunderam, V., Parallel Virtual Machine, The MIT Press, 1994.
Gelder, A.V. and Tsuji, Y.K.“Satisfiability testing with more reasoning and less guessing,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.5590–586, 1996.
Gent, I., and Walsh, T.,“Unsatisfied variables in local search,” Hybrid Problems, Hybrid Solutions (AISB-95), Amsterdam, 1995.
Gu, J.“Efficient local search for very large-scale satisfiability problems,”Sigart Bulletin, Vol.3, No.1, pp.8–12, 1992.
Hampson, S. and Kibler, D.“Large plateaus and plateau search n boolean satisfiability problems: When to give up searching and start again,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.437–455, 1996.
Hiraishi, H., Hamaguchi, K., Ochi, H. and Yajima, S.,“Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification,” Proc. CAV’ 91 (LNCS 575), pp.214–224, 1991.
Johnson, D.S. and Trick, M.A. Eds.“Cliques,Coloring,and Satisfiability,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, 1996.
Jaumard, B., Stan, M. and Desrosiers, J.,“Tabu search and a quadratic relaxation for satisfiability problem,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.457–478, 1996.
Koutsoupias, E. and Papadimitriou, C.H.,“On the greedy algorithm for satisfiability,” Information Processing Letters, Vol.43, pp.53–55, 1992.
Mitchell, D., Selman, B. and Levesque, H.,“Hard and easy distributions of SAT problems,” Proc.AAAI-92, pp.459–465, 1992.
Miyazaki, S., Iwama, K. and Kambayashi, Y.,“Database queries as combinatorial optimization problems,” Proc.CODAS’ 96, pp.448–454, 1996.
Morris, P.,“The breakout method for escaping from local minima,” Proc.AAAI-93, pp.40–45, 1993.
Papadimitriou, C.H.,“On selecting a satisfying truth assignment,” Proc. FOCS’ 91, pp.163–169, 1991.
Pretolani, D.,“Efficiency and sability of hypergraph SAT algorithms,” in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.479–498, 1996.
Resende, M.G.C. and Feo, T.A.,“A GRASP for satisfiability,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.499–520, 1996.
Schoning, U,“A probabilistic algorithm for k-SAT and constraint satisfaction problems,” Proc.FOCS’ 99, pp.410–414, 1999.
Selman, B.and Kautz, H., GSAT USER’s GUIDE Version 35, ftp://ftp.research.att.com/dist/ai/GSAT_USERS_GUIDE,1993.
Selman, B. and Kautz, H.,“An empirical study of greedy local search for satisfiability testing,” Proc.AAAI-93, pp.46–51, 1993.
Selman, B. and Kautz, H.,“Local search strategies for satisfiability testing,” 2nd DIMACS Challenge Workshop, 1993.
Selman, B., Levesque, H.J. and Mitchell, D.G.,“A new method for solving hard satisfiability problems,” Proc.AAAI-92, pp.440–446, 1992.
Selman, B., Kautz, H. and Cohen, B.,“Local Search Strategies for Satisfiability Testing,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science,volume 26, American Mathematical Society, pp.521–531, 1996.
Spears, W.M.“Simulated annealingfor hard satisfiability problems,” DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 26, American Mathematical Society, pp.533–557, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Iwama, K., Kawai, D., Miyazaki, S., Okabe, Y., Umemoto, J. (2001). Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM. In: Näher, S., Wagner, D. (eds) Algorithm Engineering. WAE 2000. Lecture Notes in Computer Science, vol 1982. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44691-5_11
Download citation
DOI: https://doi.org/10.1007/3-540-44691-5_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42512-0
Online ISBN: 978-3-540-44691-0
eBook Packages: Springer Book Archive