Advancing stochastic 3-SAT solvers by dissipating oversatisfied constraints

TL;DR

This paper introduces DOCSAT, a new algorithm for solving 3-SAT problems that outperforms existing methods, especially on very difficult instances.

Contribution

DOCSAT introduces a novel heuristic that dissipates oversatisfied constraints to avoid local minima in solving 3-SAT problems.

Findings

DOCSAT outperforms WalkSAT and Kissat on the hardest 3-SAT instances.

DOCSAT pushes feasible problem sizes by an order of magnitude.

The algorithm's performance is benchmarked on randomly generated 3-SAT instances up to N = 15,000.

Abstract

Hard decision problems, in computational complexity theory known as NP-complete, are of universal importance. From a conceptual perspective, an efficient solution to one such complete problem is tantamount to solving any other in the wide class of efficiently verifiable (NP) problems. Moreover, paradigmatic examples such as the Boolean satisfiability problem 3-SAT have ubiquitous applications ranging from circuit design to logistics. In this paper, we introduce the heuristic algorithm DOCSAT that drastically outperforms previous methods to tackle 3-SAT in the notoriously difficult regime of barely satisfiable randomly generated instances. There, our DOCSAT solver pushes the feasible problem sizes by about an order of magnitude, quite remarkably so in light of the asymptotically exponential cost reflecting the NP-completeness of the considered problem.

We introduce and benchmark a stochastic local search heuristic for the Nondeterministic Polynomial Time (NP) complete satisfiability problem 3-SAT that drastically outperforms existing solvers in the notoriously difficult realm of critically hard instances. Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima that are distinguished from true solutions by a larger number of oversatisfied combinatorial constraints. To address this issue, the proposed algorithm dissipates oversatisfied constraints (DOC), hence coined DOCSAT, i.e. reduces their unfavorable abundance so as to render them critical. We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N = 15,000. Quite remarkably, we find that DOCSAT outperforms both WalkSAT and other well known algorithms including the complete solver Kissat, even when comparing its ability to solve the hardest quintile of the sample to the average performance of its competitors. The essence of DOCSAT may be seen as a way of harnessing statistical structure beyond the primary cost function of a combinatorial problem to avoid or escape local minima traps in stochastic local search, which opens avenues for generalization to other optimization problems.

Figures