Dec, 2023

解决四类 SAT 问题的通用方法

PDF
TL;DR该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT，用于解决不同类型的布尔可满足性问题，包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数，构建了统一的整数规划表示方法，并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构，在 SAT 问题上应用了蒙特卡罗树搜索（MCTS）方法，证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明，该方法能够剪枝不必要的搜索空间，找到问题的最优布尔赋值，同时为 SAT 问题的监督学习方法提供多样的标签。
发现论文，激发创造
  • SAT 问题的机器学习：约束启发式和新的图表示

    布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法，通过减少步数来降低运行时间，但是由于有用的模型相对较大和较慢，这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤，然后将控制权交给经典启发式算法，这简化了 SAT 求解的冷启动，并可以减少步数和总运行时间，但需要单独决定何时将控制权交给求解器。此外，我们介绍了一种改进的 Graph-Q-SAT，专门针对从其他领域转换而来的 SAT 问题，例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。

    Jul, 2023

  • 结合多臂老虎机和局部搜索的 MaxSAT 算法

    本文提出了一种基于多臂赌博机的本地搜索算法 BandHS 用来解决 MaxSAT 及其两个泛化问题，和一个初始化方法优化算法的表现。经过大量实验证明，本文提出的方法在解决 MaxSAT 问题时表现出色。

    Nov, 2022

  • DPMS：基于 ADD 的符号化方法解决广义 MaxSAT 问题

    通过代数决策图和级联项目 - 加入树生成器，我们提出了动态规划最大可满足性（DPMS），一种解决广义 MaxSAT 问题的新方法。实证结果表明，DPMS 能够快速解决某些问题，由此开辟了未来更多研究的新方向。

    May, 2022

  • 利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

    利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

    Sep, 2023

  • 分而治之：约束满足问题的通用方法

    介绍一种用几何模型来解决多约束条件优化问题的方法，并在布尔可满足性问题和球体堆积问题两个基准测试中说明了其有效性和竞争性。

    Dec, 2007

  • 解决布尔可满足性问题的机器学习方法

    本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

    Mar, 2022

  • 用低秩半定规划解决 MAX2SAT 问题

    本文提出了一种将搜索方法与半定规划方法相结合的算法，其用于解决 MAX2SAT 问题。文中称，使用这种方法能够显著提高问题的解决速度，并在一些问题上取得了 order of magnitude 级别的速度提升。

    Dec, 2018

  • 重新思考 MaxSAT 局部搜索求解器中的软冲突伪布尔约束

    本研究使用 MaxSAT 问题中的 SPB 约束和子句权重技术，提出了一种新的局部搜索算法 SPB-MaxSAT，为 MaxSAT 局部搜索求解器的子句权重方法提供了新的视角和优秀的性能。

    Jan, 2024

  • 用概率方法扩展机器学习以解决组合优化问题的隐蔽博弈

    应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 10,000 个变量的公式的可满足性，提出了新的分类器，可以对大多数困难水平的相同数据集进行显着改进，从而打破了过去基于公式的句法特征学习的方法，并使用求解器计算的简短前缀进行学习。

    Nov, 2022

  • 挑战 SAT 求解中分辨率限制

    本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。

    May, 2017