Heuristics are crucial in SAT solvers, while no heuristic rules are suitable for all problem instances. Therefore, it typically requires to refine specific solvers for specific problem instances. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Large Models (LLMs) which is able to autonomously generate code, conduct evaluation, then utilize the 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 preliminary setup and model training, and fosters a Chain of Thought collaborative process with fault-tolerance, ensuring robust heuristic optimization. Extensive experiments on a Conflict-Driven Clause Learning (CDCL) solver demonstrates the overall superior performance of AutoSAT, especially in solving some specific SAT problem instances.

翻译：启发式方法在SAT求解器中至关重要，但没有任何启发式规则适用于所有问题实例。因此，通常需要针对特定问题实例调整特定求解器。在此背景下，我们提出了AutoSAT，一个用于自动优化SAT求解器中启发式方法的新颖框架。AutoSAT基于大语言模型（LLMs），能够自主生成代码、进行评测，并利用反馈进一步优化启发式方法，从而减少人工干预并增强求解器能力。AutoSAT以即插即用的方式运行，无需大量前期设置和模型训练，并支持具有容错性的思维链协作过程，确保启发式优化鲁棒。在基于冲突驱动子句学习（CDCL）求解器上的大量实验表明，AutoSAT整体性能优越，尤其在解决某些特定SAT问题实例时表现突出。