Behavior of heuristics and state space structure near SAT/UNSAT transition

TL;DR

This paper investigates the behavior of the ASAT heuristic for solving large random SAT problems near the SAT/UNSAT transition, demonstrating its efficiency and scalability in solving instances with up to one million variables.

Contribution

It introduces and analyzes ASAT, a simple focused stochastic local search heuristic, showing its effectiveness in solving large SAT instances near the phase transition.

Findings

ASAT solves large 3SAT instances in linear time up to 4.21 clauses per variable.

ASAT efficiently solves K-SAT instances up to K=7 at the FRSB threshold.

The heuristic's simplicity does not compromise its ability to handle large problem sizes.

Abstract

We study the behavior of ASAT, a heuristic for solving satisfiability problems by stochastic local search near the SAT/UNSAT transition. The heuristic is focused, i.e. only variables in unsatisfied clauses are updated in each step, and is significantly simpler, while similar to, walksat or Focused Metropolis Search. We show that ASAT solves instances as large as one million variables in linear time, on average, up to 4.21 clauses per variable for random 3SAT. For K higher than 3, ASAT appears to solve instances at the ``FRSB threshold'' in linear time, up to K=7.