Guiding High-Performance SAT Solvers with Unsat-Core Predictions

TL;DR

This paper demonstrates that training a simplified NeuroSAT model to predict unsatisfiable cores can effectively guide high-performance SAT solvers, significantly improving their problem-solving capabilities on real-world benchmarks.

Contribution

The authors adapt NeuroSAT to predict unsatisfiable cores and integrate it into SAT solvers, leading to notable performance improvements on standard and domain-specific benchmarks.

Findings

Modified solvers solve 10-20% more problems within timeouts.

Specialized training yields up to 20% more solved problems.

NeuroSAT guidance enhances solver effectiveness on real problems.

Abstract

The NeuroSAT neural network architecture was recently introduced for predicting properties of propositional formulae. When trained to predict the satisfiability of toy problems, it was shown to find solutions and unsatisfiable cores on its own. However, the authors saw "no obvious path" to using the architecture to improve the state-of-the-art. In this work, we train a simplified NeuroSAT architecture to directly predict the unsatisfiable cores of real problems. We modify several high-performance SAT solvers to periodically replace their variable activity scores with NeuroSAT's prediction of how likely the variables are to appear in an unsatisfiable core. The modified MiniSat solves 10% more problems on SAT-COMP 2018 within the standard 5,000 second timeout than the original does. The modified Glucose solves 11% more problems than the original, while the modified Z3 solves 6% more. The gains are even greater when the training is specialized for a specific distribution of problems; on a benchmark of hard problems from a scheduling domain, the modified Glucose solves 20% more problems than the original does within a one-hour timeout. Our results demonstrate that NeuroSAT can provide effective guidance to high-performance SAT solvers on real problems.