Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers
算法驱动的子句学习SAT求解器的性能关键取决于可变状态独立衰减和（VSIDS）分支启发式。尽管VSIDS在近15年前被提出，并且此后提出了许多其他用于SAT求解的分支算法，但VSIDS仍然是最有效的分支算法之一。在本文中，我们通过回答以下关键问题来推进我们对VSIDS的理解。我们提出的第一个问题是“VSIDS选择添加碰撞的变量类有什么特别之处？“在回答这个问题时，我们发现VSIDS绝大多数都选择、碰撞和学习桥变量，桥变量定义为连接SAT实例社区结构中不同社区的变量。这是令人惊讶的，因为VSIDS是在社区结构和SAT求解器性能之间的联系被发现之前十多年发明的。此外，我们表明，VSIDS被视为一个排名功能强烈相关的时间图中心的措施。把这两个发现放在一起，我们得出结论，VSIDS挑选高中心性的桥梁变量。我们提出的第二个问题是“乘法衰变在使VSIDS如此有效方面发挥了什么作用？“我们表明，乘法衰减的行为就像指数移动平均（EMA），有利于持续发生冲突的变量（信号），而不是间歇发生的变量（噪声）。我们提出的第三个问题是“VSIDS是否在时间和空间上集中。“我们表明，VSIDS不成比例地从少数社区中挑选变量，这与随机分支启发式不同。我们将这些发现放在一起，发明了一种新的自适应VSIDS分支启发式算法，该算法比SAT竞赛2013基准测试中最知名的VSIDS变体之一解决了更多的实例。
2015-09-14 cs.LO
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper)
我们结合约束字面量模型表示的关键概念，从一阶叠加和命题冲突驱动的子句学习（CDCL）创建新的演算非冗余子句学习（NRCL）决定Bernays-Schönfinkel片段。我们的演算使用一阶文字约束的元组之间的条件紧凑的模型表示。NRCL继承了叠加的抽象冗余准则和单调模型算子。CDCL增加了对诱导模型的原子排序的动态的、冲突驱动的搜索。因此，在NRCL中，可以有效地以当前模型候选为模来找到假子句。它指导推导一阶有序的预解式，从来没有多余的。类似于CDCL中的1UIP学习，学习的解决方案会导致回溯，并且通过传播阻止先前的冲突状态，它会强制寻找模型或反驳。非冗余的结果也意味着只有1000个子句可以由NRCL在Bernays-Schönfinkel片段上生成，这可以作为终止的论据。
2015-07-19 cs.LO
A Two-Watched Literal Scheme for First-Order Logic
Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）；Graduate School of Computer Science, Saarland Informatics Campus（萨尔兰州信息校园计算机科学研究生院）
本文提出了一种扩展到一阶逻辑的二维观察子句方案，用于高效检测可传播和虚假子句，同时证明了该方案的正确性和完备性，并展示了其在处理长子句时优于传统动态规划方法的性能。
2026-05-20 cs.LO
Extending CDCL to disjunctions of parity equations
University of Washington（华盛顿大学）
本文提出CDCL(⊕)算法，扩展到XNF公式，证明其与Res(⊕)的双向连接，并在XNF公式基准上优于现有求解器。
2026-05-14 cs.CC cs.LO
Towards Clause Learning à la Carte through VarMonads
越来越多的语言需要约束求解功能，例如错误检测或自动代码生成。想象一下，一种依赖类型的语言，只要给出它的类型，就可以立即实现一个程序。在SAT求解中，已经有几种技术来加速搜索过程，以满足可以用于程序合成的变量的分配。这些技术之一是子句学习，如果搜索分支遇到冲突，则分析冲突的原因并用于创建新子句，以便在冲突再次出现时使分支更早失败。我们提供了一个框架，这种技术可以来免费的布尔求解器，但任何约束求解器上运行的递归代数数据类型。我们通过跟踪变量赋值之前发生的读操作来实现这一点，并使用这些信息来创建冲突分析所需的依赖图。我们的结果在Agda中实现以获得最佳可读性，但它们也可以转移到其他函数式语言中。为了简洁起见，我们没有提供利用子句学习的整个搜索系统，但是从形式主义中可以清楚地看出，我们的技术确实能够构建子句学习搜索系统。
2022-08-22 cs.LO cs.PL
Extended Resolution Clause Learning via Dual Implication Points
University of California, San Diego（加州大学圣地亚哥分校）；Lorica Cybersecurity（洛里卡网络安全）；Georgia Institute of Technology（佐治亚理工学院）；Universitat Politècnica de Catalunya（加泰罗尼亚理工大学）
提出一种基于双蕴含点（DIP）动态引入新变量的扩展归结子句学习（ERCL）算法，并集成到CDCL求解器中，实验表明在Tseitin和XORified公式上优于多个领先求解器。
2026-05-22 cs.LO
SAT Solving Using XOR-OR-AND Normal Forms
本文提出逻辑公式的 XOR-OR-AND 范式（2-XNF），给出 CNF/ANF 到 2-XNF 的转换方法，并设计基于 DPLL 的求解器，在 ASCON-128 密码实例上优于现有方法。
2024-09-26 cs.LO math.AC math.LO
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
ITMO University（圣彼得堡国立信息技术、机械学与光学研究型大学）；Australian National University（澳大利亚国立大学）
介绍了基于新的冲突消解演算的无等式纯一阶逻辑第一定理证明器Scavenger。冲突解决有一个限制性的决议推理规则，类似于（一阶泛化）单位传播，以及一个规则，用于假设决策文字和规则派生新的条款（一阶泛化）冲突驱动的条款学习。
2017-10-31 cs.AI cs.FL cs.LO
Quantifier Elimination With Structural Learning
考虑了含有存在量词的命题CNF公式的量词消去问题。QE在形式化验证中起着关键作用。前面，我们提出了一种基于以下观察的方法。为了执行量化宽松，人们只需要添加一组依赖于自由变量的子句，这使得量化子句（即具有量化变量的子句）冗余。为了实现这种方法，我们引入了一个分支算法，使量化子句在子空间中冗余，并合并分支的结果。为了实现这个算法，我们开发了机器的D-序列。D-子句是一个记录，说明量化子句在指定的子空间中是冗余的。子句的冗余是一种结构属性（即，它只适用于逻辑上等价的公式的子集，而不是语义属性）。因此，在SAT问题中，重复使用D-序列并不像重复使用冲突子句那么容易。在本文中，我们解决这个问题。我们引入了一个新的定义的D-序列，使他们的可重用性。我们开发了一个理论，表明在什么条件下，D-射线可以安全地重复使用。
2018-10-15 cs.LO
Improving NLSAT for Nonlinear Real Arithmetic
针对 NLSAT 决策时忽略子句对算术变量影响的问题，本文引入子句级信息，提出可行集前瞻与算术传播分支启发式，并实现 clauseSMT，在 QF_NRA 可满足实例上优于 CVC5、Z3 和 YICES2。
2025-09-26 cs.LO cs.SC
On CDCL-based proof systems with the ordered decision strategy
我们证明了冲突驱动的子句学习SAT求解器与有序决策策略和决策学习计划是等价的有序决议。我们还证明了，通过替换这个学习计划与其相反，停止后的第一个新的条款回溯时，他们成为等同于一般决议。据我们所知，这是第一次从理论上研究特定决策策略和小句学习之间的相互作用。对于这两个结果，我们允许非确定性的求解器的能力，执行单位传播，冲突分析，并重新启动，在某种程度上，是类似于以前的作品在文献中。为了帮助介绍我们的结果，并可能在未来的研究，我们定义了一个模型和语言来讨论基于CDCL的证明系统，允许简洁和精确的定理语句。
2019-09-09 cs.CC cs.LO
Exploiting Isomorphic Subgraphs in SAT (Long version)
虽然静态对称破缺在SAT社区已经探索了几十年，但直到2010年，研究才集中在动态地利用相同的对称性，在SAT求解器运行期间，通过学习额外的子句。这两种方法是不同的，不兼容。前者修剪解决方案，而后者不修剪-它只修剪没有解决方案的搜索区域，如标准冲突条款。然而，这两种方法都需要我们称之为\emph{full symmetry}的东西，即文字之间的命题一致的映射$σ$，使得$σ(φ) \equiv φ$，其中$\equiv$表示句法等价模子句排序和子句内的文字排序。在这篇文章中，我们表明，这样的完全对称性是不是一个必要条件，增加额外的条款：同构之间的可能重叠的子图的着色关联图是充分的。虽然找到这样的子图是一个计算困难的问题，但在许多情况下，通过分析CNF所源自的问题的高级结构，可以检测到它们。我们证明了这一原则与几个著名的问题，包括范德瓦尔登数，有界模型检验和布尔毕达哥拉斯三元组。
2021-08-12 cs.LO
On the Effect of Learned Clauses on Stochastic Local Search
Ulm University（乌尔姆大学）
在成功的SAT求解器中有两种相互竞争的范式：随机驱动的子句学习（CDCL）和随机局部搜索（SLS）。CDCL系统地探索搜索空间，并具有学习新子句的能力。SLS检查当前完整分配的邻域。与CDCL不同，它缺乏从错误中学习的能力。这项工作围绕着SLS在原始公式中添加新条款是否有益的问题展开。我们的实验表明，条款与大量的正确文字w。R. t.一个固定的解决方案是有益的运行SLS。我们称这种条款为高质量条款。实验结果表明，CDCL学习的短句具有高质量的属性。我们研究了几个领域的随机生成的实例，并推导出最有益的策略，添加高质量的条款作为预处理步骤。在SLS求解器中实现的策略，它表明，这大大提高了国家的最先进的随机生成的实例。结果具有统计学意义。
2020-05-07 cs.AI cs.LO
Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
本文提出一种基于CDCL的反驳框架，用于确定量子k-SAT实例是否存在满足的产品态，通过几何近似和子句学习实现产品态不可满足性的证明。
2026-03-20 cs.CC cs.LO quant-ph
CDCL-inspired Word-level Learning for Bit-vector Constraint Solving
无量化位向量（QF_BV）理论在软件验证中具有重要意义。可满足性检查的标准方法将位向量问题简化为布尔问题，利用强大的SAT求解技术及其冲突驱动子句学习（CDCL）机制。然而，这种位级方法丢失了初始位向量问题的结构。我们提出了一个冲突驱动的，字级的，可组合的约束学习理论的量词免费位向量。这项工作铺平了道路，真正字级的决策程序的位向量，充分利用最近在CP和SMT社区设计的字级传播。
2017-06-28 cs.LO
Clause Vivification by Unit Propagation in CDCL SAT Solvers
Huazhong University of Science and Technology（华中科技大学）；University of Picardie Jules Verne（皮卡第儒勒·凡尔纳大学）；Artificial Intelligence Research Institute (IIIA), Spanish Scientific Research Council (CSIC)（西班牙高等科学研究委员会人工智能研究所（IIIA））
原始和学习的条款，在语句驱动的子句学习（CDCL）SAT求解器往往包含冗余的文字。这可能会对性能产生负面影响，因为冗余文字可能会降低布尔约束传播的有效性和后续学习子句的质量。为了克服这个缺点，我们提出了一个子句活化方法，通过应用单位传播消除冗余的文字。在SAT求解器触发一些选定的重新启动之前，激活所提出的子句活化，并且仅影响原始子句和学习子句的子集，根据文字块距离（LBD）等度量，这些子句被认为是更相关的。此外，我们进行了实证调查的实例来自最近的SAT比赛的硬组合和应用类别。结果表明，显着数量的额外的情况下，解决了所提出的方法被纳入五个最好的表现CDCL SAT求解器（葡萄糖，TC_葡萄糖，COMiniSatPS，MapleCOMSPS和MapleCOMSPS_LRB）。更重要的是，实证研究包括对小句活化的有效性的深入分析。值得一提的是，这里描述的SAT求解器之一在2017年SAT竞赛的主赛道中排名第一，这要归功于引入了拟议的子句vivification。该求解器在本文中得到了进一步的改进，并在2018年SAT竞赛的主赛道上获得铜牌。
2018-07-29 cs.AI cs.LO
On Enumerating Short Projected Models
针对命题模型枚举中避免重复的问题，提出两种采用对偶推理缩短模型长度的算法，分别基于对偶编码的阻塞子句和调整冲突驱动子句学习过程实现无阻塞子句枚举，并提供了正确性证明。
2024-11-12 cs.LO
Lifting CDCL to Template-based Abstract Domains for Program Verification
冲突驱动子句学习（CDCL）在布尔可满足性方面的成功启发了其他领域的采用。我们提出了一种新的提升CDCL的程序分析称为抽象冲突驱动的学习程序（ACDLP）。ACDLP在模型搜索和冲突分析之间交替，模型搜索使用约束传播执行过近似推理，冲突分析使用启发式选择执行欠近似溯因。我们将模型搜索和冲突分析算法实例化到模板多面体的抽象域，严格地将CDCL从布尔格推广到更丰富的格结构。我们的模板多面体可以表示程序变量上的区间、八边形和受限多面体约束。我们已经实现了ACDLP的自动边界安全验证的C程序。我们通过与CBMC（使用CDCL）和Astree（一种商业摘要解释工具）的比较来评估我们的分析器的性能。我们观察到两个数量级的决策，传播和冲突的数量减少，以及在运行时的1.5倍加速相比，CBMC。与Astree相比，ACDLP解决了两倍多的基准测试，并且具有更高的精度。这是CDCL的第一个实例化与模板多面体抽象域。
2017-07-07 cs.LO
Improving SAT Solvers via Blocked Clause Decomposition
Donghua University（东华大学）
最具竞争力的CDCL（基于条件驱动的子句学习）SAT求解器使用的决策变量选择策略是VSIDS（可变状态独立衰减和）或其变体，如指数版本EVSIDS。VSIDS及其变体的共同特点是在求解过程中利用了统计信息，而忽略了问题的结构信息。为此，本文对决策变量选择策略进行了改进，提出了一种基于BCD（Blocked Clause Decomposition）的SAT求解技术。其基本思想是一部分决策变量由VSIDS启发式算法选择，另一部分决策变量由BCD算法得到的分块集选择。与现有的基于BCD码的方法相比，该方法简单，不需要对CNF公式进行重新编码。经过认证的UNSAT轨道的SAT解算器也可以应用我们基于BCD的技术。我们的应用程序基准测试的实验表明，新的变量选择策略的基础上BCD可以提高SAT求解器，如abcdSAT的性能。带有BCD的求解器解决了SAT Race 2015中的一个实例，该实例迄今为止尚未被任何求解器解决。这表明在某些情况下，基于结构信息的启发式算法比基于统计信息的启发式算法更有效。
2016-04-02 cs.AI cs.LO
PICID: Proof-Driven Clause Learning in Neural Network Verification
The Hebrew University of Jerusalem（特拉维夫大学）；Amherst College（阿默斯特学院）；Stanford University（斯坦福大学）
PICID是一种生成标准Alethe格式证明的神经网络验证器，通过并行CDCL(T)架构结合先进SAT求解器和Marabou验证器，提升验证的可靠性和证明生成效率。
2026-09-22 cs.LG cs.LO
Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination
本文通过将TBUDDY库集成到CryptoMiniSat求解器中，使其在利用Gauss-Jordan消元法处理含大量奇偶约束的公式时能够生成兼容标准子句证明框架的不可满足性证明。
2023-04-09 cs.LO
Phase Selection Heuristics for Satisfiability Solvers
一般来说，基于冲突驱动DPLL的SAT Solver包括变量选择、相位选择、布尔约束传播、冲突分析、子句学习和数据库维护。优化这些组件的任何部分都可以提高求解器的性能。本文主要研究相位选择的优化问题。虽然ACE（组合先行评估的近似）权重被应用于诸如March的先行SAT求解器，但是到目前为止，没有冲突驱动的SAT求解器成功地应用ACE权重，因为计算ACE权重是耗时的。在这里，我们将ACE权重应用于冲突驱动的SAT求解器的部分相位选择。这可以看作是对Jeroslow-Wang（1990）提出的启发式的改进。我们将ACE启发式和现有的阶段选择算法在新的求解器MPhaseSAT，并选择一个阶段启发式的方式类似于投资组合方法。实验结果表明，加入ACE启发式可以提高冲突驱动求解器。特别是在应用程序实例上，具有ACE启发式的MPhaseSAT明显优于没有ACE启发式的MPhaseSAT，甚至可以解决一些至今仍无法解决的SAT实例。
2011-06-07 cs.DM cs.LO
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
School of Mathematical Sciences, Peking University（北京大学数学科学学院）；Peking University（北京大学）
提出了一种判定实数上多项式公式可满足性的新算法。该算法的关键是一个新的投影算子，称为样本单元投影算子，定制的搜索驱动子句学习（CDCL）风格的搜索。虽然新算子也是CAD（柱形代数分解）类投影算子，其计算包含给定样本的单元（不一定是圆柱的），使得来自问题的每个多项式在单元上是符号不变的，但是它具有单指数时间复杂度。样本细胞投影算子可以有效地引导CDCL风格的搜索远离冲突状态。实验证明了新算法的有效性。
2020-03-04 cs.AI cs.LO cs.SC
On Tackling the Limits of Resolution in SAT Solving
布尔可满足性（SAT）求解器的实际成功源于SAT求解的CDCL方法。然而，从命题证明复杂性的角度来看，CDCL并不比解决证明系统更强大，因为存在许多困难的例子。提出了一种新的问题变换，将合取范式（CNF）公式的判定问题转化为求解Horn公式的最大可满足性问题.给出了新的变换，证明了鸽洞公式MaxSAT分解步数的多项式界.这一结果是在明显的对比与早期的结果的长度证明的MaxSAT分辨率鸽子公式。本文还建立了相同的多项式约束的情况下，现代核心引导MaxSAT求解器。实验结果表明，CNF公式已知是很难CDCL SAT求解器，这些可以有效地解决与现代MaxSAT求解器。
2017-07-05 cs.LO
Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning
研究大语言模型约束推理，在接近匹配子句密度时测试实例级转移，比较不同公式和锚点，发现求解器与模型硬度差异，以及模型对证明保留重新标记敏感，还研究了完成令牌花费与代理的关系。
2026-07-21 cs.AI cs.LG cs.LO
