{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:47Z","timestamp":1750220027673,"version":"3.41.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2022,12,13]],"date-time":"2022-12-13T00:00:00Z","timestamp":1670889600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM J. Exp. Algorithmics"],"published-print":{"date-parts":[[2022,12,31]]},"abstract":"<jats:p>The satisfiability problem (SAT) is one of the most famous problems in computer science. Traditionally, its NP-completeness has been used to argue that SAT is intractable. However, there have been tremendous practical advances in recent years that allow modern SAT solvers to solve instances with millions of variables and clauses. A particularly successful paradigm in this context is stochastic local search (SLS).<\/jats:p>\n          <jats:p>\n            In most cases, there are different ways of formulating the underlying SAT problem. While it is known that the precise formulation of the problem has a significant impact on the runtime of solvers, finding a helpful formulation is generally non-trivial. The recently introduced\n            <jats:monospace>GapSAT<\/jats:monospace>\n            solver\u00a0[Lorenz\u00a0and\u00a0W\u00f6rz\u00a02020] demonstrated a successful way to improve the performance of an SLS solver on average by learning additional information, which logically entails from the original problem. Still, there were also cases in which the performance slightly deteriorated. This justifies in-depth investigations into how learning logical implications affects runtimes for SLS algorithms.\n          <\/jats:p>\n          <jats:p>\n            In this work, we propose a method for generating logically equivalent problem formulations, generalizing the ideas of\n            <jats:monospace>GapSAT<\/jats:monospace>\n            . This method allows a rigorous mathematical study of the effect on the runtime of SLS SAT solvers. Initially, we conduct empirical investigations. If the modification process is treated as random, then Johnson SB distributions provide a perfect characterization of the hardness. Since the observed Johnson SB distributions approach lognormal distributions, our analysis also suggests that the hardness is long-tailed.\n          <\/jats:p>\n          <jats:p>\n            As a second contribution, we theoretically prove that restarts are useful for long-tailed distributions. This implies that incorporating additional restarts can further refine\n            <jats:italic>all<\/jats:italic>\n            algorithms employing above mentioned modification technique.\n          <\/jats:p>\n          <jats:p>Since the empirical studies compellingly suggest that the runtime distributions follow Johnson\u00a0SB distributions, we also investigate this property on a theoretical basis. We succeed in proving that the runtimes for the special case of Sch\u00f6ning\u2019s random walk algorithm\u00a0[Sch\u00f6ning\u00a02002] are approximately Johnson\u00a0SB distributed.<\/jats:p>","DOI":"10.1145\/3569170","type":"journal-article","created":{"date-parts":[[2022,10,26]],"date-time":"2022-10-26T14:11:24Z","timestamp":1666793484000},"page":"1-38","source":"Crossref","is-referenced-by-count":0,"title":["Toward an Understanding of Long-tailed Runtimes of SLS Algorithms"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9554-4347","authenticated-orcid":false,"given":"Jan-Hendrik","family":"Lorenz","sequence":"first","affiliation":[{"name":"Institute of Theoretical Computer Science, Universit\u00e4t Ulm, Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2463-8167","authenticated-orcid":false,"given":"Florian","family":"W\u00f6rz","sequence":"additional","affiliation":[{"name":"Institute of Theoretical Computer Science, Universit\u00e4t Ulm, Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12,13]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"The Lognormal Distribution\u2014With Special Reference to Its Uses in Economics (2nd ed.)","author":"Aitchison John","year":"1963","unstructured":"John Aitchison and J. A. C. Brown. 1963. The Lognormal Distribution\u2014With Special Reference to Its Uses in Economics (2nd ed.). Cambridge University Press."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068413000392"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661509"},{"key":"e_1_3_3_5_2","series-title":"Department of Computer Science Report Series B","volume-title":"Proceedings of the MaxSAT Evaluation 2021: Solver and Benchmark Descriptions","volume":"2021","author":"Bacchus Fahiem","year":"2021","unstructured":"Fahiem Bacchus, Jeremias Berg, Matti J\u00e4rvisalo, and Ruben Martins (Eds.). 2021. In Proceedings of the MaxSAT Evaluation 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B, Vol. B-2021-2. University of Helsinki."},{"key":"e_1_3_3_6_2","unstructured":"Adrian Balint. 2015. Original Implementation of probSAT. Retrieved from https:\/\/github.com\/adrianopolus\/probSAT."},{"key":"e_1_3_3_7_2","series-title":"Department of Computer Science Report Series B","first-page":"37","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2016","author":"Balint Adrian","year":"2016","unstructured":"Adrian Balint and Norbert Manthey. 2016. Dimetheus. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2016-1). University of Helsinki, 37\u201338."},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_3"},{"key":"e_1_3_3_9_2","first-page":"133","volume-title":"Proceedings of the 11th International Symposium on Combinatorial Search (SOCS\u201918)","author":"Balyo Tom\u00e1\u0161","year":"2018","unstructured":"Tom\u00e1\u0161 Balyo and Luk\u00e1s Chrpa. 2018. Using algorithm configuration tools to generate hard SAT benchmarks. In Proceedings of the 11th International Symposium on Combinatorial Search (SOCS\u201918). AAAI Press, 133\u2013137."},{"issue":"188701","key":"e_1_3_3_10_2","first-page":"1","article-title":"Hiding solutions in random satisfiability problems: A statistical mechanics approach","volume":"88","author":"Barthel Wolfgang","year":"2002","unstructured":"Wolfgang Barthel, Alexander K. Hartmann, Michele Leone, Federico Ricci-Tersenghi, Martin Weigt, and Riccardo Zecchina. 2002. Hiding solutions in random satisfiability problems: A statistical mechanics approach. Phys. Rev. Lett. 88, 188701 (2002), 1\u20134.","journal-title":"Phys. Rev. Lett."},{"key":"e_1_3_3_11_2","volume-title":"Introduction to Real Analysis (3rd ed.)","author":"Bartle Robert G.","year":"2000","unstructured":"Robert G. Bartle and Donald R. Sherbert. 2000. Introduction to Real Analysis (3rd ed.). Wiley New York."},{"key":"e_1_3_3_12_2","series-title":"Department of Computer Science Report Series B","first-page":"39","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2014","author":"Biere Armin","year":"2014","unstructured":"Armin Biere. 2014. Yet another local search solver and Lingeling and friends entering the SAT competition. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2014-2). University of Helsinki, 39\u201340."},{"key":"e_1_3_3_13_2","series-title":"Department of Computer Science Report Series B","first-page":"14","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2017","author":"Biere Armin","year":"2017","unstructured":"Armin Biere. 2017. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2017-1). University of Helsinki, 14\u201315."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_3_15_2","series-title":"Department of Computer Science Report Series B","first-page":"51","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2020","author":"Biere Armin","year":"2020","unstructured":"Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. 2020. CaDiCal, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2020-1), Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 51\u201353."},{"key":"e_1_3_3_16_2","series-title":"Department of Computer Science Report Series B","first-page":"10","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2021","author":"Biere Armin","year":"2021","unstructured":"Armin Biere, Mathias Fleury, and Maximillian Heisinger. 2021. CaDiCal, Kissat, Paracooba entering the SAT competition. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2021-1), Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 10\u201313."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-28121-6"},{"key":"e_1_3_3_19_2","series-title":"Department of Computer Science Report Series B","first-page":"52","volume-title":"Proceedings of the SAT Competition: Solver and Benchmark Descriptions","volume":"2018","author":"Cai Shaowei","year":"2018","unstructured":"Shaowei Cai and Xindi Zhang. 2018. ReasonLS. In Proceedings of the SAT Competition: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2018-1). University of Helsinki, 52\u201353."},{"key":"e_1_3_3_20_2","series-title":"Department of Computer Science Report Series B","first-page":"35","volume-title":"Proceedings of SAT Race: Solver and Benchmark Descriptions","volume":"2019","author":"Cai Shaowei","year":"2019","unstructured":"Shaowei Cai and Xindi Zhang. 2019. Four relaxed CDCL solvers. In Proceedings of SAT Race: Solver and Benchmark Descriptions(Department of Computer Science Report Series B, Vol. B-2019-1), Marijn J. H. Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 35\u201336."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-80223-3_6"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.13666"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198505044.001.0001"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_3_26_2","series-title":"Statistics: A Series of Textbooks and Monographs","volume-title":"Lognormal Distributions: Theory and Applications","author":"Crow Edwin L.","year":"1988","unstructured":"Edwin L. Crow and Kunio Shimizu (Editors). 1988. Lognormal Distributions: Theory and Applications. Statistics: A Series of Textbooks and Monographs, Vol. 88. Marcel Dekker."},{"key":"e_1_3_3_27_2","unstructured":"Maximilian Diemer. 2021. Source Code of GenFactorSat. Retrieved from https:\/\/github.com\/madiemer\/gen-factor-sat\/."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_7"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-9473-8"},{"key":"e_1_3_3_31_2","first-page":"327","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI\/IAAI\u201997)","author":"Frost Daniel","year":"1997","unstructured":"Daniel Frost, Irina Rish, and Llu\u00eds Vila. 1997. Summarizing CSP hardness with continuous probability distributions. In Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI\/IAAI\u201997). 327\u2013333."},{"key":"e_1_3_3_32_2","unstructured":"Oliver Gableske. 2015. Source Code of kcnfgen (Version 1.0). Retrieved from https:\/\/www.gableske.net\/downloads\/kcnfgen_v1.0.tar.gz."},{"key":"e_1_3_3_33_2","first-page":"190","volume-title":"Proceedings of the 13th Conference on Uncertainty in Artificial Intelligence (UAI\u201997)","author":"Gomes Carla P.","year":"1997","unstructured":"Carla P. Gomes and Bart Selman. 1997. Algorithm portfolio design: Theory vs. practice. In Proceedings of the 13th Conference on Uncertainty in Artificial Intelligence (UAI\u201997). 190\u2013197."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006314320276"},{"key":"e_1_3_3_35_2","first-page":"238","volume-title":"Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI\u201998)","author":"Hoos Holger H.","year":"1998","unstructured":"Holger H. Hoos and Thomas St\u00fctzle. 1998. Evaluating Las Vegas algorithms: Pitfalls and remedies. In Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI\u201998). 238\u2013245."},{"key":"e_1_3_3_36_2","article-title":"Reciprocal of Shifted Lognormal Random Variable","author":"empiricus) Sextus Empiricus (https:\/\/stats.stackexchange.com\/users\/164061\/sextus","year":"2018","unstructured":"Sextus Empiricus (https:\/\/stats.stackexchange.com\/users\/164061\/sextus empiricus). 2018. Reciprocal of Shifted Lognormal Random Variable. Cross Validated (Stats Stack Exchange). Retrieved from https:\/\/stats.stackexchange.com\/q\/379626.","journal-title":"Cross Validated (Stats Stack Exchange)"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/36.3-4.297"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/36.1-2.149"},{"key":"e_1_3_3_39_2","volume-title":"Continuous Univariate Distributions, Volume 1 (2nd ed.)","author":"Johnson Norman L.","year":"1994","unstructured":"Norman L. Johnson, Samuel Kotz, and Narayanaswamy Balakrishnan. 1994. Continuous Univariate Distributions, Volume 1 (2nd ed.). John Wiley & Sons."},{"issue":"1","key":"e_1_3_3_40_2","article-title":"A note on the non-colorability threshold of a random graph","volume":"7","author":"Kaporis Alexis C.","year":"2000","unstructured":"Alexis C. Kaporis, Lefteris M. Kirousis, and Yannis C. Stamatiou. 2000. A note on the non-colorability threshold of a random graph. Electr. J. Combinat. 7, 1 (2000).","journal-title":"Electr. J. Combinat."},{"key":"e_1_3_3_41_2","volume-title":"Biostatistical Methods: The Assessment of Relative Risks (2nd ed.)","author":"Lachin John M.","year":"2011","unstructured":"John M. Lachin. 2011. Biostatistical Methods: The Assessment of Relative Risks (2nd ed.). John Wiley & Sons."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11518-016-5301-9"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_30"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_7"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73117-9_35"},{"key":"e_1_3_3_46_2","unstructured":"Jan-Hendrik Lorenz and Florian W\u00f6rz. 2021. Source Code of concealSATgen. Retrieved from https:\/\/github.com\/FlorianWoerz\/concealSATgen\/."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_16"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-80223-3_27"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.5555\/1122667.1122669"},{"key":"e_1_3_3_51_2","volume-title":"Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis (2nd ed.)","author":"Mitzenmacher Michael","year":"2017","unstructured":"Michael Mitzenmacher and Eli Upfal. 2017. Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis (2nd ed.). Cambridge University Press."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_3_53_2","unstructured":"Jayakrishnan Nair Adam Wierman and Bert Zwart. 2020. The Fundamentals of Heavy Tails: Properties Emergence and Estimation. Preprint California Institute of Technology."},{"key":"e_1_3_3_54_2","volume-title":"System Reliability Theory: Models, Statistical Methods, and Applications (2nd ed.)","author":"Rausand Marvin","year":"2003","unstructured":"Marvin Rausand, Anne Barros, and Arnljot Hoyland. 2003. System Reliability Theory: Models, Statistical Methods, and Applications (2nd ed.). John Wiley & Sons."},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017436"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46135-3_38"},{"key":"e_1_3_3_57_2","volume-title":"Principles of Mathematical Analysis","author":"Rudin Walter","year":"1964","unstructured":"Walter Rudin. 1964. Principles of Mathematical Analysis. Vol. 3. McGraw-Hill New York."},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-001-0094-7"},{"key":"e_1_3_3_59_2","first-page":"337","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence (AAAI\u201994)","author":"Selman Bart","year":"1994","unstructured":"Bart Selman, Henry A. Kautz, and Bram Cohen. 1994. Noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence (AAAI\u201994). AAAI Press\/MIT Press, 337\u2013343."},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btu818"},{"key":"e_1_3_3_62_2","first-page":"1","article-title":"On logarithmic correlation with an application to the distribution of ages at first marriage","volume":"84","author":"Wicksell Sven Dag","year":"1917","unstructured":"Sven Dag Wicksell. 1917. On logarithmic correlation with an application to the distribution of ages at first marriage. Meddelanden fr\u00e5n Lunds Astronomiska Observatorium 84 (1917), 1\u201321.","journal-title":"Meddelanden fr\u00e5n Lunds Astronomiska Observatorium"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ESA.2021.82"},{"key":"e_1_3_3_64_2","unstructured":"Florian W\u00f6rz and Jan-Hendrik Lorenz. 2022. Data Set for \u201cToward an Understanding of Long-tailed Runtimes.\u201dWe have provided all data of this article. All base instances resolvents and modifications can be found under 10.5281\/zenodo.4715893. Visual and statistical evaluations can be found under https:\/\/github.com\/FlorianWoerz\/Towards-an-Understanding-of-Long-Tailed-Runtimes where all evaluations take place in the files .\/evaluation\/jupyter_SB\/evaluate_*.ipynb. A permanent version of this repository has been preserved under 10.5281\/zenodo.6945926"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3569170","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3569170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:41Z","timestamp":1750182701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3569170"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,13]]},"references-count":63,"alternative-id":["10.1145\/3569170"],"URL":"https:\/\/doi.org\/10.1145\/3569170","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"type":"print","value":"1084-6654"},{"type":"electronic","value":"1084-6654"}],"subject":[],"published":{"date-parts":[[2022,12,13]]}}}