Abstract
The emerging large-scale computational grid infrastructure is providing an interesting platform for massive distributed computations. In this paper a novel distribution method called scattering is introduced for solving SAT problem instances in grid environments. The key advantages of scattering are that it can be used in conjunction with any sequential SAT solver (including industrial black box solvers), the distribution heuristic is strictly separated from the heuristic used in sequential solving, and it requires no communication between processes solving subproblems but still allows coordination of such processes. An implementation of the method has been developed for NorduGrid, a large widely distributed production-level grid running in Scandinavia.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: AAAI/IAAI 1996, pp. 1194–1201. AAAI Press, Menlo Park (1996)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Zhang, H., Bonacina, M., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. J. Symbolic Computation 21(4), 543–560 (1996)
Chrabakh, W., Wolski, R.: GridSAT: A chaff-based distributed SAT solver for the grid. In: SC 2003, IEEE, Los Alamitos (2003)
Jurkowiak, B., Li, C., Utard, G.: A parallelization scheme based on work stealing for a class of SAT solvers. Journal of Automated Reasoning 34(1), 73–101 (2005)
Sinz, C., Blochinger, W., Küchlin, W.: PaSAT — Parallel SAT-checking with lemma exchange: Implementation and applications. In: SAT 2001. Electronic Notes in Discrete Mathematics, vol. 9, pp. 12–13. Elsevier, Amsterdam (2001)
Blochinger, W., Sinz, C., Küchlin, W.: Parallel propositional satisfiability checking with distributed dynamic learning. J. Parallel Computing 29(7), 969–994 (2003)
Forman, S., Segre, A.: NAGSAT: A randomized, complete, parallel solver for 3-SAT. In: SAT (2002), Online Presented at http://gauss.ececs.uc.edu/Conferences/SAT2002/sat2002list.html
Boehm, M., Speckenmeyer, E.: A fast parallel SAT-solver: Efficient workload balancing. Annals of Mathematics and Artificial Intelligence 17(4-3), 381–400 (1996)
Okushi, F.: Parallel cooperative propositional theorem proving. Annals of Mathematics and Artificial Intelligence 26(1-4), 59–85 (1999)
Speckenmeyer, E., Boehm, M., Heusch, P.: On the imbalance of distributions of solutions of CNF-formulas and its impact on satisfiability solvers. In: Satisfiability Problem: Theory and Applications, DIMACS, pp. 669–676 (1997)
Blochinger, W., Westje, W., Küchlin, W., Wedeniwski, S.: ZetaSAT – Boolean satisfiability solving on desktop grids. In: CCGrid 2005, pp. 1079–1086. IEEE, Los Alamitos (2005)
Gomes, C.P., Selman, B., Crato, N., Kautz, H.A.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. Automated Reasoning 24(1/2), 67–100 (2000)
Gomes, C.P., Selman, B.: Algorithm portfolios. Artificial Intelligence 126(1-2), 43–62 (2001)
Eerola, P., et al.: Building a production grid in Scandinavia. IEEE Internet Computing 7(4), 27–35 (2003)
Zhang, L.: SAT-solving: From Davis-Putnam to Zchaff and beyond, lecture notes (2003), Available online at http://research.microsoft.com/users/lintaoz/SATSolving/satsolving.htm
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001, pp. 530–535. ACM, New York (2001)
Hyvärinen, A.E.J.: SATU: A system for distributed propositional satisfiability checking in computational grids. Research Report A100, Helsinki Univ. of Technology, Lab. for Theoretical Comp. Science, Espoo, Finland (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hyvärinen, A.E.J., Junttila, T., Niemelä, I. (2006). A Distribution Method for Solving SAT in Grids. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_39
Download citation
DOI: https://doi.org/10.1007/11814948_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)