{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T08:26:03Z","timestamp":1758270363893},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"unspecified","delay-in-days":86,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1017\/s1471068413000392","type":"journal-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T16:24:58Z","timestamp":1380126298000},"page":"625-639","source":"Crossref","is-referenced-by-count":8,"title":["Using sequential runtime distributions for the parallel speedup prediction of SAT local search"],"prefix":"10.1017","volume":"13","author":[{"given":"ALEJANDRO","family":"ARBELAEZ","sequence":"first","affiliation":[]},{"given":"CHARLOTTE","family":"TRUCHET","sequence":"additional","affiliation":[]},{"given":"PHILIPPE","family":"CODOGNET","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"S1471068413000392_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-012-9121-3"},{"key":"S1471068413000392_ref11","volume-title":"Stochastic Local Search: Foundations and Applications","author":"Hoos","year":"2005"},{"key":"S1471068413000392_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s11590-006-0031-4"},{"key":"S1471068413000392_ref10","doi-asserted-by":"publisher","DOI":"10.1002\/0471722162"},{"key":"S1471068413000392_ref22","volume-title":"3rd International Workshop on Applied Parallel Computing, Industrial Computation and Optimization","author":"Pardalos","year":"1996"},{"key":"S1471068413000392_ref23","unstructured":"Pham D. N. and Gretton C. 2007. gNovelty+. In Solver Description, SAT Competition 2007."},{"key":"S1471068413000392_ref1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015061802659"},{"key":"S1471068413000392_ref4","first-page":"57","volume-title":"ICTAI'12","author":"Arbelaez","year":"2012"},{"key":"S1471068413000392_ref5","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-642-37198-1_14"},{"key":"S1471068413000392_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25566-3_4"},{"key":"S1471068413000392_ref8","first-page":"10","volume-title":"SAT'10","author":"Balint","year":"2010"},{"key":"S1471068413000392_ref9","first-page":"13","volume-title":"SAT Challenge 2012: Solver and Benchmark Descriptions","author":"Cai","year":"2012"},{"key":"S1471068413000392_ref28","unstructured":"Verhoeven M. G. A. 1996. Parallel local search. PhD thesis, University of Eindhoven, Eindhoven, Netherlands."},{"key":"S1471068413000392_ref14","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","article-title":"ParamILS: An automatic algorithm configuration framework.","volume":"36","author":"Hutter","year":"2009","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1471068413000392_ref15","first-page":"346","volume-title":"SAT'10","author":"Kroc","year":"2010"},{"key":"S1471068413000392_ref16","unstructured":"Luby M. , Sinclair A. and Zuckerman D. 1993. Optimal speedup of las vegas algorithms. In ISTCS, 128\u2013133."},{"key":"S1471068413000392_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.06.053"},{"key":"S1471068413000392_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4739-8_10"},{"key":"S1471068413000392_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.spl.2007.05.022"},{"key":"S1471068413000392_ref21","unstructured":"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\u2013331."},{"key":"S1471068413000392_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10898-011-9769-z"},{"key":"S1471068413000392_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2010.08.004"},{"key":"S1471068413000392_ref26","volume-title":"Proceedings of ICPP-2013, 42nd International Conference on Parallel Processing","author":"Truchet","year":"2013"},{"key":"S1471068413000392_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF02430365"},{"key":"S1471068413000392_ref30","volume-title":"The Mathematica Book","author":"Wolfram","year":"2003"},{"key":"S1471068413000392_ref31","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","article-title":"Satzilla: Portfolio-based algorithm selection for sat.","volume":"32","author":"Xu","year":"2008","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1471068413000392_ref3","first-page":"142","volume-title":"15th International Conference on Principles and Practice of Constraint Programming","author":"Ans\u00f3tegui","year":"2009"},{"key":"S1471068413000392_ref27","first-page":"317","volume-title":"SAT'11","author":"Van Gelder","year":"2011"},{"key":"S1471068413000392_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00048-X"},{"key":"S1471068413000392_ref7","unstructured":"Babai L. 1979. Monte-Carlo algorithms in graph isomorphism testing. Research Report D.M.S. No. 79-10, Universit\u00e9 de Montr\u00e9al."},{"key":"S1471068413000392_ref12","first-page":"238","volume-title":"Proceedings of the Fourteenth Conference on Uncertainty in Artificial Intelligence, UAI'98","author":"Hoos","year":"1998"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068413000392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T09:29:27Z","timestamp":1715592567000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068413000392\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":31,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S1471068413000392"],"URL":"https:\/\/doi.org\/10.1017\/s1471068413000392","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}