Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms

TL;DR

This paper investigates the long-tailed runtime distributions of SLS algorithms for SAT, proposing a method to generate equivalent problem formulations, analyzing their impact on solver performance, and demonstrating the Johnson SB distribution as a key model.

Contribution

It introduces a method for generating equivalent SAT problem formulations, enabling a rigorous analysis of their effect on SLS solver runtimes and establishing Johnson SB distributions as a model for these runtimes.

Findings

Runtime distributions are well-characterized by Johnson SB distributions.

Long-tailed distributions imply the effectiveness of restarts.

Runtimes of Schöning's algorithm are approximately Johnson SB.

Abstract

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.