The Satisfiability problem (SAT) is fundamental in computational complexity theory and has a wide range of industrial applications. Optimizing modern SAT solvers in real-world settings is quite challenging due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces. Here we develop AutoModSAT, a framework that uses large language models (LLMs) to automatically optimize SAT solvers. AutoModSAT combines an LLM-compatible modular solver design, unsupervised prompt optimization to diversify generated functions, and an efficient search procedure based on presearch strategy and a $(1+λ)$ evolutionary algorithm. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves $40\%$ performance improvement over the baseline solver and $30\%$ improvement over the state-of-the-art solvers. Moreover, AutoModSAT also attains a notable speedup compared to the parameter-tuned alternatives of the state-of-the-art solvers over most of the test datasets. These results demonstrate the potential of LLM-guided heuristic discovery for optimizing complex SAT solvers.

翻译：可满足性问题（SAT）是计算复杂性理论中的基础问题，并在工业领域具有广泛应用。由于现代SAT求解器架构复杂，在真实场景中优化它们极具挑战性。尽管已有自动配置框架，但这些框架依赖于人工约束的搜索空间。本文开发了AutoModSAT框架，该框架利用大型语言模型自动优化SAT求解器。AutoModSAT结合了与LLM兼容的模块化求解器设计、用于多样化生成函数的无监督提示优化，以及基于预搜索策略和$(1+λ)$进化算法的高效搜索流程。在多种数据集上进行的大量实验表明，相较于基线求解器，AutoModSAT实现了$40\%$的性能提升，相较于最先进的求解器则实现了$30\%$的提升。此外，在大多数测试数据集上，与经过参数调优的最先进求解器替代方案相比，AutoModSAT还实现了显著的加速。这些结果展示了LLM引导的启发式发现方法在优化复杂SAT求解器方面的潜力。