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.

AutoSAT 是一种自动优化 SAT 解算器中启发式算法的新框架，基于大型模型（LLMs），它能够自主生成代码、进行评估，并利用反馈进一步优化启发式算法，从而减少人工干预并增强解算器的能力。AutoSAT 在插拔式基础上操作，不需要广泛的预备设置和模型训练，促进了具有容错性的思维链的合作过程，确保了强大的启发式优化。对 Conflict-Driven Clause Learning (CDCL) 解算器进行的大量实验证明了 AutoSAT 的整体优异性能，特别是在解决一些特定的 SAT 问题实例中。