# Discovering heuristics in a complex SAT solver with large language models

arXiv: https://arxiv.org/abs/2507.22876 · HTML: https://mlsanity.com/paper/2507.22876/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 49 references that are in the map.
- First posted on arXiv 30 Jul 2025.

## Builds on (most cited first, 19 of 19)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Qwen Technical Report](https://mlsanity.com/paper/2309.16609/) (2023)
- [Large Language Models Are Human-Level Prompt Engineers](https://mlsanity.com/paper/2211.01910/) (2022)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Automatic Prompt Optimization with "Gradient Descent" and Beam Search](https://mlsanity.com/paper/2305.03495/) (2023)
- [CodeT5+: Open Code Large Language Models for Code Understanding and Generation](https://mlsanity.com/paper/2305.07922/) (2023)
- [ReEvo: Large Language Models as Hyper-Heuristics with Reflective Evolution](https://mlsanity.com/paper/2402.01145/) (2024)
- [Evolution of Heuristics: Towards Efficient Automatic Algorithm Design Using Large Language Model](https://mlsanity.com/paper/2401.02051/) (2024)
- [SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization](https://mlsanity.com/paper/2109.09831/) (2021)
- [HSEvo: Elevating Automatic Heuristic Design with Diversity-Driven Harmony Search and Genetic Algorithm Using LLMs](https://mlsanity.com/paper/2412.14995/) (2024)
- [A Systematic Survey on Large Language Models for Algorithm Design](https://mlsanity.com/paper/2410.14716/) (2024)
- [A Survey of Circuit Foundation Model: Foundation AI Models for VLSI Circuit Design and EDA](https://mlsanity.com/paper/2504.03711/) (2025)
- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [Benchmarking a (μ+λ) Genetic Algorithm with Configurable Crossover Probability](https://mlsanity.com/paper/2006.05889/) (2020)
- [Extracting Problem Structure with LLMs for Optimized SAT Local Search](https://mlsanity.com/paper/2501.14630/) (2025)
- [Towards a Theory-Guided Benchmarking Suite for Discrete Black-Box Optimization Heuristics: Profiling (1+λ) EA Variants on OneMax and LeadingOnes](https://mlsanity.com/paper/1808.05850/) (2018)

## Built on by (most cited first, 4 of 4)

- [Autonomous Code Evolution Meets NP-Completeness](https://mlsanity.com/paper/2509.07367/) (2025)
- [Agentic MIP Research: Accelerated Constraint Handler Generation](https://mlsanity.com/paper/2605.09186/) (2026)
- [An Information-Theoretic Criterion for Efficient Data Synthesis](https://mlsanity.com/paper/2605.16379/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

The Satisfiability problem (SAT) is fundamental in computational complexity theory and has a wide range of industrial applications. Optimizing modern SAT solvers in real-world settings is quite challenging due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces. Here we develop AutoModSAT, a framework that uses large language models (LLMs) to automatically optimize SAT solvers. AutoModSAT combines an LLM-compatible modular solver design, unsupervised prompt optimization to diversify generated functions, and an efficient search procedure based on presearch strategy and a (1+λ) evolutionary algorithm. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves 40% performance improvement over the baseline solver and 30% improvement over the state-of-the-art solvers. Moreover, AutoModSAT also attains a notable speedup compared to the parameter-tuned alternatives of the state-of-the-art solvers over most of the test datasets. These results demonstrate the potential of LLM-guided heuristic discovery for optimizing complex SAT solvers.