Enhancing SAT solvers with glue variable predictions

TL;DR

This paper introduces a new method for enhancing SAT solvers by predicting glue variables using a simpler neural network architecture, enabling CPU inference and improving solver performance on multiple benchmarks.

Contribution

It proposes predicting glue variables as a new training target, allowing for easier data generation and reinforcement learning, and demonstrates improved SAT solver performance.

Findings

Improved SAT solver performance on SATCOMP 2018 and SATRACE 2019 benchmarks.

Effective CPU-based neural network inference for large industrial problems.

Successful application of reinforcement learning to enhance solver efficiency.

Abstract

Modern SAT solvers routinely operate at scales that make it impractical to query a neural network for every branching decision. NeuroCore, proposed by Selsam and Bjorner, offered a proof-of-concept that neural networks can still accelerate SAT solvers by only periodically refocusing a score-based branching heuristic. However, that work suffered from several limitations: their modified solvers require GPU acceleration, further ablations showed that they were no better than a random baseline on the SATCOMP 2018 benchmark, and their training target of unsat cores required an expensive data pipeline which only labels relatively easy unsatisfiable problems. We address all these limitations, using a simpler network architecture allowing CPU inference for even large industrial problems with millions of clauses, and training instead to predict {\em glue variables}---a target for which it is easier to generate labelled data, and which can also be formulated as a reinforcement learning task. We demonstrate the effectiveness of our approach by modifying the state-of-the-art SAT solver CaDiCaL, improving its performance on SATCOMP 2018 and SATRACE 2019 with supervised learning and its performance on a dataset of SHA-1 preimage attacks with reinforcement learning.