Research map / Graph learning / Graph algorithms and clustering
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes NeuroBack, which uses a one-shot offline GNN (graph transformer) trained to predict backbone variable phases and uses those predictions to initialize phases in Kissat, running on CPU only.
Problem
Prior GNN-based enhancements of CDCL SAT solvers either fail to improve solving effectiveness on large instances or require frequent GPU-based online inference, which is impractical for parallel solving.
Approach
Perform a single offline GNN inference before solving to predict phases of backbone variables (generalized to variables in most satisfying assignments), using a compact bipartite graph with meta nodes and a graph transformer with GSA and LSA blocks, then use these predictions as initial phases in Kissat.
Key results
- NeuroBack-Kissat solved 203 vs 193 problems (Default-Kissat) on 308 inferred SATCOMP-2022 problems, a 5.2% improvement.
- NeuroBack-Kissat solved 204 vs 198 problems (Default-Kissat) on 353 inferred SATCOMP-2023 problems, a 3.0% improvement (7.4% over Random-Kissat).
- Fine-tuned backbone phase classifier reached 0.928 F1 and 0.887 accuracy on the validation split; pre-trained model reached 0.751 accuracy.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Initialize Kissat variable phases using NeuroBack predictions instead of the default all-true initialization | Kissat · SATCOMP-2022 inferred problems | solved problems: 193 -> 203; improvement of 5.2% | Helped |
| Initialize Kissat variable phases using NeuroBack predictions instead of random initialization | Kissat · SATCOMP-2022 inferred problems | solved problems: 197 -> 203; improvement of 3.0% | Helped |
| Initialize Kissat variable phases using NeuroBack predictions instead of the default all-true initialization | Kissat · SATCOMP-2023 inferred problems | solved problems: 198 -> 204; improvement of 3.0% | Helped |
| Initialize Kissat variable phases using NeuroBack predictions instead of random initialization | Kissat · SATCOMP-2023 inferred problems | solved problems: 190 -> 204; improvement of 7.4% | Helped |
| Fine-tune the pre-trained NeuroBack model on DataBack-FT | NeuroBack · DataBack-FT validation set | accuracy: 0.751 -> 0.887 | Helped |
Surprising findings
- Random phase initialization beats default phase initialization on SATCOMP-2022 (197 vs 193) but is worse on SATCOMP-2023.
- Gains are larger on satisfiable problems (about 53% average improvement) than on unsatisfiable ones (about 15%).
Limitations
- Only 308 of 800 SATCOMP-2022/2023 problems could be inferred under the memory limit, so results cover a subset and unsuccessful inferences fall back to baseline.
- Predicted phases are used only as static initialization; dynamic use (e.g., during rephasing) is not explored.
- Pre-training requires a large dataset, and the pre-trained model's recall on backbone phases is modest (76.6%).
Experimental setup
Datasets: CNFgen SATLIB model counting competitions 2020-2022 SAT competition random tracks 2004-2021 SAT competition main tracks 2004-2021 SATCOMP-2022 SATCOMP-2023
Benchmarks: SATCOMP-2022 main track SATCOMP-2023 main track DataBack-FT validation split
Metrics: number of problems solved solving time precision recall F1 accuracy
Baselines: Default-Kissat Random-Kissat NeuroCore
Builds on: Kissat GraphTrans NeuroCore CadiBack
Closest papers by meaning
- Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs (ICLR 2026 · similarity 0.88)
- NSNet: A General Neural Probabilistic Framework for Satisfiability Problems (NeurIPS 2022 · similarity 0.88)
- Learning a SAT Solver from Single-Bit Supervision (ICLR 2019 · similarity 0.88)
- G2SAT: Learning to Generate SAT Formulas (NeurIPS 2019 · similarity 0.87)
- Learning Better Representations From Less Data For Propositional Satisfiability (NeurIPS 2024 · similarity 0.87)
- Learning How to Cube (NeurIPS 2026 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.