用大模型自动发现优化复杂SAT求解器的启发式规则，性能提升超40%。
Discovering heuristics in a complex SAT solver with large language models
- 用大模型生成并优化求解器模块，无需人工设定搜索范围。
- 在多个数据集上比基线提升40%，比现有最优解快30%。
- 适合对求解器性能有极致要求的工业场景或算法研究者。
可满足性问题（SAT）是计算复杂性理论的基础，在工业领域应用广泛。现代SAT求解器架构复杂，真实场景下的优化极具挑战性。尽管已有自动配置框架，但依赖人工约束的搜索空间。本文提出AutoModSAT框架，利用大语言模型（LLMs）自动优化SAT求解器。该框架结合了适配LLM的模块化求解器设计、无监督提示优化以多样化生成函数，以及基于预搜索策略和$(1+λ)$进化算法的高效搜索过程。在多种数据集上的大量实验表明，AutoModSAT相比基线求解器性能提升40%，相比当前最优求解器提升30%。此外，在多数测试数据集上，其速度显著优于经参数调优的最优求解器。结果表明，大模型引导的启发式发现具有优化复杂SAT求解器的巨大潜力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。