arXiv:2501.14630v2 宣告类型: 修改 摘要: 局部搜索预处理通过提供高质量的起始点使冲突驱动子句学习（CDCL）求解器速度更快，现代SAT求解器已经将这种技术融入到它们的预处理步骤中。然而，这些工具依赖于基本策略，这些策略未能捕捉问题中的结构性模式。我们提出了一种方法，该方法利用大型语言模型（LLMs）分析基于Python的编码代码。这揭示了问题转换为SAT隐藏的结构性模式。该方法自动生成专门的局部搜索算法，寻找这些模式并使用它们创建强大的初始分配。这适用于同一编码类型下的任何问题实例。我们的测试表明取得了鼓舞人心的结果，与基准预处理系统相比，求解时间更快。