Discovering heuristics in a complex SAT solver with large language models

Area of Science:

• Computer Science
• Artificial Intelligence
• Computational Complexity Theory

Background:

• The Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial relevance.
• Optimizing complex SAT solvers is challenging due to intricate architectures and manually constrained configuration frameworks.

Purpose of the Study:

• To develop AutoModSAT, a novel framework leveraging large language models (LLMs) for automated SAT solver optimization.
• To overcome limitations of existing automatic configuration methods by enabling LLM-driven heuristic discovery.

Main Methods:

• Designed an LLM-compatible modular SAT solver architecture.
• Employed unsupervised prompt optimization for diverse function generation.
• Implemented an efficient search procedure incorporating presearch strategy and a (1+λ) evolutionary algorithm.

Main Results:

• AutoModSAT demonstrated a 40% performance improvement over the baseline SAT solver.
• Achieved a 30% performance enhancement compared to state-of-the-art solvers.
• Showcased notable speedup against parameter-tuned state-of-the-art solver alternatives.

Conclusions:

• AutoModSAT effectively utilizes LLM-guided heuristic discovery for optimizing complex SAT solvers.
• The framework offers a promising direction for advancing SAT solver performance and efficiency.
• Highlights the potential of AI in tackling fundamental challenges in computational complexity.