AAAIDec, 2019

FourierSAT: 一个基于傅里叶展开的代数框架求解混合布尔约束问题

PDF
TL;DRFourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。
boolean satisfiability problemcdcllocal search sat solversnon-cnf constraintsfouriersat
发现论文，激发创造
  • 基于 GPU 的混合 SAT 求解的大规模并行连续局部搜索

    提出了基于梯度驱动连续局部搜索（CLS）的高度并行混合 SAT 求解器 FastFourierSAT，该算法利用图形处理单元（GPU）的并行性能加速计算，可以比之前的方法快 100 + 倍，并在更大规模的案例上表现出良好的性能。

    Aug, 2023

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

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

    May, 2017

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

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

    Dec, 2020

  • G2SAT：学习生成 SAT 公式

    本研究提出了 G2SAT 这一深度生成式框架，可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式，旨在扩展现有的数据集，为 SAT 求解器的性能提供优化方案。

    Oct, 2019

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

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

    Dec, 2007

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

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

    Sep, 2023

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

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

    Jan, 2024

  • 利用因果推理解释 SAT 求解

    本文介绍了使用因果推理探究 SAT 求解器内在工作机制的方法 CausalSAT，并通过实验验证了其中四条经验法则和三个与现代 SAT 求解器实现密切相关的问题。

    Jun, 2023

  • SATformer: 应用于 SAT 求解的 Transformer

    本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构以捕捉这些子句之间的关系，并注重没能同时出现在 UNSAT 核心中的子句的权重，实验结果表明，SATformer 能够优于现有的基于学习的 SAT 求解器。

    Sep, 2022

  • 结合 $k$-CNF 和 XOR 相变

    本文首次研究了随机 $k$-CNF-XOR 公式的可满足性，并证明了 $k$-CNF-XOR 公式以及 $k = 2$ 时的相变存在性，发现了服从 $k$-CNF 和 XOR 约束之间线性权衡的惊人相变现象，并且提供了 SAT 求解器在此相变中的性能实证结果。

    Feb, 2017