SAT问题的机器学习：受限启发式和新图表示
摘要：布尔可满足性（SAT）是一个基本的NP完全问题，具有许多应用，包括自动规划和调度。为了解决大规模实例，SAT求解器必须依赖启发式方法，例如在DPLL和CDCL求解器中选择一个分支变量。这样的启发式方法可以通过机器学习（ML）模型得到改进；它们可以减少步骤的数量，但通常会降低运行时间，因为有效的模型相对较大且速度较慢。我们建议使用经过训练的ML模型进行几个初始步骤，然后释放控制权给传统的启发式方法；这简化了SAT求解的冷启动，并且可以减少步骤的数量和总运行时间，但需要单独决定何时将控制权释放给求解器。此外，我们介绍了一种修改过的Graph-Q-SAT方法，专门用于将SAT问题从其他领域转换而来，例如开放式车间调度问题。我们通过随机和工业SAT问题验证了我们的方法的可行性。
作者：Mikhail Shirokikh, Ilya Shenbin, Anton Alekseev, Sergey Nikolenko
论文ID：2307.09141
分类：Artificial Intelligence
分类简称：cs.AI
提交时间：2023-07-19