May, 2022

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

PDF
TL;DR通过代数决策图和级联项目 - 加入树生成器，我们提出了动态规划最大可满足性（DPMS），一种解决广义 MaxSAT 问题的新方法。实证结果表明，DPMS 能够快速解决某些问题，由此开辟了未来更多研究的新方向。
boolean maxsatgeneralized formulationsdynamic-programming approachalgebraic decision diagramsdpms
发现论文，激发创造
  • 混合约束下的动态规划优化

    通过引入 DPMC 和 DPO，结合动态规划和代数决策图技术实现了精确求解更为一般化的最大概率解释问题 Boolean MPE，并在随机生成的混合子句 - 异或范式公式实验中显著优于目前的 MaxSAT 状态最优求解器。

    May, 2022

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

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

    Dec, 2023

  • DPER: 针对存在 - 随机难题的动态规划

    本研究将 graded project-join trees 上的动态规划方法扩展到了 ER-SSAT 问题，并实现了名为 DPER 的动态规划求解器。实证评估表明，DPER 在低宽度问题实例上具有与最先进的 ER-SSAT 求解器（DC-SSAT 和 erSSAT）竞争性相当的性能。

    May, 2022

  • SPUDD：使用决策图的随机计划

    本研究提出了一种基于代数决策图来表示价值函数和策略的 Markov 决策过程的值迭代算法，并将其应用于波西网络和 ADDs 表示的大规模 MDPs 中，相较于树形结构表示方式大幅降低了节点数量。

    Jan, 2013

  • 离散与连续状态 MDP 的符号动态规划

    本文介绍了符号动态规划（SDP）技术的扩展，提供了一种能够处理离散和连续状态的马尔可夫决策过程（DC-MDP）的最优解决方案，在 XADD 中引入约束基剪枝以提高效率。SDP 与 XADD 用于声明性问题的自动规划，从而实现在 DC-MDP 的线性和非线性函数中生成最优解决方案。

    Feb, 2012

  • 基于 ASP 的声明式流程挖掘（扩展摘要）

    本文提出了 ASP 作为建模和解决声明性流程挖掘领域中的问题的方法，着重讨论了日志生成、一致性检查和查询检查三个经典问题。该方法基于将过程规范表示为（有限状态）自动机，由此可以处理更一般的规范，例如在有限跟踪上的线性时态逻辑公式。

    May, 2022

  • 半定规划层次结构在图模型推断中的应用

    本文提出使用具有两个创新的二进制 SDP 松弛，同时聚焦于计算效率的 SOS 层次结构进行 MAP 推理，该算法在实际问题如图像去噪和 Ising 自旋玻璃方面表现优于 BP 和 GBP。

    Sep, 2017

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

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

    Dec, 2018

  • 基于代数决策图的加权模型计数

    使用动态规划算法和代数决策图作为主要数据结构来计算布尔公式的精确文字加权模型计数，并将该方法实现在 ADDMC 中，通过在 1914 个标准模型计数基准测试中的比较，展示 ADDMC 在加权模型计数上显著优于现有最佳的求解器。

    Jul, 2019

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

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

    Nov, 2022