UpMax:用戶分區的 MaxSAT
本研究分析了现有的基于不可满足子公式识别的最大可满足性问题(MaxSAT)算法,并提出了几个关键性优化和新的替代算法,这些优化和新算法在实际应用中的 MaxSAT 实例上提供了显着的性能提升。
Dec, 2007
本研究使用 MaxSAT 问题中的 SPB 约束和子句权重技术,提出了一种新的局部搜索算法 SPB-MaxSAT,为 MaxSAT 局部搜索求解器的子句权重方法提供了新的视角和优秀的性能。
Jan, 2024
本文提出了两种近似策略来改进不完全解决 MaxSAT 问题,并通过在 MaxSAT 评估 2017 中实验结果表明,这两种策略能够比最佳不完全求解器找到更好的解决方案。这两种策略分别是:通过聚类并用代表权重近似表示,以及将求解无法满足的子句权重之和最小化的问题分解成多个最小化子问题。
Jun, 2018
该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT,用于解决不同类型的布尔可满足性问题,包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数,构建了统一的整数规划表示方法,并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构,在 SAT 问题上应用了蒙特卡罗树搜索(MCTS)方法,证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明,该方法能够剪枝不必要的搜索空间,找到问题的最优布尔赋值,同时为 SAT 问题的监督学习方法提供多样的标签。
Dec, 2023
本文提出了一种将搜索方法与半定规划方法相结合的算法,其用于解决 MAX2SAT 问题。文中称,使用这种方法能够显著提高问题的解决速度,并在一些问题上取得了 order of magnitude 级别的速度提升。
Dec, 2018
本文提出了一种新的问题转化方法,将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题,并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。
May, 2017
本文提出了一种新的路线,即通过引入可微(平滑)的最大可满足性(MAXSAT)求解器,将逻辑推理纳入更大的深度学习系统的循环中,从而在端到端学习系统中学习有挑战性的问题的逻辑结构,表现出集成逻辑结构于深度学习的潜力。
May, 2019
该研究提出了一种基于 MAX-SAT 的错误定位算法,通过符号执行,将程序的追踪记录编码为布尔可满足公式,构造出不可满足公式,并使用 MAX-SAT 找到可能的错误原因集合,其算法实现在名为 bug-assist 的工具中,并可以自动为普遍的错误类型建议修复。
Nov, 2010