# AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

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

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 54 references that are in the map.
- First posted on arXiv 16 Feb 2024.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Qwen Technical Report](https://mlsanity.com/paper/2309.16609/) (2023)
- [CAMEL: Communicative Agents for "Mind" Exploration of Large Language Model Society](https://mlsanity.com/paper/2303.17760/) (2023)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023)
- [A Comprehensive Overview of Large Language Models](https://mlsanity.com/paper/2307.06435/) (2023)
- [AgentVerse: Facilitating Multi-Agent Collaboration and Exploring Emergent Behaviors](https://mlsanity.com/paper/2308.10848/) (2023)
- [Eureka: Human-Level Reward Design via Coding Large Language Models](https://mlsanity.com/paper/2310.12931/) (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)
- [Auto-GPT for Online Decision Making: Benchmarks and Additional Opinions](https://mlsanity.com/paper/2306.02224/) (2023)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [SwiftSage: A Generative Agent with Fast and Slow Thinking for Complex Interactive Tasks](https://mlsanity.com/paper/2305.17390/) (2023)
- [Cognitive Mirage: A Review of Hallucinations in Large Language Models](https://mlsanity.com/paper/2309.06794/) (2023)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Let the Flows Tell: Solving Graph Combinatorial Optimization Problems with GFlowNets](https://mlsanity.com/paper/2305.17010/) (2023)
- [Flows: Building Blocks of Reasoning and Collaborating AI](https://mlsanity.com/paper/2308.01285/) (2023)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [Survey on Evolutionary Deep Learning: Principles, Algorithms, Applications and Open Issues](https://mlsanity.com/paper/2208.10658/) (2022)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)

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

- [Can Large Language Models Reason? A Characterization via 3-SAT](https://mlsanity.com/paper/2408.07215/) (2024)
- [Deep Insights into Automated Optimization with Large Language Models and Evolutionary Algorithms](https://mlsanity.com/paper/2410.20848/) (2024)
- [Generalizable Heuristic Generation Through LLMs with Meta-Optimization](https://mlsanity.com/paper/2505.20881/) (2025)
- [Large Language Models in Operations Research: Methods, Applications, and Challenges](https://mlsanity.com/paper/2509.18180/) (2025)
- [Discovering heuristics in a complex SAT solver with large language models](https://mlsanity.com/paper/2507.22876/) (2025)
- [STRCMP: Integrating Graph Structural Priors with Language Models for Combinatorial Optimization](https://mlsanity.com/paper/2506.11057/) (2025)
- [Refining Hybrid Genetic Search for CVRP via Reinforcement Learning-Finetuned LLM](https://mlsanity.com/paper/2510.11121/) (2025)
- [Canonical Intermediate Representation for LLM-based optimization problem formulation and code generation](https://mlsanity.com/paper/2602.02029/) (2026)
- [How Large Language Models Need Symbolism](https://mlsanity.com/paper/2509.21404/) (2025)
- [IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking](https://mlsanity.com/paper/2604.03232/) (2026)
- [Agentic MIP Research: Accelerated Constraint Handler Generation](https://mlsanity.com/paper/2605.09186/) (2026)
- [MiniOpt: Reasoning to Model and Solve General Optimization Problems with Limited Resources](https://mlsanity.com/paper/2606.25832/) (2026)
- [An Information-Theoretic Criterion for Efficient Data Synthesis](https://mlsanity.com/paper/2605.16379/) (2026)
- [Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience](https://mlsanity.com/paper/2607.14818/) (2026)
- [From Hand-Crafted to LLM-Based Variation Operators in Metaheuristics: A Tutorial](https://mlsanity.com/paper/2609.31649/) (2026)

## Abstract (arXiv)

Conflict-Driven Clause Learning (CDCL) is the mainstream framework for solving the Satisfiability problem (SAT), and CDCL solvers typically rely on various heuristics, which have a significant impact on their performance. Modern CDCL solvers, such as MiniSat and Kissat, commonly incorporate several heuristics and select one to use according to simple rules, requiring significant time and expert effort to fine-tune in practice. The pervasion of Large Language Models (LLMs) provides a potential solution to address this issue. However, generating a CDCL solver from scratch is not effective due to the complexity and context volume of SAT solvers. Instead, we propose AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers. Unlike existing automated algorithm design approaches focusing on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics. In this first attempt at optimizing SAT solvers using LLMs, several strategies including the greedy hill climber and (1+1) Evolutionary Algorithm are employed to guide LLMs to search for better heuristics. Experimental results demonstrate that LLMs can generally enhance the performance of CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.