利用大型语言模型在复杂的SAT求解器中发现启发式方法

《Nature Communications》：Discovering heuristics in a complex SAT solver with large language models

　　

摘要

可满足性问题（SAT）在计算复杂度理论中具有基础性地位，同时也在众多工业领域有着广泛应用。由于现代SAT求解器结构极为复杂，要在实际环境中对其进行优化是一项艰巨任务。虽然已有自动配置框架被开发出来，但它们仍依赖于人工设定的搜索空间。在此，我们提出了AutoModSAT这一框架，它利用大型语言模型自动优化SAT求解器。AutoModSAT结合了与大型语言模型兼容的模块化求解器设计、通过无监督提示词优化来增加生成函数的多样性，以及基于预搜索策略和(1 + λ)进化算法的高效搜索流程。在多种数据集上的大量实验表明，AutoModSAT相比基准求解器性能提升了40%，相比现有的最先进求解器则提升了30%。此外，在大多数测试数据集上，AutoModSAT的速度也明显快于经过参数调优的最先进求解器版本。这些结果充分展现了借助大型语言模型引导的启发式方法在优化复杂SAT求解器方面的巨大潜力。