Papers › Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
Jan-Hendrik Lorenz, Florian Wörz
The satisfiability problem is one of the most famous problems in computer science. Its NP-completeness has been used to argue that SAT is intractable. However, there have been tremendous advances that allow SAT solvers to solve instances with millions of variables. A particularly successful paradigm is stochastic local search. In most cases, there are different ways of formulating the underlying problem. While it is known that this has an impact on the runtime of solvers, finding a helpful formulation is generally non-trivial. The recently introduced GapSAT solver [Lorenz and W\"orz 2020] 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 cases in which the performance slightly deteriorated. This justifies in-depth investigations into how learning logical implications affects runtimes for SLS. In this work, we propose a method for generating logically equivalent problem formulations, generalizing the ideas of GapSAT. This allows a rigorous mathematical study of the effect on the runtime of SLS solvers. If the modification process is treated as random, 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. As a second contribution, we theoretically prove that restarts are useful for long-tailed distributions. This implies that additional restarts can further refine all algorithms employing above mentioned modification technique. Since the empirical studies compellingly suggest that the runtime distributions follow Johnson SB distributions, we investigate this property theoretically. We succeed in proving that the runtimes for Sch\"oning's random walk algorithm are approximately Johnson SB.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections