TLDR: SATLUTION, a novel AI agent framework, has successfully evolved C/C++ SAT solvers at a full repository scale, encompassing tens of thousands of lines of code. It leverages large language models, a self-evolving rule system, and distributed feedback to autonomously improve algorithms for the NP-complete Boolean Satisfiability (SAT) problem. The evolved solvers decisively outperformed human-designed champions of the SAT Competition 2025, demonstrating a significant leap in AI-driven software development and problem-solving efficiency.
Large Language Models (LLMs) have demonstrated impressive capabilities in generating and iteratively improving code. While previous efforts like AlphaEvolve showed promise in refining isolated code kernels, a new framework called SATLUTION is pushing the boundaries, extending LLM-based code evolution to entire software repositories, encompassing hundreds of files and tens of thousands of lines of C/C++ code.
SATLUTION specifically targets the Boolean Satisfiability (SAT) problem, a fundamental challenge in computer science known for its NP-complete complexity. SAT solving is crucial in various fields, including hardware verification, software analysis, and artificial intelligence. The framework orchestrates LLM agents to directly evolve SAT solver repositories, ensuring strict correctness guarantees and leveraging distributed runtime feedback. What’s more, SATLUTION also self-evolves its own evolution policies and rules, making it a truly adaptive system.
Outperforming Human Experts
Starting with codebases and benchmarks from the SAT Competition 2024, SATLUTION evolved solvers that decisively outperformed the human-designed winners of the SAT Competition 2025. It also surpassed both 2024 and 2025 champions when tested on the 2024 benchmarks. This achievement marks a significant milestone, demonstrating an AI agent’s ability to achieve champion-level performance in solving NP-complete problems at a repository scale.
The framework’s success is highlighted by its performance in the SAT Competition 2025. Despite being trained exclusively on 2024 data, SATLUTION’s evolved solvers achieved new state-of-the-art results, attaining the lowest PAR-2 scores (Penalized Average Runtime) among all entrants. This indicates both a greater number of solved instances and faster runtimes on average, proving its ability to generalize beyond its training environment.
How SATLUTION Works
SATLUTION operates through an autonomous agent-based code evolution system that iteratively improves SAT solvers. It features two main LLM-based stages: Planning and Coding. The Planning agent performs high-level reasoning, analyzing solver performance and proposing modification directions. The Coding agent then executes these plans by directly editing the solver repository, managing build configurations, fixing compilation errors, and debugging functional failures.
A crucial aspect of SATLUTION is its sophisticated rule system. This system provides structured guidance for planning, programming, and verification. It includes static initialization rules that embed basic SAT domain knowledge and critical correctness constraints, ensuring that agents evolve solvers without requiring deep SAT-specific expertise. Furthermore, the rule system itself is dynamic and self-evolving, adapting based on learnings from each evolution cycle, such as new failure patterns or process improvements.
Ensuring Correctness and Efficiency
To prevent the introduction of bugs or unsound behavior, each iteration of SATLUTION undergoes a stringent two-stage verification pipeline. The first stage involves compilation and a smoke test on trivial cases to catch immediate errors. If successful, the second stage performs full correctness validation on a larger set of benchmarks, verifying SAT solutions and validating UNSAT proofs using an external DRAT proof checker. Only correctly verified solvers proceed to performance evaluation.
Performance evaluation is conducted using a distributed runtime evaluator on a cluster of 800 CPU nodes, allowing for rapid feedback on how changes affect solver performance. Metrics like PAR-2 scores, number of solved instances (SAT and UNSAT), and memory usage guide the agent’s next steps. This massive parallelism enables near-immediate fitness assessment, maximizing evolutionary speed.
Also Read:
- AI System Automates Expert-Level Scientific Software Development
- CP-Model-Zoo: Simplifying Access to Constraint Programming Models with Natural Language
Learned Insights and Future Directions
Through its evolution, SATLUTION discovered novel solver-design insights, including refinements to clause learning strategies, bandit-based tuning for various heuristics (like vivification and UIP depth), improved reward design for optimization, and integration of symmetry-breaking techniques. These cumulative modifications expanded the repository by over 10,000 lines of code.
While highly automated, the framework currently benefits from semi-automated operation with targeted human intervention for complex errors. The research highlights the indispensable role of a carefully calibrated verifier, which was manually engineered, in enabling efficient and reliable repository-scale evolution. Future work aims for agents to autonomously construct and adapt their own verifiers, potentially transforming fields like electronic design automation (EDA) where correctness is paramount.
The entire self-evolution process, including token usage for coding agents and CPU time for distributed evaluation, incurred a total cost significantly lower than the implicit cost of human expert labor over months or years. This demonstrates the economic viability and efficiency of autonomous code evolution for complex problem-solving. For more detailed information, you can read the full research paper here.
