Boolean satisfiability, the SAT problem, is the engine beneath a vast range of computing tasks, from chip verification to cybersecurity to formal proof checking. The algorithms that solve it have been refined by human experts over decades, incrementally improving performance through clever heuristics for variable selection, clause reduction, and restart timing.
A study published in Nature Communications on July 17 shows that large language models can now generate SAT solver heuristics that outperform human-designed ones, achieving a 40% improvement in runtime over a baseline solver and beating the best parameter-tuned versions of state-of-the-art systems on 8 of 11 benchmark datasets.
What the Researchers Did
The team, led by Ke Wei of Fudan University and Shaowei Cai of the Chinese Academy of Sciences, built a framework called AutoModSAT. The key insight was that SAT solver codebases are massive and tangled, the popular Kissat solver runs to 250,000 tokens. Asking an LLM to modify such a codebase directly would be hopeless. Instead, the researchers modularized a CDCL (conflict-driven clause learning) solver, exposing exactly seven heuristic functions, restart timing, clause reduction, variable activity bumping, and others, as a clean search space.
With the solver modularized, the system cycles through three LLM agents: a Coder generates new C++ heuristic code, an Evaluator filters out code that is semantically identical to existing heuristics, and a Repairer fixes compilation errors. The best-performing heuristics are kept in an evolutionary loop. The entire process uses 50 LLM calls per problem domain and relies on DeepSeek-V3, chosen for its competitive performance at low cost.
What It Found
On 11 benchmark datasets spanning SAT Competition problems, EDA (electronic design automation) verification, and combinatorial puzzles, AutoModSAT generated optimized heuristics that delivered a 40% average improvement in PAR-2 score (a standard metric that penalizes unsolved instances) over the baseline modular solver.
Compared with parameter-tuned versions of state-of-the-art solvers Kissat and CaDiCaL, AutoModSAT won on 8 of 11 datasets with roughly a 20% average speedup. On the register-allocation problem, the LLM-discovered heuristic solved 18 of 20 instances while the baseline managed fewer than 6. On the hashtable-safety verification problem, with 11.7 million variables and 53.6 million clauses, AutoModSAT produced a PAR-2 score of 3,302 against the best competitor’s 7,322.
The LLM also invented heuristics that had not previously been described in the literature. For restart strategy, it generated a dynamic method using moving averages of clause quality scores, a novel approach that was not part of any existing solver.
Why It Matters
This is qualitatively different from automated hyperparameter tuning, which adjusts existing knobs. AutoModSAT generates new algorithmic code, heuristics that human experts had not conceived. The total cost is a few dollars in API fees per optimization run, making it practical for real industrial deployment.
The modularization approach itself is the paper’s strongest claim: making solver code LLM-friendly is not optional but foundational. The approach could extend to other complex solvers for mixed-integer programming, constraint satisfaction, and theorem proving.
Caveats
The baseline solver (ModSAT) is simpler than state-of-the-art systems like Kissat, which have decades of optimization. Some gains reflect the baseline’s relative weakness. The framework only exposes seven heuristic functions and cannot touch top-level preprocessing parameters, which are critical on some datasets. On the Zamkeller dataset, parameter-tuned Kissat beat AutoModSAT by a factor of four because the gap was in a component the system could not modify.
The paper is published in Nature Communications (DOI: 10.1038/s41467-026-74949-2) by Y. Sun, F. Ye, Z. Chen, K. Wei, and S. Cai.
Sources
1. Y. Sun, F. Ye, Z. Chen, K. Wei, S. Cai, “Discovering Heuristics in a Complex SAT Solver with Large Language Models,” Nature Communications (2026). DOI: 10.1038/s41467-026-74949-2