Evidence for Long-Tails in SLS Algorithms

TL;DR

This paper investigates how modifying SAT instances affects solver performance, revealing a long-tailed distribution of hardness and demonstrating that restart strategies can improve all such algorithms.

Contribution

It models the modification process, empirically shows the long-tail distribution of hardness, and proves that restart strategies can enhance algorithms with this property.

Findings

Hardness follows a lognormal distribution, indicating long-tail behavior.

Restart mechanisms can significantly improve solver performance.

All algorithms with long-tail hardness can benefit from restarts.

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. 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.