学习可解释的 WalkSAT 启发式方法
布尔可满足性 (SAT) 是一个基础的 NP-complete 问题,具有许多应用,包括自动计划和调度。为了解决大规模的情况,SAT 求解器必须依赖启发式算法,如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法,通过减少步数来降低运行时间,但是由于有用的模型相对较大和较慢,这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤,然后将控制权交给经典启发式算法,这简化了 SAT 求解的冷启动,并可以减少步数和总运行时间,但需要单独决定何时将控制权交给求解器。此外,我们介绍了一种改进的 Graph-Q-SAT,专门针对从其他领域转换而来的 SAT 问题,例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。
Jul, 2023
建议并评估了一种系统,该系统学习了一种用于基于正向搜索的满足经典规划的神经网络启发式函数。我们的系统从头开始学习目标估计器,并生成训练数据。通过反向回归搜索或通过反向搜索从给定或猜测的目标状态生成培训数据。
Jun, 2023
本文介绍了一种结合 solution prediction model 和神经网络的方法 ——NLocalSAT,用于提高 stochastic local search 在解 Boolean satisfiability problem 时的有效性,并且在 SAT Competition 2018 的实验中取得了 27% ~ 62% 的性能提升。
Jan, 2020
研究领域特定规划的学习启发式,通过学习排名问题,引入了新的方法来计算捕获近似计划中的时间交互的特征。在最近的国际规划竞赛问题上进行的实验表明,RankSVM 学习启发式优于原始启发式和通过普通回归学习的启发式。
Aug, 2016
应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性(SAT)问题,并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器,我们对现有的最先进模型进行训练,以预测具有 10,000 个变量的公式的可满足性,提出了新的分类器,可以对大多数困难水平的相同数据集进行显着改进,从而打破了过去基于公式的句法特征学习的方法,并使用求解器计算的简短前缀进行学习。
Nov, 2022
本文介绍了使用图神经网络进行函数逼近的增强学习的 Graph-Q-SAT 分支启发式算法,该算法可用于解决 SAT 问题,并且在使用 MiniSat 求解器进行交互时可以减少解决 SAT 问题所需的迭代次数 2-3 倍。
Sep, 2019
使用 SaIL 特有的算法,训练启发式策略来遍历搜索树中的节点,以减少搜索次数。实验证明 SaIL 算法在实时规划环境中优于现有算法,这为学习体现 ' 快速找到可行解并随时间增量调整 ' 的启发式方法铺平了道路。
Jul, 2017
本论文研究了使用随机局部搜索解决基于满足性问题的 SAT 问题的流行范式,以及通过学习逻辑蕴含来改善求解器性能,并提出了一种生成逻辑等价问题形式的方法,进一步深入研究学习逻辑蕴含如何影响 SLS 运行时间的问题。
Oct, 2022
我们对神经网络与组合优化中的局部搜索算法进行了综合研究,结果表明基于禁忌搜索的简单学习启发式方法在性能和泛化性方面超过了最先进的学习启发式方法,挑战了现有假设,并为组合优化的未来研究和创新开辟了新的方向。
Oct, 2023