Using deep learning to construct stochastic local search SAT solvers with performance bounds

TL;DR

This paper introduces a novel approach that uses graph neural networks as oracles to improve stochastic local search SAT solvers, achieving better performance and theoretical guarantees.

Contribution

It proposes leveraging machine learning models, specifically GNNs, as oracles to enhance the efficiency and effectiveness of SLS SAT solvers, bridging theory and practice.

Findings

Significant reduction in step counts for solving SAT instances

Improved solved instance rates on random and pseudo-industrial benchmarks

Demonstrated the practical potential of machine learning-enhanced SLS solvers

Abstract

The Boolean Satisfiability problem (SAT), as the prototypical $\mathsf{NP}$-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable ``oracles'', i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees.