Oct, 2023

新的布尔可满足性问题启发式策略：最小正负乘积策略

PDF
TL;DR本研究提出了一种名为 “Minimal Positive Negative Product Strategy” 的新型启发式算法，用于指导 CDCL 算法解决布尔可满足性问题，它通过数学解释阐明了该算法相对于动态最大个体和变量状态独立衰减和求和等广泛使用的启发式算法的优势，实验结果进一步证实这种启发式策略在问题求解中的有效性。
heuristic algorithmcdcl algorithmboolean satisfiability problemminimal positive negative product strategyexperimental results
发现论文，激发创造
  • 驱动 CDCL 搜索

    通过嵌入特定领域的启发式方法来提高 CDCL 算法的性能并不容易，本文提出了一种通用框架来设计和实现新的启发式方法，并在两个工业领域实验中取得成功。

    Nov, 2016

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

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

    May, 2017

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

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

    Dec, 2023

  • IntSat: 基于冲突驱动约束学习的整数线性规划

    通过扩展冲突驱动子句学习技术，本文使用基于整数线性规划方法处理复杂的实际问题，并讨论该方法在优化方面的潜在改进。

    Feb, 2024

  • SAT 问题的机器学习：约束启发式和新的图表示

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

    Jul, 2023

  • 信息过载：CDCL 求解器为何需要遗忘已学子句

    文章发现适当的子句学习可以促进 CDCL 求解器的性能，但在某些情况下，此方法可能会大大降低求解过程，这主要来自 CDCL 求解器具有多峰运行时间分布。通过使用威布尔混合分布来描述这种多峰分布，得出遗忘子句在 CDCL 求解器中对于优化单元传播速度外还有其它应用的结论。

    Feb, 2022

  • 软件产品线中解决优先级成对测试数据生成问题的 CMSA 算法

    软件产品线中的优先级配对测试数据生成问题是一个重要的挑战，传统的算法在大规模问题上无法达到合理时间复杂度，因此我们提出了一个名为 Construct, Merge, Solve & Adapt 的混合元启发式算法，通过分析发现该算法在大多数情况下能够提供更好的质量解决方案，尽管需要更多的执行时间。

    Feb, 2024

  • 不完整 MaxSAT 的近似策略

    本文提出了两种近似策略来改进不完全解决 MaxSAT 问题，并通过在 MaxSAT 评估 2017 中实验结果表明，这两种策略能够比最佳不完全求解器找到更好的解决方案。这两种策略分别是：通过聚类并用代表权重近似表示，以及将求解无法满足的子句权重之和最小化的问题分解成多个最小化子问题。

    Jun, 2018

  • 关于连续的基于本地 BDD 的混合 SAT 求解

    提出一种基于连续局部搜索与信念传播结合的算法 GradSAT，能在求解混合布尔约束问题方面有很好的应用表现，对称布尔约束和小系数伪布尔约束也可适用，并有望成为解决布尔满足性和优化问题的有效方法之一。

    Dec, 2020

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

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

    Mar, 2022