NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions
share
The NeuroSAT neural network architecture was introduced for predicting properties of propositional formulae. When trained to predict the satisfiability of toy problems, it was shown to find solutions and unsatisiable 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, and modify several state-of-the art 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 timeout than the original does. The modified Glucose 4.1 solves 11 problems than the original, while the modified Z3 solves 6 demonstrate that NeuroSAT (and in particular, NeuroCore) can provide effective guidance to high-performance SAT solvers on real problems.
READ FULL TEXT