AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

📄 arXiv: 2402.10705v3 📥 PDF

作者: Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, Shaowei Cai

分类: cs.AI

发布日期: 2024-02-16 (更新: 2024-11-13)

💡 一句话要点

提出AutoSAT以自动优化SAT求解器的启发式算法

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: SAT求解 启发式算法 自动化优化 大型语言模型 CDCL求解器 算法设计 性能提升

📋 核心要点

  1. 现有CDCL求解器依赖多种启发式算法，调优过程复杂且耗时，影响求解器性能。
  2. AutoSAT框架利用大型语言模型自动优化启发式算法，能够在预定义的搜索空间中生成新算法。
  3. 实验结果显示，AutoSAT在多个数据集上超越了传统求解器，展现出良好的性能提升。

📝 摘要（中文）

冲突驱动子句学习（CDCL）是解决可满足性问题（SAT）的主流框架，现有的CDCL求解器依赖多种启发式算法，且这些算法的选择对性能影响显著。传统求解器如MiniSat和Kissat通常需要专家进行复杂的调优。本文提出的AutoSAT框架利用大型语言模型（LLMs）在预定义的模块化搜索空间中自动优化启发式算法。与现有的自动化算法设计方法不同，AutoSAT能够生成新的高效启发式算法。实验结果表明，LLMs能够显著提升CDCL求解器的性能，AutoSAT在12个数据集中的9个上超越了MiniSat，并在4个数据集上超过了最先进的混合求解器Kissat。

🔬 方法详解

问题定义：本文旨在解决现有CDCL求解器在启发式算法选择上的复杂性和效率问题。现有方法依赖人工调优，导致性能不稳定且耗时。

核心思路：AutoSAT框架通过利用大型语言模型（LLMs）在预定义的模块化搜索空间中自动优化启发式算法，旨在生成新的高效启发式，而非仅仅进行超参数调优。

技术框架：AutoSAT的整体架构包括多个模块，首先是基于现有CDCL求解器的启发式算法库，然后通过LLMs进行搜索和优化，最后评估生成的启发式算法的性能。

关键创新：AutoSAT的主要创新在于其能够生成新的启发式算法，而不仅仅是优化现有的超参数或选择操作符。这种方法利用了LLMs的强大生成能力，显著提升了求解器的性能。

关键设计：在设计中，AutoSAT采用了贪婪爬山算法和(1+1)进化算法等策略来引导LLMs搜索更优的启发式算法，确保生成的算法在性能上具有优势。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，AutoSAT在12个数据集中的9个上超越了MiniSat，并在4个数据集上超过了最先进的混合求解器Kissat，展示了LLMs在优化SAT求解器中的有效性和潜力。

🎯 应用场景

AutoSAT的研究成果在SAT求解领域具有广泛的应用潜力，能够为各种组合优化问题提供高效的求解方案。其自动化的特性将降低对专家知识的依赖，提升求解器的普适性和适应性，未来可扩展到其他领域的算法优化中。

📄 摘要（原文）

Conflict-Driven Clause Learning (CDCL) is the mainstream framework for solving the Satisfiability problem (SAT), and CDCL solvers typically rely on various heuristics, which have a significant impact on their performance. Modern CDCL solvers, such as MiniSat and Kissat, commonly incorporate several heuristics and select one to use according to simple rules, requiring significant time and expert effort to fine-tune in practice. The pervasion of Large Language Models (LLMs) provides a potential solution to address this issue. However, generating a CDCL solver from scratch is not effective due to the complexity and context volume of SAT solvers. Instead, we propose AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers. Unlike existing automated algorithm design approaches focusing on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics. In this first attempt at optimizing SAT solvers using LLMs, several strategies including the greedy hill climber and (1+1) Evolutionary Algorithm are employed to guide LLMs to search for better heuristics. Experimental results demonstrate that LLMs can generally enhance the performance of CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.