Targeting Clause Type Distributions: a Picklock for Random Satisfiability Problems

TL;DR

The paper introduces TSAT, a novel algorithm that significantly improves the ability of stochastic local search methods to solve large, hard random 3-SAT problems by leveraging problem-specific statistical information.

Contribution

TSAT is a new algorithm that triples the tractable problem sizes in the hardest regimes of random 3-SAT, surpassing previous local search methods.

Findings

TSAT roughly triples the problem sizes solvable in the hardest regimes.

TSAT outperforms established local search algorithms in the critical parameter space.

The analysis explains limitations of existing algorithms and how TSAT overcomes them.

Abstract

Optimization problems such as the NP-complete 3-SAT provide an important benchmark for the difficult task of finding ground-states in strongly correlated many-body systems with rugged energy landscapes. The study of random 3-SAT problems as Ising spin Hamiltonians in statistical physics has yielded major insights including the existence of a satisfiability phase transition, and the prediction of a critical parameter line of particularly hard instances. Yet, progress on solving those instances has been scarce for several decades. Here, introducing the Target-SAT (TSAT) algorithm, we roughly triple the tractable problem sizes in the hardest regime, with an even greater improvement in a vast range of neighboring regions. By leveraging statistical information hidden in the combinatorial constraints of the problem, TSAT is actively guided in its stochastic local search toward a target within the relevant parameter space. Our analysis also explains why established local search algorithms are limited to relatively small system sizes due to a vast low-energy trap. Furthermore, we characterize the aforementioned critical line in terms of a dominant additional complexity barrier, whose exponential scaling is quickly overcome by TSAT only in the surrounding parameter space. With TSAT, the lead in solving the hardest known random satisfiability problems returns to the realm of stochastic local search algorithms.