Document Open Access Logo

Evidence for Long-Tails in SLS Algorithms

Authors Florian Wörz , Jan-Hendrik Lorenz

PDF
Thumbnail PDF

File

LIPIcs.ESA.2021.82.pdf
  • Filesize: 1.44 MB
  • 16 pages

Document Identifiers

Author Details

Florian Wörz
  • Institut für Theoretische Informatik, Universität Ulm, Germany
Jan-Hendrik Lorenz
  • Institut für Theoretische Informatik, Universität Ulm, Germany

Funding

  • Wörz, Florian: Supported by the Deutsche Forschungsgemeinschaft (DFG) under project number 430150230, "Complexity measures for solving propositional formulas".

Acknowledgements

The authors acknowledge support by the state of Baden-Württemberg through bwHPC.

Cite AsGet BibTex

Florian Wörz and Jan-Hendrik Lorenz. Evidence for Long-Tails in SLS Algorithms. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 82:1-82:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ESA.2021.82

Abstract

Stochastic local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one [Jan{-}Hendrik Lorenz and Florian Wörz, 2020]. Empirically, this technique was found to be promising as it improves the performance of state-of-the-art SLS solvers. Currently, there is only a shallow understanding of how this modification technique affects the runtimes of SLS solvers. Thus, we model this modification process and conduct an empirical analysis of the hardness of logically equivalent formulas. Our results are twofold. First, if the modification process is treated as a random process, a lognormal distribution perfectly characterizes the hardness; implying that the hardness is long-tailed. This means that the modification technique can be further improved by implementing an additional restart mechanism. Thus, as a second contribution, we theoretically prove that all algorithms exhibiting this long-tail property can be further improved by restarts. Consequently, all SAT solvers employing this modification technique can be enhanced.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Probabilistic algorithms
  • Mathematics of computing → Distribution functions
Keywords
  • Stochastic Local Search
  • Runtime Distribution
  • Statistical Analysis
  • Lognormal Distribution
  • Long-Tailed Distribution
  • SAT Solving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Alejandro Arbelaez, Charlotte Truchet, and Philippe Codognet. Using sequential runtime distributions for the parallel speedup prediction of SAT local search. Theory and Practice of Logic Programming, 13(4-5):625-639, 2013. Google Scholar
  2. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI '09), pages 399-404, 2009. Google Scholar
  3. Adrian Balint. Original implementation of probSAT, 2015. Available at URL: https://github.com/adrianopolus/probSAT.
  4. Adrian Balint, Anton Belov, Marijn J. H. Heule, and Matti Järvisalo. SAT Competition 2013: Results. URL: http://satcompetition.org/2013/results.shtml.
  5. Tomáš Balyo and Lukás Chrpa. Using algorithm configuration tools to generate hard SAT benchmarks. In Proceedings of the 11th International Symposium on Combinatorial Search (SOCS '18), pages 133-137. AAAI Press, 2018. Google Scholar
  6. Wolfgang Barthel, Alexander K. Hartmann, Michele Leone, Federico Ricci-Tersenghi, Martin Weigt, and Riccardo Zecchina. Hiding solutions in random satisfiability problems: A statistical mechanics approach. Physical review letters, 88(188701):1-4, 2002. Google Scholar
  7. Armin Biere. Yet another local search solver and Lingeling and friends entering the SAT Competition 2014. In Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, volume B-2014-2, pages 39-40. University of Helsinki, 2014. Google Scholar
  8. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  9. Russell Cheng. Non-standard parametric statistical inference. Oxford University Press, 2017. Google Scholar
  10. Maximilian Diemer. Source code of GenFactorSat, 2021. Newest version available at URL: https://github.com/madiemer/gen-factor-sat/.
  11. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Selected Revised Papers of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT '03), volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2004. Google Scholar
  12. Sergey Foss, Dmitry Korshunov, and Stan Zachary. An Introduction to Heavy‑Tailed and Subexponential Distributions, volume 6. Springer, 2011. Google Scholar
  13. Daniel Frost, Irina Rish, and Lluís Vila. 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 '97), pages 327-333, 1997. Google Scholar
  14. Oliver Gableske. Source code of kcnfgen (version 1.0), 2015. Retrieved from URL: https://www.gableske.net/downloads/kcnfgen_v1.0.tar.gz.
  15. Carla P. Gomes and Bart Selman. Algorithm portfolio design: Theory vs. practice. In Proceedings of the 13th Conference on Uncertainty in Artificial Intelligence (UAI '97), pages 190-197, 1997. Google Scholar
  16. Carla P. Gomes, Bart Selman, Nuno Crato, and Henry A. Kautz. Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning, 24:67-100, 2000. Related version in CP '97. Google Scholar
  17. Marijn J. H. Heule, Matti Järvisalo, and Tomáš Balyo. SAT Competition 2017: Results. URL: https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=results.
  18. Holger H. Hoos and Thomas Stützle. Evaluating Las Vegas algorithms: Pitfalls and remedies. In Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI '98), pages 238-245, 1998. Google Scholar
  19. Norman L. Johnson, Samuel Kotz, and Narayanaswamy Balakrishnan. Continuous Univariate Distributions, Volume 1. Wiley Series in Probability and Statistics. John Wiley & Sons, 2nd edition, 1994. Google Scholar
  20. Alexis C. Kaporis, Lefteris M. Kirousis, and Yannis C. Stamatiou. A note on the non-colorability threshold of a random graph. The Electronic Journal of Combinatorics, 7(1), 2000. Google Scholar
  21. Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. CNFgen: A generator of crafted benchmarks. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT '17), pages 464-473, 2017. Google Scholar
  22. Jan-Hendrik Lorenz. Runtime distributions and criteria for restarts. In Proceedings of the 44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '18), pages 493-507. Springer, 2018. Google Scholar
  23. Jan-Hendrik Lorenz and Florian Wörz. On the effect of learned clauses on stochastic local search. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT '20), volume 12178 of Lecture Notes in Computer Science, pages 89-106. Springer, 2020. Implementation and statistical tests of GapSAT available at Zenodo 10.5281/zenodo.3776052. Google Scholar
  24. Jan-Hendrik Lorenz and Florian Wörz. Source code of concealSATgen, 2021. Newest version available at URL: https://github.com/FlorianWoerz/concealSATgen/.
  25. Chuan Luo, Shaowei Cai, and Kaile Su. DCCAlm in SAT Competition 2016. In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, volume B-2016-1. University of Helsinki, 2016. Google Scholar
  26. Chuan Luo, Shaowei Cai, Wei Wu, and Kaile Su. Focused random walk with configuration checking and break minimum for satisfiability. In Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming (CP '13), volume 8124 of Lecture Notes in Computer Science, pages 481-496. Springer, 2013. Google Scholar
  27. Chuan Luo, Shaowei Cai, Wei Wu, and Kaile Su. Double configuration checking in stochastic local search for satisfiability. In Proceedings of the 28th AAAI Conference on Artificial Intelligence, pages 2703-2709. AAAI Press, 2014. Google Scholar
  28. Chuan Luo, Shaowei Cai, Wei Wu, and Kaile Su. CSCCSat in SAT Competition 2016. In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, volume B-2016-1. University of Helsinki, 2016. Google Scholar
  29. Stephan Mertens, Marc Mézard, and Riccardo Zecchina. Threshold values of random k-SAT from the cavity method. Random Structures & Algorithms, 28(3):340-373, 2006. Google Scholar
  30. Jayakrishnan Nair, Adam Wierman, and Bert Zwart. The fundamentals of heavy tails: Properties, emergence, and estimation. Preprint, California Institute of Technology, 2020. Google Scholar
  31. Marvin Rausand, Anne Barros, and Arnljot Hoyland. System reliability theory: models, statistical methods, and applications. John Wiley & Sons, 2nd edition, 2003. Google Scholar
  32. Irina Rish and Daniel Frost. Statistical analysis of backtracking on inconsistent CSPs. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP '97), pages 150-162, 1997. Google Scholar
  33. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965. Google Scholar
  34. Yongshao Ruan, Eric Horvitz, and Henry A. Kautz. Restart policies with dependence among runs: A dynamic programming approach. In Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP '02), volume 2470 of Lecture Notes in Computer Science, pages 573-586. Springer, 2002. Google Scholar
  35. Walter Rudin. Principles of mathematical analysis, volume 3. McGraw-Hill New York, 1964. Google Scholar
  36. Uwe Schöning. A probabilistic algorithm for k-SAT based on limited local search and restart. Algorithmica, 32(4):615-623, 2002. Preliminary version in FOCS '99. Google Scholar
  37. Uwe Schöning and Jacobo Torán. The Satisfiability Problem: Algorithms and Analyses, volume 3 of Mathematics for Applications (Mathematik für Anwendungen). Lehmanns Media, 2013. Google Scholar
  38. Oleg V. Shylo, Timothy Middelkoop, and Panos M. Pardalos. Restart strategies in optimization: parallel and serial cases. Parallel Computing, 37(1):60-68, 2011. Google Scholar
  39. Gunnar Völkel, Ludwig Lausser, Florian Schmid, Johann M. Kraus, and Hans A. Kestler. Sputnik: ad hoc distributed computation. Bioinformatics, 31(8):1298-1301, 2015. Google Scholar
  40. Sven Dag Wicksell. On logarithmic correlation with an application to the distribution of ages at first marriage. Meddelanden från Lunds Astronomiska Observatorium, 84:1-21, 1917. Google Scholar
  41. Florian Wörz and Jan-Hendrik Lorenz. Evidence for long-tails in SLS algorithms. Technical Report 2107.00378, arXiv.org, 2021. This is the full-length version of the present paper. Google Scholar
  42. Florian Wörz and Jan-Hendrik Lorenz. Supplementary Data for "Evidence for Long-Tails in SLS Algorithms", 2021. We have provided all data of this paper. 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/SLS_Evidence_long_tail, where all evaluations take place in the files ./evaluation/jupyter/evaluate_*.ipynb. A permanent version of this repository has been preserved under 10.5281/zenodo.5026180.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact