Guiding High-Performance SAT Solvers with Unsat-Core Predictions
This work provides a practical method to enhance SAT solver performance on real-world problems, though it is incremental as it builds on existing NeuroSAT and solver frameworks.
The authors tackled the problem of improving high-performance SAT solvers by training a simplified NeuroSAT architecture to predict unsatisfiable cores and using these predictions to guide solvers, resulting in a 10-11% increase in solved problems on standard benchmarks and up to 20% on domain-specific hard problems.
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.