Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-22T04:25:45.420Z Has data issue: false hasContentIssue false
  • English
  • Français

Using sequential runtime distributions for the parallel speedup prediction of SAT local search

Published online by Cambridge University Press:  25 September 2013

ALEJANDRO ARBELAEZ ,
CHARLOTTE TRUCHET  and
PHILIPPE CODOGNET
ALEJANDRO ARBELAEZ
Affiliation:
JFLI / Univesity of Tokyo (e-mail: [email protected])
CHARLOTTE TRUCHET
Affiliation:
LINA, UMR 6241/ University of Nantes (e-mail: [email protected])
PHILIPPE CODOGNET
Affiliation:
JFLI-CNRS / UPMC / University of Tokyo (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper presents a detailed analysis of the scalability and parallelization of local search algorithms for the Satisfiability problem. We propose a framework to estimate the parallel performance of a given algorithm by analyzing the runtime behavior of its sequential version. Indeed, by approximating the runtime distribution of the sequential process with statistical methods, the runtime behavior of the parallel process can be predicted by a model based on order statistics. We apply this approach to study the parallel performance of two SAT local search solvers, namely Sparrow and CCASAT, and compare the predicted performances to the results of an actual experimentation on parallel hardware up to 384 cores. We show that the model is accurate and predicts performance close to the empirical data. Moreover, as we study different types of instances (random and crafted), we observe that the local search solvers exhibit different behaviors and that their runtime distributions can be approximated by two types of distributions: exponential (shifted and non-shifted) and lognormal.

Keywords

SATlocal searchparallelismruntime distributionsstatistical analysis
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 13 , Special Issue 4-5: 29th International Conference on Logic Programming , July 2013 , pp. 625 - 639
Copyright
Copyright © 2013 [ALEJANDRO ARBELAEZ, CHARLOTTE TRUCHET and PHILIPPE CODOGNET] 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

The first author was supported by the Japan Society for the Promotion of Science (JSPS) under the JSPS Postdoctoral Program and the kakenhi Grant-in-aid for Scientific Research.

References

Aiex, R., Resende, M. and Ribeiro, C. 2002. Probability distribution of solution time in GRASP: An experimental investigation. Journal of Heuristics 8, 343–373.CrossRefGoogle Scholar
Aiex, R., Resende, M. and Ribeiro, C. 2007. TTT Plots: A perl program to create time-to-target plots. Optimization Letters 1, 355–366.CrossRefGoogle Scholar
Ansótegui, C., Sellmann, M. and Tierney, K. 2009. A gender-based genetic algorithm for the automatic configuration of algorithms. In 15th International Conference on Principles and Practice of Constraint Programming, Gent, I. P., Ed. LNCS, vol. 5732. Springer, Lisbon, Portugal, 142–157.Google Scholar
Arbelaez, A. and Codognet, P. 2012. Massivelly parallel local search for SAT. In ICTAI'12. IEEE Computer Society, Athens, Greece, 57–64.Google Scholar
Arbelaez, A. and Codognet, P. 2013. From sequential to parallel local search for SAT. In 13th European Conference on Evolutionary Computation in Combinatorial Optimisation (EvoCOP'13), To appear.CrossRefGoogle Scholar
Arbelaez, A. and Hamadi, Y. 2011. Improving parallel local search for SAT. In Learning and Intelligent Optimization, 5th International Conference, LION'11, Coello, C. A. C., Ed. LNCS, vol. 6683. Springer, 46–60.CrossRefGoogle Scholar
Babai, L. 1979. Monte-Carlo algorithms in graph isomorphism testing. Research Report D.M.S. No. 79-10, Université de Montréal.Google Scholar
Balint, A. and Fröhlich, A. 2010. Improving stochastic local search for SAT with a new probability distribution. In SAT'10, Strichman, O. and Szeider, S., Eds. LNCS, vol. 6175. Springer, Edinburgh, UK, 10–15.Google Scholar
Cai, S., Luo, C. and Su, K. 2012. CCASAT: Solver description. In SAT Challenge 2012: Solver and Benchmark Descriptions. Vol. B-2012-2 of Department of Computer Science Series of Publications B. University of Helsinki, 13–14.Google Scholar
David, H. and Nagaraja, H. 2003. Order Statistics. Wiley series in probability and mathematical statistics. Probability and mathematical statistics. John Wiley.CrossRefGoogle Scholar
Hoos, H. and Stütze, T. 2005. Stochastic Local Search: Foundations and Applications. Morgan Kaufmann.Google Scholar
Hoos, H. H. and Stützle, T. 1998. Evaluating las vegas algorithms: Pitfalls and remedies. In Proceedings of the Fourteenth Conference on Uncertainty in Artificial Intelligence, UAI'98. Morgan Kaufmann, 238–245.Google Scholar
Hoos, H. H. and Stützle, T. 1999. Towards a characterisation of the behaviour of stochastic local search algorithms for SAT. Artif. Intell. 112, 1–2, 213–232.Google Scholar
Hutter, F., Hoos, H. H., Leyton-Brown, K. and Stützle, T. 2009. ParamILS: An automatic algorithm configuration framework. Journal of Artificial Intelligence Research 36, 267–306.10.1613/jair.2861CrossRefGoogle Scholar
Kroc, L., Sabharwal, A. and Selman, B. 2010. An empirical study of optimal noise and runtime distributions in local search. In SAT'10, Strichman, O. and Szeider, S., Eds. LNCS, vol. 6175. Springer, Edinburgh, UK, 346–351.Google Scholar
Luby, M., Sinclair, A. and Zuckerman, D. 1993. Optimal speedup of las vegas algorithms. In ISTCS, 128–133.Google Scholar
Maneva, E. and Sinclair, A. 2008. On the satisfiability threshold and clustering of solutions of random 3-SAT formulas. Theoretical Computer Science 407, 1–3, 359–369.CrossRefGoogle Scholar
Martins, R., Manquinho, V. and Lynce, I. 2012. An overview of parallel SAT solving. Constraints 17, 304–347.CrossRefGoogle Scholar
Munoz, P., Barrero, D. and Moreno, M. 2012. Run-time analysis of classical path-planning algorithms. In Proceedings of SGAI 2012, Research and Development in Intelligent Systems XXIX. Springer Verlag, 137–148.Google Scholar
Nadarajah, S. 2008. Explicit expressions for moments of order statistics. Statistics & Probability Letters 78, 2 (Feb.), 196–205.CrossRefGoogle Scholar
Pardalos, P. M., Pitsoulis, L. S., Mavridou, T. D. and Resende, M. G. C. 1995. Parallel search for combinatorial optimization: Genetic algorithms, simulated annealing, tabu search and GRASP. In Parallel Algorithms for Irregularly Structured Problems (IRREGULAR), 317–331.Google Scholar
Pardalos, P. M., Pitsoulis, L. S. and Resende, M. G. C. 1996. A parallel grasp for MAX-SAT problems. In 3rd International Workshop on Applied Parallel Computing, Industrial Computation and Optimization, Wasniewski, J., Dongarra, J., Madsen, K. and Olesen, D., Eds. LNCS. Springer, Lyngby, Denmark.Google Scholar
Pham, D. N. and Gretton, C. 2007. gNovelty+. In Solver Description, SAT Competition 2007.Google Scholar
Ribeiro, C., Rosseti, I. and Vallejos, R. 2012. Exploiting run time distributions to compare sequential and parallel stochastic local search algorithms. Journal of Global Optimization 54, 405–429.CrossRefGoogle Scholar
Shylo, O. V., Middelkoop, T. and Pardalos, P. M. 2011. Restart strategies in optimization: Parallel and serial cases. Parallel Computing 37, 1, 60–68.CrossRefGoogle Scholar
Truchet, C., Richoux, F. and Codognet, P. 2013. Prediction of parallel speed-ups for Las Vegas algorithms. In Proceedings of ICPP-2013, 42nd International Conference on Parallel Processing, Dongarra, J. and Robert, Y., Eds. IEEE Press.Google Scholar
Van Gelder, A. 2011. Careful ranking of multiple solvers with timeouts and ties. In SAT'11, Sakallah, K. and Simon, L., Eds. Lecture Notes in Computer Science, vol. 6695. Springer, Ann Arbor, MI, USA, 317–328.Google Scholar
Verhoeven, M. G. A. 1996. Parallel local search. PhD thesis, University of Eindhoven, Eindhoven, Netherlands.Google Scholar
Verhoeven, M. and Aarts, E. 1995. Parallel local search. Journal of Heuristics 1, 1, 43–65.CrossRefGoogle Scholar
Wolfram, S. 2003. The Mathematica Book, 5th edition. Wolfram Media.Google Scholar
Xu, L., Hutter, F., Hoos, H. H. and Leyton-Brown, K. 2008. Satzilla: Portfolio-based algorithm selection for sat. Journal of Artificial Intelligence Research 32, 565–606.CrossRefGoogle Scholar
Supplementary material: PDF

Arbelaez et al. supplementary material

Appendix

Download Arbelaez et al. supplementary material(PDF)
PDF 132.3 KB