Research map / Learning theory and algorithms / Combinatorial and search optimization
SAT and model counting solvers
Improves satisfiability, model counting and pseudo-Boolean solving with learned heuristics and proof certification.
89 accepted papers at ICML, NeurIPS, ICLR, CVPR and AAAI (2016–2026) · an approach in Combinatorial and search optimization, keyword cluster “logic · sat · boolean”
State History Tried Preprints Who Export
Where it stands
Not enough benchmark data Fewer than four papers report the same benchmark, so there is no record to follow.
22 papers in 2023–24 and 21 in 2025–26 (at ICML, NeurIPS, ICLR, CVPR and AAAI); its share of the topic held steady, from 6.3% to 5.8%.
How this is decided
A benchmark is tracked when at least four papers of this approach report their own method on the same dataset and metric in at least two different years. Its record is the best number reported up to 2024 compared with the best reported in 2025–26: still improving means at least 1% better, flat means at most 0.2% better with at least two papers from 2025–26 trying. Numbers on a different scale from the rest (a fraction among percentages) and far outliers are left out. Results come from different papers with different setups, so they are signals, not head-to-head comparisons. The share of papers is counted at ICML, NeurIPS, ICLR, CVPR and AAAI.
How it got here
Most cited paper of each year
- 2016 · The Complexity of LTL on Finite Traces: Hard and Easy Fragments (AAAI 2016 · 25 citations)
- 2017 · Maximum Model Counting (AAAI 2017 · 25 citations)
- 2018 · Schur Number Five (AAAI 2018 · 54 citations)
- 2019 · BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting (AAAI 2019 · 94 citations)
- 2020 · Justifying All Differences Using Pseudo-Boolean Reasoning (AAAI 2020 · 17 citations)
- 2021 · Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs (AAAI 2021 · 18 citations)
- 2022 · Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (AAAI 2022 · 11 citations)
- 2023 · Circuit Minimization with QBF-Based Exact Synthesis (AAAI 2023 · 8 citations)
- 2024 · An Approximate Skolem Function Counter (AAAI 2024 · 2 citations)
- 2025 · Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization (AAAI 2025 · 2 citations)
- 2026 · A Knowledge Compilation Map for Quantum Information (AAAI 2026 · 2 citations)
Earliest papers here
- The Complexity of LTL on Finite Traces: Hard and Easy Fragments (AAAI 2016 · 25 citations)
- Component Caching in Hybrid Domains with Piecewise Polynomial Densities (AAAI 2016 · 20 citations)
- SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators (AAAI 2016 · 8 citations)
What has been tried
67 papers here report 404 measured changes (a component added, removed or swapped, compared with a baseline): helped 75%, no clear effect 5%, hurt 15%, mixed 5%. Papers mostly publish changes that helped, so "helped" is over-represented.
Ablations in recent papers
| What was changed | Measured on | Result | Effect | Paper |
|---|---|---|---|---|
| Partition linear constraints | Small-SAT · Deciding SAT time (s) | 5 528 ± 1 498 -> 9 ± 1 | Helped | CEGAR-Based Approach for Solving Combinatorial Optimization Modulo Quantified Linear Arithmetics Problems (AAAI 2024 · 2 citations) |
| Use bottom-up instead of top-down constraint compilation | Sensor placement · instances completed | 580 -> 638 | Helped | Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · 2 citations) |
| Add budgeting propagation | Random algebra samples, orders 16–256 · instances solved within 30 minutes | Helped | SAT-Based Techniques for Lexicographically Smallest Finite Models (AAAI 2024 · 2 citations) | |
| Add reward replay to PPO | Topology-design training · training convergence time | 24% | Helped | AI-Powered Algorithm-Centric Quantum Processor Topology Design (AAAI 2025 · 0 citations) |
| add CAS-generated symmetry-breaking blocking clauses | R(3,7), 23 vertices · solve time | 2 minutes vs. could not solve it in 24 hours | Helped | A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract) (AAAI 2024 · 0 citations) |
Recent preprints
Loading recent arXiv preprints…
Who publishes on it
Institutions on the most papers of this approach since 2023 (of 43 papers; from OpenAlex and the papers' affiliations).
- National Taiwan University · 4 papers
- University of Toronto · 4 papers
- National University of Singapore · 3 papers
- Czech Technical University in Prague · 3 papers
- Georgia Institute of Technology · 3 papers
- Algorithms and Complexity Group · 2 papers
- Independent Researcher · 2 papers
- University of Windsor · 2 papers
- Friedrich Schiller University Jena · 2 papers
- NOVA FCT · 2 papers
Use it
Download BibTeX of 40 key papersOpen the topic in the interactive map
Get alerts. Describe your idea in scime atlas and save it (free scime account): you get a weekly email when new preprints land close to it.
Related approaches
Same keyword cluster
- Logic and answer set programming theory (150 papers)
- Structure and complexity of constraint reasoning (92 papers)
- Differentiable and symbolic reasoning (56 papers)
Elsewhere in the topic
- Heuristic and local search algorithms (147 papers)
- Classical and HTN planning (145 papers)
- Unsupervised neural combinatorial optimization (113 papers)
- Constrained neural network optimization (111 papers)
- Decision-focused optimization (97 papers)
- Multi-objective optimization (93 papers)
- Predict-then-optimize learning (89 papers)
- Heuristics for integer programming (60 papers)
Benchmark numbers, ablations and baseline numbers are extracted by AI from each paper's full text and can be wrong; the paper is the authority. Data: results index of 2026-11-02, citation counts from OpenAlex (2026-10-09).