Nov, 2010

因果诱因语句：利用最大可满足性进行错误定位

PDF
TL;DR该研究提出了一种基于 MAX-SAT 的错误定位算法，通过符号执行，将程序的追踪记录编码为布尔可满足公式，构造出不可满足公式，并使用 MAX-SAT 找到可能的错误原因集合，其算法实现在名为 bug-assist 的工具中，并可以自动为普遍的错误类型建议修复。
发现论文，激发创造
  • 使用不可满足性解决最大可满足性问题

    本研究分析了现有的基于不可满足子公式识别的最大可满足性问题（MaxSAT）算法，并提出了几个关键性优化和新的替代算法，这些优化和新算法在实际应用中的 MaxSAT 实例上提供了显着的性能提升。

    Dec, 2007

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

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

    May, 2017

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

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

    Jun, 2023

  • UpMax：用戶分區的 MaxSAT

    本文提出了一种新的框架 UpMax，将分割过程与 MaxSAT 解决算法分离，使用户能够根据问题来提出分割方案，证明分割对于基于不可满足性的 MaxSAT 算法的性能有很大的影响。

    May, 2023

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

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

    Jan, 2024

  • MaxSAT 的渐增式基数约束

    本文介绍了一种新的方法，利用增量式计数约束来解决最大可满足性问题 (MaxSAT)。实验结果表明，与非增量式计数约束相比，该方法在性能上有显著的提高。

    Aug, 2014

  • 将 SAT 问题化简为 Max2XOR 问题

    本文提出了将 SAT 子句翻译成至多两个变量等于零或一的 XOR 子句的 Max2XOR 约束的装置，并提出了 Max2XOR 问题的新的解析规则，以提高求解效率。

    Apr, 2022

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

    FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

    Dec, 2019

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

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

    Dec, 2020

  • SATNet: 使用可微可满足性求解器桥接深度学习与逻辑推理

    本文提出了一种新的路线，即通过引入可微（平滑）的最大可满足性（MAXSAT）求解器，将逻辑推理纳入更大的深度学习系统的循环中，从而在端到端学习系统中学习有挑战性的问题的逻辑结构，表现出集成逻辑结构于深度学习的潜力。

    May, 2019