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.

翻译：冲突驱动子句学习（CDCL）是解决可满足性问题（SAT）的主流框架，CDCL求解器通常依赖多种启发式策略，这些策略对其性能具有显著影响。现代CDCL求解器（如MiniSat和Kissat）通常集成多种启发式方法，并依据简单规则选择使用，在实际应用中需要耗费大量时间和专家精力进行调优。大语言模型（LLMs）的普及为这一问题提供了潜在的解决方案。然而，由于SAT求解器的复杂性和上下文规模，从头生成CDCL求解器并不现实。为此，我们提出AutoSAT框架，该框架基于现有CDCL求解器，在预定义的模块化搜索空间中自动优化启发式策略。与现有专注于超参数调优和算子选择的自动化算法设计方法不同，AutoSAT能够生成全新的高效启发式策略。在此次使用LLMs优化SAT求解器的首次尝试中，我们采用包括贪婪爬山法和(1+1)进化算法在内的多种策略来引导LLMs搜索更优的启发式方法。实验结果表明，LLMs能够普遍提升CDCL求解器的性能。AutoSAT的一个实现版本在12个数据集中的9个上优于MiniSat，甚至在4个数据集上超越了当前最先进的混合求解器Kissat。