Research map / Architectures and efficiency / RNNs and normalization
Learning Better Representations From Less Data For Propositional Satisfiability
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 NeuRes, a neuro-symbolic GNN-plus-attention model that generates resolution proofs of unsatisfiability and satisfying assignments for CNF formulas, trained with certificate supervision and bootstrapped expert iteration to shorten teacher proofs.
Problem
Neural networks for NP-complete SAT typically need huge training sets and external symbolic verifiers, and neural unsat predictions come without easily checkable certificates.
Approach
Train a NeuroSAT-style formula embedder with attention-based heads that autoregressively select clause pairs to perform resolution (certificate-driven training), run in parallel with a satisfying-assignment decoder, and use expert iteration so model-generated shorter proofs replace teacher proofs.
Key results
- NeuRes (Full-Attn) proves 98.2% of SR(40) test formulas (96.8% SAT, 99.6% UNSAT) versus NeuroSAT's 85% predicted accuracy, with NeuRes predicting 91.65% total, trained on 16K formulas versus NeuroSAT's millions.
- Bootstrapped training reduces the teacher proof dataset by about 31.85% in total and yields test p-Len of 1.15 with 100% success on the unsat set.
- Top-3 Full-Attn fan-out reduces p-Len to 0.57 and raises total proven rate to 99.9%; top-5 gives 0.52 and 100.0%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Train with certificate-driven resolution proofs rather than classification-only supervision | NeuRes representations · SR(40) | predicted total (%): 85 -> 91.65 | Helped |
| Use dynamic rather than static embeddings (ablation) | NeuRes attention variants · SR(U(10, 40)) unsat test | proven (%): 14.72 -> 37.33; 25.38 -> 95.2; 28.72 -> 60.5 | Helped |
| Use Full-Attn rather than Casc-Attn (ablation) | NeuRes with dynamic embeddings · SR(U(10, 40)) unsat test | proven (%): 37.33 -> 95.2 | Helped |
| Use Full-Attn rather than Anch-Attn (ablation) | NeuRes with dynamic embeddings · SR(U(10, 40)) unsat test | proven (%): 60.5 -> 95.2 | Helped |
| Use Anch-Attn rather than Full-Attn (ablation) | NeuRes with static embeddings · SR(U(10, 40)) unsat test | proven (%): 25.38 -> 28.72 | Helped |
| Take the top 3 attention-grid steps per forward pass rather than only the top step (ablation) | Full-Attn NeuRes · SR(40) test | Total proven (%): 98.2 -> 99.9 | Helped |
| Take the top 3 attention-grid steps per forward pass rather than only the top step (ablation) | Full-Attn NeuRes · SR(40) test | p-Len: 1.15 -> 0.57 | Helped |
| Take the top 5 attention-grid steps per forward pass rather than only the top step (ablation) | Full-Attn NeuRes · SR(40) test | Total proven (%): 98.2 -> 100.0 | Helped |
| Take the top 5 attention-grid steps per forward pass rather than only the top step (ablation) | Full-Attn NeuRes · SR(40) test | p-Len: 1.15 -> 0.52 | Helped |
| Replace teacher proofs with shorter model-generated proofs during iterative training (ablation) | NeuRes · SR(U(10, 40)) training set | Total Reduction (%): 31.85 | Helped |
| Supervise both positive- and negative-literal assignment decoders instead of only the positive assignment (ablation) | NeuRes assignment decoder · SAT formulas | performance | No clear effect |
Surprising findings
- Using negative literals at test time sometimes yields satisfying assignments before positive literals, despite no direct supervision on them.
- Trained models produce shorter proofs on unseen test formulas than on training formulas, marginally.
Limitations
- Standalone neural solver does not outperform highly engineered industrial SAT solvers.
- Python prototype is slower than the BooleForce C teacher solver in runtime (45 ms vs 4.5 ms average total).
- Full-Attn attention grid grows quadratically with the number of clauses.
Experimental setup
Datasets: SR(U(10,40)) generated formulas BooleForce teacher proofs SR(40) SR distributions from NeuroSAT
Benchmarks: SR(40) SR(U(10,40)) test set NeuroSAT SR distributions up to 5x larger variables
Metrics: proven rate (%) predicted accuracy (%) p-Len success rate runtime (ms)
Baselines: NeuroSAT BooleForce
Builds on: NeuroSAT expert iteration
Closest papers by meaning
- NSNet: A General Neural Probabilistic Framework for Satisfiability Problems (NeurIPS 2022 · similarity 0.90)
- Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach (ICLR 2019 · similarity 0.88)
- Grounding Neural Inference with Satisfiability Modulo Theories (NeurIPS 2023 · similarity 0.88)
- Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible (ICML 2025 · similarity 0.87)
- NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks (ICLR 2024 · similarity 0.87)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.87)
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.