Source-linked AI summary
Guiding High-Performance SAT Solvers with Unsat-Core Predictions
Daniel Selsam, Nikolaj Bjørner
TL;DR
Existing NeuroSAT work found no obvious path to improving state-of-the-art SAT solving, despite predicting properties such as satisfiability and unsatisfiable cores. This paper trains NeuroSAT to predict unsatisfiable-core variables and periodically uses those predictions to guide high-performance solvers, which solve more benchmark problems than their original versions. The approach is limited by the simplicity and generality of binary core prediction, especially because real problems often lack tiny cores.
Problem
Prior NeuroSAT work reported no obvious path to improving existing SAT solvers, motivating a method for using neural predictions on real problems.
Method
The paper trains a simplified NeuroSAT to predict variables likely to appear in unsatisfiable cores and periodically uses those predictions to refocus solver variable-activity scores.
Results
The modified MiniSat, Glucose, and Z3 solve 10%, 11%, and 6% more SAT-COMP 2018 problems, respectively, while specialized training yields a 20% gain for Glucose on hard scheduling problems.
Takeaways & Limitations
NeuroSAT can provide effective guidance to high-performance SAT solvers on real problems.
Takeaways & Limitations
Binary core-presence prediction is simplistic and may be uninformative when a smallest core contains every variable or when only a few core variables make good branches.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper repurposes NeuroSAT as NeuroCore, a heuristic that predicts unsatisfiable-core variables and periodically guides high-performance SAT solvers. This modification improves solver performance on broad and specialized real-problem benchmarks.
- 1 Introduction: The work addresses NeuroSAT’s earlier gap between finding cores on toy problems and improving state-of-the-art SAT solving on real problems.The original authors reported no obvious path to beating existing SAT solvers.
- 1 Introduction: NeuroCore periodically resets solver variable activity scores in proportion to predicted likelihood of appearing in an unsatisfiable core, complementing existing branching heuristics.The approach queries the entire problem periodically rather than replacing efficient solver heuristics at every branching decision.
- 1 Introduction: The training pipeline generates unsatisfiable problems, extracts core variables from DRAT proofs, trains NeuroCore on these labels, and integrates predictions into MiniSat, Glucose, and Z3.The pipeline uses original and learnt clauses when periodically querying the network.
2 Data generation
The authors overcome the scarcity of labeled unsatisfiable problems by generating more than 150,000 labeled subproblems from existing benchmarks. The resulting dataset supports core prediction but does not guarantee diverse cores, and the binary labels are intentionally simplistic.
- 2 Data generation: Over 150,000 unsatisfiable subproblems with labeled cores are generated because only roughly one thousand unsatisfiable problems exist across SATCOMP competitions.The subproblems are derived from existing problems to increase the amount of training data.
- 2 Data generation: The pipeline distributes workers that solve subproblems, produce DRAT proofs, and extract variables appearing in unsatisfiable cores.The driver initializes work from SATCOMP problems through 2017 and hard scheduling problems.
- 2 Data generation: The generated dataset is not guaranteed to contain diverse cores because the branching process may select variables that fail to change the core.Different noncore clauses can still make the resulting subproblems distinct.
- 2 Data generation: Binary core-membership prediction can be uninformative when a smallest core contains every variable or when only some core variables make good branches.The authors suggest richer scores derived from the full DRAT proof as a more sophisticated alternative.
3 Neural Network Architecture
NeuroCore is a simplified NeuroSAT-style message-passing network that represents CNF formulas with clause-literal incidence matrices. It produces a score for each variable, trains against core-derived probability distributions, and is simplified for cheap heuristic guidance on large problems.
- 3 Neural Network Architecture: NeuroCore represents a CNF formula with a sparse nc×2nv clause-literal matrix and uses three multilayer perceptrons to update clause and literal embeddings.Rows encode clauses and literals, while Flip and Flop organize positive and negative literal representations.
- 3 Neural Network Architecture: After four message-passing iterations, NeuroCore flops literal embeddings and projects them into one numerical score per variable.Applying softmax to these scores defines a probability distribution over variables.
- 3 Neural Network Architecture: Training assigns uniform target probability to variables in each labeled core and zero probability to others, then minimizes Kullback-Leibler divergence.The three MLPs are optimized jointly against these core-derived distributions.
- 3 Neural Network Architecture: The architecture is simplified for cheap guidance: it uses four iterations rather than the original NeuroSAT’s 26 training iterations and potentially thousands at test time.The paper’s goal is coarse heuristic guidance on potentially large problems, not perfect end-to-end solving.
4 Hybrid Solving: Extending CDCL with NeuroCore
The hybrid solver periodically refocuses CDCL’s variable-branching heuristic using NeuroCore’s predictions, while retaining the solver’s efficient activity-based search. NeuroCore is queried on a selected snapshot of the problem and its scores replace EVSIDS activities.
- CDCL variable branching: EVSIDS prioritizes variables involved in recent conflicts, with older conflict contributions discounted by the decay factor ρ.The score is defined from conflict involvement and exponentially decayed history.
- Integrating NeuroCore: NeuroCore periodically replaces CDCL variable activity scores with predictions of which variables are likely to belong to an unsatisfiable core.The integration queries NeuroCore on the entire problem rather than conditioning on the current trail, then replaces the activity scores.
- Integrating NeuroCore: At each query, the solver supplies selected non-eliminated, non-level-0-unit variables and a bounded collection of original and learned clauses.The resulting sparse clause-literal adjacency matrix limits the problem representation passed to NeuroCore as learned clauses accumulate.
- Integrating NeuroCore: NeuroCore converts variable scores into a temperature-scaled softmax distribution, scales it by problem size and κ, and resets all EVSIDS activities.In MiniSat, this also resets the variable increment and rebuilds the order heap.
- Integrating NeuroCore: Because NeuroCore queries are expensive, the hybrid strategy complements rather than replaces the solver’s efficient branching heuristic through periodic refocusing.MiniSat’s hybrid solver queries NeuroCore once every 100 seconds, allowing the neural intervention to redirect search without querying every decision.
5 Solver Experiments
NeuroCore-assisted SAT solvers outperform their original counterparts across SATCOMP-2018 and specialized scheduling benchmarks, with gains varying by solver and problem distribution. The experiments also examine robustness, computational fairness, and whether improvements arise from NeuroCore’s signal or periodic refocusing itself.
- Experimental considerations: SATCOMP-2018 results include coarse hyperparameter tuning based on runs on SATCOMP-2018 problems, despite no SATCOMP training examples.The authors regret not using alternate problems for tuning but suspect other sources would have produced a similar parameter range.
- MiniSat: Neuro-minisat solves 205 SATCOMP-2018 problems versus 187 for minisat, a 10% increase within the 5,000-second timeout.Most of the improvement comes from satisfiable problems: 125 versus 109, while unsatisfiable problems increase by 3% from 78 to 80.
- Glucose: 11% more SATCOMP-2018 problems are solved by neuro-glucose, increasing the count from 186 to 206.The experiment used exponential-backoff NeuroCore queries, and its scatter plot shows many cases solved within seconds that glucose times out on.
- Z3: Modified Z3 solves 170 problems versus 161 for the original, a 6% increase within the timeout.The two solvers were evaluated simultaneously, and increased contention partly explains their lower absolute scores than MiniSat and Glucose.
- A more favorable regime: 20% more scheduling problems are solved by neuro-glucose than glucose within the one-hour timeout.The solvers are roughly tied for 30 minutes before neuro-glucose pulls away through the timeout.
- Ablations: Periodic random refocusing performs impressively on SATCOMP-2018 but unimpressively on scheduling problems, indicating domain-dependent NeuroCore signal.The scheduling ablation does not exclude another non-neural heuristic matching NeuroCore’s performance.
6 Related Work
Prior machine-learning work in automated deduction has focused on strategy, axiom, clause, and branch selection. NeuroCore instead combines global neural predictions with periodic, fine-grained CDCL branching heuristics.
- Strategy and axiom selection: Strategy selection configures solver parameters, whereas axiom and clause selection focus inference on selected input or learned clauses.Examples include domain-specific axiom selection and machine-learned redundant-clause elimination in CryptoMiniSat.
- Branch selection: Machine-learning integration for branch selection in SAT remains relatively unexplored compared with established VSIDS-, CHB-, and VMTF-style heuristics.Look-ahead solvers instead accept greater overhead to identify branch literals using clause-reduction metrics.
- Related branching paradigms: MIP branch-and-bound and SAT cube-and-conquer share branching similarities, but modern MIP solvers apply branching relatively rarely alongside linear-programming methods.This contrasts with the frequent branching decisions central to CDCL SAT solving.
- Branch selection: NeuroCore performs global analysis to predict an ordering among unassigned variables, then periodically lets CDCL heuristics handle fine-grained inference decisions.This places the approach between CDCL's fine-grained branching and look-ahead solvers' single-step branch decisions.
7 Discussion
The discussion surveys alternative ways to train and use NeuroSAT, finding that unsat-core predictions were more effective than several explored heuristics while leaving substantial design space open.
- The authors frame NeuroCore as one small point in a broad design space for training NeuroSAT and guiding SAT solvers.They hope these initial results encourage other approaches.
- Core prediction is less decisive on general real problems than on synthetic instances with tiny, similar cores.The authors note that real problems rarely have tiny cores, limiting even a perfect predictor’s impact.
- Unsat-core predictions outperformed March-based predictions for refocusing EVSIDS, while core-based cubing remained worse than the March baseline but better than random.The March-refocusing comparison was affected by the predictions being peakier than unsat-core predictions.
- Exploration-based learning faces huge variable spaces and delayed feedback from solving subproblems, motivating imitation learning and value-function pretraining.The authors also experimented with direct model prediction and Monte Carlo or reinforcement-learning approaches.
- The paper concludes that NeuroCore’s promising initial results warrant further investigation of alternative ways to leverage NeuroSAT.