Bridging LLMs and SAT Solving: Automated Evolution of High-Performance Heuristics

摘要

Despite decades of intensive research and optimization, modern Boolean Satisfiability (SAT) solvers have reached a plateau where significant performance gains are increasingly difficult to achieve. While Large Language Models (LLMs) have demonstrated remarkable capabilities in pattern recognition and code generation for combinatorial optimization, their direct application to highly optimized SAT solvers remains a formidable challenge due to the extreme complexity and sensitivity of solver heuristics. In this paper, we introduce AESAT (Auto-Evolving SAT solving), a novel neuro-symbolic framework designed to automatically evolve and optimize the heuristic functions of SAT solvers. AESAT employs a memetic-inspired approach, synergizing LLM-guided individual optimization with evolutionary exploration. By leveraging self-optimized prompting techniques, our framework enables LLMs to iteratively discover and refine sophisticated heuristics that bypass the limitations of human-engineered designs. The efficacy of AESAT is demonstrated by its flagship derivative, AE-Kissat-MAB, which won the main track of the 2025 International SAT Competition by a wide margin. This result represents the first time an LLM-enhanced solver has dominated the world's premier SAT competition, marking a paradigm shift in the automated design of reasoning algorithms.