Abstract
Satisfiability problem (SAT) is a cornerstone of computational complexitywith broad industrial applications, and it remains challenging to optimizemodern SAT solvers in real-world settings due to their intricate architectures.While automatic configuration frameworks have been developed, they rely onmanually constrained search spaces and yield limited performance gains. Thiswork introduces a novel paradigm which effectively optimizes complex SATsolvers via Large Language Models (LLMs), and a tool called AutoModSAT isdeveloped. Three fundamental challenges are addressed in order to achievesuperior performance: (1) LLM-friendly solver: Systematic guidelines areproposed 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 optimizationmethod is introduced to advance the diversity of LLMs' output; (3) Efficientsearch strategy: We design a presearch strategy and an EA evolutionaryalgorithm for the final efficient and effective discovery of heuristics.Extensive experiments across a wide range of datasets demonstrate thatAutoModSAT achieves 50% performance improvement over the baseline solver andachieves 30% superiority against the state-of-the-art (SOTA) solvers. Moreover,AutoModSAT attains a 20% speedup on average compared to parameter-tunedalternatives of the SOTA solvers, showcasing the enhanced capability inhandling complex problem instances. This work bridges the gap between AI-drivenheuristics discovery and mission-critical system optimization, and providesboth methodological advancements and empirically validated results fornext-generation complex solver development.