Automatically discovering heuristics in a complex SAT solver with large language models

TL;DR

This paper presents AutoModSAT, a novel approach using Large Language Models to automatically discover heuristics for complex SAT solvers, significantly improving performance and speed over existing methods.

Contribution

It introduces a new paradigm leveraging LLMs for heuristic discovery in SAT solvers, including solver design guidelines, automatic prompt optimization, and an efficient search strategy.

Findings

Achieves 50% performance improvement over baseline solvers

Outperforms state-of-the-art solvers by 30% in effectiveness

Attains 20% average speedup over parameter-tuned SOTA alternatives

Abstract

Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial applications, and it remains challenging to optimize modern SAT solvers in real-world settings due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces and yield limited performance gains. This work introduces a novel paradigm which effectively optimizes complex SAT solvers via Large Language Models (LLMs), and a tool called AutoModSAT is developed. Three fundamental challenges are addressed in order to achieve superior performance: (1) LLM-friendly solver: Systematic guidelines are proposed for developing a modularized solver to meet LLMs' compatibility, emphasizing code simplification, information share and bug reduction; (2) Automatic prompt optimization: An unsupervised automatic prompt optimization method is introduced to advance the diversity of LLMs' output; (3) Efficient search strategy: We design a presearch strategy and an EA evolutionary algorithm for the final efficient and effective discovery of heuristics. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves 50% performance improvement over the baseline solver and achieves 30% superiority against the state-of-the-art (SOTA) solvers. Moreover, AutoModSAT attains a 20% speedup on average compared to parameter-tuned alternatives of the SOTA solvers, showcasing the enhanced capability in handling complex problem instances. This work bridges the gap between AI-driven heuristics discovery and mission-critical system optimization, and provides both methodological advancements and empirically validated results for next-generation complex solver development.