Heuristics are crucial in SAT solvers, but no heuristic rules are suitable for all SAT problems. Therefore, it is helpful to refine specific heuristics for specific problems. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Language Models (LLMs) which is able to autonomously generate codes, conduct evaluation, and then utilize feedback to further optimize heuristics, thereby reducing human intervention and enhancing solver capabilities. AutoSAT operates on a plug-and-play basis, eliminating the need for extensive enterprise and model training, and fosters a Multi-Agent-based collaborative process with fault tolerance to ensure robust heuristic optimization. We implement AutoSAT on a lightweight Conflict-Driven Clause Learning (CDCL) solver EasySAT (the volume of EasySAT is about one-fiftieth of the State-of-the-Art hybrid solver Kissat) and extensive experiments on seven datasets demonstrate its superior performance. Out of the seven testing datasets, AutoSAT shows a superior performance to Kissat in two datasets and displays an overall similar performance in three datasets. Some heuristics generated by AutoSAT are even counter-intuitive but are very effective.

翻译：启发式策略在SAT求解器中至关重要，但不存在适用于所有SAT问题的通用启发式规则。因此，针对特定问题优化专用启发式策略具有重要价值。在此背景下，我们提出AutoSAT——一种用于自动优化SAT求解器启发式策略的新型框架。AutoSAT基于大语言模型（LLMs），能够自主生成代码、执行评估，并利用反馈进一步优化启发式策略，从而减少人工干预并提升求解器性能。AutoSAT采用即插即用机制，无需大量工程投入与模型训练，并通过基于多智能体的容错协作流程确保启发式优化的鲁棒性。我们在轻量级冲突驱动子句学习（CDCL）求解器EasySAT（其代码规模约为当前最先进混合求解器Kissat的五十分之一）上实现了AutoSAT，并在七个数据集上的大量实验证明了其优越性能。在七个测试数据集中，AutoSAT在两个数据集上表现优于Kissat，在三个数据集上呈现总体相当的性能。AutoSAT生成的某些启发式策略甚至反直觉却极为有效。