Partitioning Search Spaces of a Randomized Search

• Autorzy: Hyvärinen A. E. J. , Junttila T. , Niemelä I.
• Języki publikacji: EN

Abstrakty

EN

This paper studies the following question: given an instance of the propositional satisfiability problem, a randomized satisfiability solver, and a cluster of n computers, what is the best way to use the computers to solve the instance? Two approaches, simple distribution and search space partitioning as well as their combinations are investigated both analytically and empirically. It is shown that the results depend heavily on the type of the problem (unsatisfiable, satisfiable with few solutions, and satisfiable with many solutions) as well as on how good the search space partitioning function is. In addition, the behavior of a real search space partitioning function is evaluated in the same framework. The results suggest that in practice one should combine the simple distribution and search space partitioning approaches.

Słowa kluczowe

EN

SAT solving; randomized search; distributed constraint-based search

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 2/3
• Strony: 289--311
• Opis fizyczny: Bibliogr. 38 poz., tab., wykr.

Twórcy

autor

Hyvärinen A. E. J.

autor

Junttila T.

autor

Niemelä I.

• Aalto University Department of Information and Computer Science P.0.Box 15400, FI-00076 AALTO, Finland,

Bibliografia

• [1] Blochinger, W., Sinz, C., Küchlin, W.: Parallel Propositional Satisfiability Checking with Distributed Dynamic Learning, Parallel Computing, 29(7), 2003, 969-994.
• [2] Böhm, M., Speckenmeyer, E.: A Fast Parallel SAT-solver: Efficient workload balancing, Annals of Mathematics and Artificial Intelligence, 17(4-3), 1996, 381-400.
• [3] Bordeaux, L., Hamadi, Y., Samulowitz, H.: Experiments with Massively Parallel Constraint Solving, Proceedings of the 21st International Joint Conference on Artificial Intelligence, 2009.
• [4] Chrabakh, W., Wolski, R.: GridSAT: a System for Solving Satisfiability Problems using a Computational Grid, Parallel Computing, 32(9), 660-687.
• [5] Chu, G., Stuckey, P. J.: PMiniSat - A parallelization of MiniSat 2.0, SAT Race 2008 system description, 2008, http://baldur.iti.uka.de/sat-race-2008/descriptions/solver_32.pdf.
• [6] Dequen, G., Vander-Swalmen, P.: Toward Easy Parallel SAT Solving, 21st IEEE International Conference on Tools with Artificial Intelligence, IEEE Computer Society, 2009.
• [7] Eén, N., Sörensson, N.: An Extensible SAT-solver, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers, 2919, Springer, 2004.
• [8] Gil, L., Flores, P., Silveira, L. M.: PMSat: a parallel version of MiniSAT, Journal on Satisfiability, Boolean Modeling and Computation, 6, 2008, 71-98.
• [9] Gomes, C. P., Selman, B.: Algorithm portfolios, Artificial Intelligence, 126(1-2), 2001, 43-62.
• [10] Gomes, C. P., Selman, B., Crato, N., Kautz, H. A.: Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems, Journal of Automated Reasoning, 24(1/2), 2000, 67-100.
• [11] Grama, A., Kumar, V.: State of the Art in Parallel Search Techniques for Discrete Optimization Problems, IEEE Transactions on Knowledge and Data Engineering, 11(1), 1999, 28-34.
• [12] Hamadi, Y., Jabbour, S., Sais, L.: Control-based Clause Sharing in Parallel SAT Solving, Proceedings of the 21st International Joint Conference on Artificial Intelligence, 2009.
• [13] Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a Parallel SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, 6, 2009, 245 - 262.
• [14] Huberman, B. A., Lukose, R. M., Hogg, T.: An Economics Approach to Hard Computational Problems, Science, 275(5296), 1997, 51-54.
• [15] Hyvärinen, A. E. J.: Approaches to Grid-Based SAT Solving, Research Report TKK-ICS-R16, Helsinki University of Technology, June 2009.
• [16] Hyvärinen, A. E. J., Junttila, T., Niemelä, I.: A Distribution Method for Solving SAT in Grids, 9th International Conference on Theory and Applications of Satisfiability Testing, 4121, Springer, 2006.
• [17] Hyvärinen, A. E. J., Junttila, T., Niemelä, I.: Strategies for Solving SAT in Grids by randomized search, Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation, 5144, Springer, 2008.
• [18] Hyvärinen, A. E. J., Junttila, T., Niemelä, I.: Incorporating Clause Learning in Grid-Based Randomized SAT Solving, Journal on Satisfiability, Boolean Modeling and Computation, 6, 2009, 223-244.
• [19] Hyvärinen, A. E. J., Junttila, T., Niemelä, I.: Partitioning Search Spaces of a Randomized Search, AI*IA 2009 International conference of the Italian Association for Artificial Intelligence, 5883, Springer, 2009.
• [20] Hyvärinen, A. E. J., Junttila, T., Niemelä, I.: Partitioning SAT Instances for Distributed Solving, 17th International Conference on Logic Programming, Artificial Intelligence, and Reasoning, 6397, Springer, 2010.
• [21] Inoue, K., Soh, T., Ueda, S., Sasaura, Y., Banbara, M., Tamura, N.: A competitive and cooperative approach to propositional satisfiability, Discrete Applied Mathematics, 154(16), 2006, 2291-2306.
• [22] Janakiram, V. K., Agrawal, D. P., Mehrotra, R.: A Randomized Parallel Backtracking Algorithm, IEEE Transactions on Computers, 37(12), December 1988, 1665-1676.
• [23] Janakiram, V. K., Gehringer, E. F., Agrawal, D. P., Mehrotra, R.: A Randomized Parallel Branch-and-Bound Algorithm, International Journal of Parallel Programming, 17(3), 1988, 277-301.
• [24] 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), 2005, 73-101.
• [25] Lai, T.-H., Sahni, S.: Anomalies in Parallel Branch-and-Bound Algorithms, Communications of the ACM, 27(6), 1984, 594 - 602.
• [26] Lewis, M., Marin, P., Schubert, T., Narizzano, M., Becker, B., Giunchiglia, E.: PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing, 12th International Conference on Theory and Applications of Satisfiability Testing, 5584, Springer, 2009.
• [27] Li, G.-J., Wah, B. W.: Computational Efficiency of Parallel Combinatorial OR-Tree Searches, IEEE Transactions on Software Engineering, 16(1), 1990, 13-31.
• [28] Luby, M., Ertel, W.: Optimal Parallelization of Las Vegas Algorithms, 11th Annual Symposium on Theoretical Aspects of Computer Science, 775, Springer, 1994.
• [29] Luby, M., Sinclair, A., Zuckerman, D.: Optimal Speedup of Las Vegas Algorithms, Information Processing Letters, 47(4), 1993, 173-180.
• [30] Ohmura, K., Ueda, K.: c-sat: A Parallel SAT Solver for Clusters, 12th International Conference on Theory and Applications of Satisfiability Testing, 5584, Springer, 2009.
• [31] Prestwich, S., Mudambi, S.: Improved Branch and Bound in Constraint Logic Programming, First International Conference on Principles and Practice of Constraint Programming, 976, Springer, 1995.
• [32] Rao, V. N., Kumar, V.: Superlinear Speedup in Parallel State-Space Search, 8th ARCS Conference on Foundations of Software Technology and Theoretical Computer Science, 338, Springer, 1988.
• [33] Rao, V. N., Kumar, V.: On the Efficiency of Parallel Backtracking, IEEE Transactions on Parallel and Distributed Systems, 4(4), 1993, 427 - 437.
• [34] Schubert, T., Lewis, M., Becker, B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing, Journal on Satisfiability, Boolean Modeling and Computation, 6, 2009, 203-222.
• [35] Segre, A. M., Forman, S. L., Resta, G., Wildenberg, A.: Nagging: A scalable fault-tolerant paradigm for distributed search, Artificial Intelligence, 140(1/2), 2002, 71-106.
• [36] Speckenmeyer, E., Monien, B., Vornberger, O.: Superlinear Speedup for Parallel Backtracking, 1st International Conference on Supercomputing, 297, Springer, 1998.
• [37] V´eron, A., Schuerman, K., Reeve, M., Li, L.-L.: Why and How in the ElipSys OR-parallel CLP System, Proceedings of the 5th International PARLE Conference, 694, Springer, 1993.
• [38] Zhang, H., Bonacina, M., Hsiang, J.: PSATO: A Distributed Propositional Prover and its Application to Quasigroup Problems, Journal of Symbolic Computation, 21(4), 1996, 543-