An Experimental Study of Permanently Stored Learned Clauses
Simon Fraser University（西蒙菲莎大学）
现代CDCL SAT求解器能够快速学习子句，一个重要的启发式算法是子句删除方案。大多数当前的求解器都有两个（或更多）子句存储。一个是永远不会删除的“有价值”条款。大多数学习子句被添加到另一个子句中，并使用积极的删除策略来限制其大小。MapleSAT家族中的最新求解器具有相对复杂的删除方案，并且表现良好。许多求解器只永久存储二进制子句，但MapleLCMDistChronoBT永久存储具有小LBD的子句。我们报告了MapleLCMDistChronoBT中永久子句存储的实验研究。我们观察到，这个商店可以得到相当大，但几种方法限制其大小降低性能。我们还表明，备用大小和LBD为基础的标准提高性能，同时仍然有大型永久商店。特别是，将子句的大小保存到8，并添加少量的高中心性子句，这两种方法都提高了性能，使用这两种方法都有最好的改进。
2021-10-27 cs.AI cs.LO
Reset Early, Reset Often, Eliminate Models
University of Cambridge（剑桥大学）
该研究提出SATResetCoP证明器，通过不回溯无成效表、启动新表生成接地子句的方式改进，在TPTP和MPTP2078基准上较leanCoP、SATCoP风格基准取得显著性能提升。
2026-10-14 cs.AI cs.LO
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
Vienna University of Technology（维也纳工业大学）；University of California at Berkeley（加州大学伯克利分校）
我们提供了一个新的理解，一些方面的实际SAT求解器是基于DPLL与单位子句传播，子句学习，并重新启动。我们这样做是通过分析一个具体的算法，我们声称是忠实于实际的求解器做什么。特别是，在做出任何新的决定或重新开始之前，求解器重复应用单位分辨率规则，直到饱和，并且除了一些内部随机性之外，不留下任何组件受非确定性的支配。我们证明了一个可能令人惊讶的事实，即尽管求解器不是为它明确设计的，但在不超过O（n^2k+2）次冲突和重新启动后，它很有可能最终表现为宽度k分辨率，其中n是变量的数量。换句话说，宽度k分辨可以被认为是O（n^2k+2）的单位分辨规则的重新开始。
2014-01-16 cs.AI cs.LO
Local Redundancy in SAT: Generalizations of Blocked Clauses
本文研究SAT公式的子句消去冗余性质，提出语义阻塞概念，证明其为最一般的局部冗余性质，并引入集合阻塞与超级阻塞，通过复杂度分析将其与文献中已知性质关联。
2018-10-23 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
Characterization of Glue Variables in CDCL SAT Solving
University of Alberta（阿尔伯塔大学）
一种评估给定学习子句重要性的最新标准称为文字块距离（LBD）得分。它测量给定学习子句中不同决策级别的数量。习得小句的LBD分数越低，其质量越好。已知LBD得分为2的学习子句（称为胶合子句）具有高修剪能力，其从未从现代CDCL SAT求解器的子句数据库中删除。在这项工作中，我们涉及胶水条款的决策变量。我们将至少出现在一个glue子句中的变量称为Glue Variables。我们首先通过在SAT Competition-2017和2018的基准测试上运行最先进的CDCL SAT求解器MapleLCMDist，实验表明，使用胶水变量的分支决策比非胶水变量更有推理和冲突效率。基于这一观察，我们开发了一个结构感知的CDCL变量碰撞计划，碰撞活动得分的胶水变量的基础上，它的外观计数胶水子句，学习到目前为止的搜索。实证评估表明，新方法在2017年和2018年SAT竞赛的主赛道实例上是有效的。
2019-04-25 cs.AI
Revisiting the Learned Clauses Database Reduction Strategies
CRIL - CNRS（CRIL - 法国国家科学研究中心）；Université d’Artois（阿图瓦大学）
在本文中，我们重新审视一个重要的问题，基于CDCL的SAT求解器，即学习子句数据库管理策略。我们的动机是从一个简单的观察随机和大小有界的减少策略的显着表现的来源。我们首先推导出一个简单的约简策略，称为大小有界随机策略（简称SBR），它结合了maintaing短子句（大小由k限制），同时删除大小大于k的随机子句。由此产生的战略优于国家的最先进的，即基于LBD的一个，从最后的SAT竞争的SAT实例。加强保持短条款的兴趣，我们提出了几个新的动态变量，我们讨论了它们的性能。
2014-02-09 cs.AI
Fast Blocked Clause Decomposition with High Quality
任何CNF公式都可以分解为两个阻塞子集，使得两者都可以通过BCE（阻塞子句消除）求解。为了使分解更有用，人们希望分解尽可能不平衡。实现这一目标往往需要时间。到目前为止，已经有几个分解和后处理算法，如PureDecompose，QuickDecompose，MixerMover等，我们发现，这些现有的算法往往是低效或低质量的分解。本文旨在提高分解质量，同时保持算法的运行时间控制。为了实现这一目标，我们改进了现有的BCE，并提出了两个新的变种PureDecompose，一个新的启发式分解称为LessInterfereDecompose，和一个新的后处理算法称为RsetGuidedDecompose。将这些新技术结合在一起，产生了一种名为MixDecompose的新算法。在我们的实验中，不存在PureDecompose+ MixDecompose的质量优于MixDecompose的应用程序公式。在速度方面，MixDecompose也非常快。我们的平均运行时间有点长，但最坏情况下的运行时间更短。理论上，我们的两个PureDecompose变体需要子句数量的线性时间。通过限制BCE使用的触摸列表的大小，我们可以保证MixDecompose总是在线性时间内运行。
2015-12-19 cs.LO
Too much information: why CDCL solvers need to forget learned clauses
Universität Ulm（乌尔姆大学）
摘要驱动小句学习是解决命题逻辑可满足性问题的一个非常成功的范例。与简单的深度优先回溯方法不同，这种求解器以附加子句的形式学习发生冲突背后的原因。然而，尽管CDCL解算器取得了巨大的成功，但人们对什么以何种方式影响这些解算器的性能仍然只有有限的了解。考虑到不同的措施，本文证明，相当令人惊讶的是，子句学习（无法摆脱一些子句）不仅可以帮助求解器，但往往可以显着恶化的解决方案的过程。通过大量的实证分析，我们进一步发现CDCL求解器的运行时间分布是多峰的。这种多模态可以被看作是上述恶化现象的原因。同时，它也给出了一个指示，为什么小句学习结合小句删除几乎是事实标准的SAT解决，尽管这一现象。作为最后的贡献，我们表明，威布尔混合分布可以准确地描述多峰分布。因此，向基实例添加新子句具有使运行时长尾化的固有效果。这种见解提供了一个解释，为什么遗忘子句的技术是有用的CDCL求解器除了优化单位传播速度。
2022-06-16 cs.AI
A Deep Dive into Conflict Generating Decisions
Department of Computing Science, University of Alberta（阿尔伯塔大学计算机科学系）
布尔可满足性（SAT）是一个著名的NP完全问题。尽管这种理论上的困难，SAT求解器基于冲突驱动子句学习（CDCL）可以解决大型SAT实例从许多重要的领域。CDCL从冲突中学习子句，这是一种允许求解器修剪其搜索空间的技术。CDCL中的选择算法优先考虑最近冲突中涉及的变量。虽然只有一小部分决策会产生冲突，但许多决策会产生多个冲突。在本文中，我们详细研究了CDCL中的冲突生成决策。我们调查的影响，单冲突（SC）的决定，只产生一个冲突，和多冲突（MC）的决定，产生两个或更多。我们经验性地描述了这两种类型的决定的基础上，每种类型的决定所产生的学习条款的质量。我们还显示了一个重要的连接在同一MC决策，其中一个学习的子句触发下一个形成一个链的子句的学习连续的子句之间的学习。这导致考虑冲突之间的相似性，为此，我们制定了conflictsproximity的概念作为一个相似性度量。我们发现，在mc决策的冲突更密切相关的连续冲突产生的SC决定。最后，我们开发了共同原因变量减少（CRVR）作为一种新的决策策略，减少了一些变量的选择优先级从学习条款的MC决策。我们在三个领先的求解器中实施的CRVR的实证评估显示了SAT竞赛-2020主赛道基准测试的性能提升。
2021-05-10 cs.AI
Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship
Clermont Auvergne University（克莱蒙奥弗涅大学）；CNRS（法国国家科学研究中心）
子句学习是冲突驱动子句学习（CDCL）SAT求解器的重要组成部分之一，在工业实例中非常有效。由于在最坏的情况下，学习子句的数量被证明是指数的，所以有必要识别最相关的子句来保持和删除不相关的子句。据文献报道，已经提出了几种学习子句删除策略。然而，在每个缩减步骤中要删除的子句的数量以及使用每个策略获得的结果的多样性造成了确定哪个标准更好的混乱。因此，在搜索步骤期间选择要移除哪些学习子句的问题仍然非常具有挑战性。在本文中，我们提出了一种新的方法来确定最相关的学习条款，而不赞成或排除任何建议的措施，但通过采用这些措施之间的优势关系的概念。我们的方法绕过了结果多样性的问题，并在对这些措施的评估之间达成了妥协。此外，所提出的方法还避免了另一个非平凡的问题，这是在学习子句数据库的每次减少要删除的子句的量。
2017-05-31 cs.AI
Community-based 3-SAT Formulas with a Predefined Solution
Anhui Province Key Laboratory of Software Engineering in Computing and Communication（安徽省计算与通信软件工程重点实验室）；School of Computer Science and Technology（计算机科学与技术学院）；University of Science and Technology of China, China（中国科学技术大学，中国）
对于SAT求解器的测试和开发来说，使用预定义的解决方案生成精心制作的SAT公式是至关重要的，因为现实世界中的许多SAT公式都有解决方案。虽然已经提出了一些生成算法来生成具有预定义解的SAT公式，但是没有考虑SAT公式的社区结构。我们提出了一个3-SAT公式生成算法，不仅保证存在一个预定义的解决方案，但也同时考虑社区结构和子句分布。所提出的3-SAT公式生成算法通过控制（1）其变量具有共同社区的子句的数量（我们称之为社区内子句）和（2）仅属于一个社区的变量的数量（我们称之为社区内变量）来控制社区结构的质量。为了研究社区结构和子句分布对SAT公式硬度的综合影响，我们测量了两个求解器，gluHack（领先的CDCL求解器）和CPSparrow（领先的SLS求解器），在不同的参数设置组下生成的SAT公式的求解运行时间。通过大量的实验，我们得到了一些值得注意的结果：（1）对于CPSparrow，社团结构对SAT公式的硬度影响很小，但对于gluHack，社团结构对SAT公式的硬度影响很大。(2)只有当SAT公式中的真文字在预定义解方面的比例为0.5时，SAT公式对于gluHack是难以求解的;当该比例低于0.5时，SAT公式对于CPSparrow是难以求解的。(3)当子句数与变量数之比约为4.25时，SAT公式对于gluHack和CPSparrow都难以求解。
2019-02-26 cs.AI
Lower bounds for set-blocked clauses proofs
本文研究 BC${}^-$、RAT${}^-$、SBC${}^-$、GER${}^-$ 等无新变量扩展归结系统，通过鸽巢原理二进制编码的指数下界证明 SBC${}^-$ 严格弱于 ER，并确立其与 RAT${}^-$、GER${}^-$ 的指数分离。
2024-01-20 cs.CC cs.LO
Explaining SAT Solving Using Causal Reasoning
National University of Singapore（新加坡国立大学）；Chennai Mathematical Institute（金奈数学研究所）；IAI, TCG-CREST（TCG-CREST 人工智能研究所）
针对CDCL算法缺乏理论解释、部分场景求解能力存疑的问题，提出CausalSAT方法，通过因果推理构建求解器组件因果图，验证经验法则并解答求解器实现相关问题。
2023-06-09 cs.AI
Generating Difficult SAT Instances by Preventing Triangles
INSIGHT Centre for Data Analytics University College Cork（科克大学INSIGHT数据分析中心（University College Cork）科克大学是爱尔兰的一所公立研究型大学，INSIGHT Centre for Data Analytics是其下属的数据分析研究中心，这里按要求提取到大学/学院级别，所以保留原机构名称。需要注意的是，“University College Cork”作为大学名称，整体是机构的一部分，所以正确的机构提取应该是包含大学名称的完整机构，即“INSIGHT Centre for Data Analytics University College Cork”，其中文翻译应保持机构名称的完整性，“科克大学INSIGHT数据分析中心”。但根据要求，机构粒度到大学/学院/公司/研究院级别即可，所以这里“University College Cork”（科克大学）本身也是一个机构，不过原文本中明确的机构是“INSIGHT Centre for Data Analytics University College Cork”，所以需要完整提取。不过仔细看，原文本中的“Affiliation:”后面跟着的是“INSIGHT Centre for Data Analytics University College Cork Cork, Ireland”，其中“INSIGHT Centre for Data Analytics”是一个中心，“University College Cork”是大学，所以完整的机构应该是“INSIGHT Centre for Data Analytics University College Cork”，即科克大学INSIGHT数据分析中心。所以正确的输出应该是：{）
在为SAT求解器创建基准测试时，我们需要容易构建但难以求解的SAT实例。在寻找这种方法的最新发展导致了平衡SAT算法，它可以创建具有m个高难度子句的k-SAT实例，对于任意k和m。本文介绍了一种基于聚类系数图统计的可满足性实例生成器--非三角形可满足性算法。我们经验比较两个算法固定的arity和变量的数量，但不同的条款的数量。我们发现的最困难的例子是由非三角形SAT产生的。此外，来自非三角形SAT的困难实例具有与来自平衡SAT的困难实例不同的子句数量，潜在地允许两种方法的组合来为更大的参数阵列找到硬SAT实例。
2019-03-08 cs.AI
Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
针对电路SAT求解中结构信息丢失的问题，提出CASCAD框架，利用图神经网络计算的条件概率引导CDCL的相位选择与子句管理，在LEC基准上实现高达10倍加速及额外23.5%运行时间减少。
2025-08-06 cs.AI
Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
针对浮点SMT求解中梯度支配导致的局部最优问题，提出GradSAT框架，将每个子句视为多任务学习任务，通过动态梯度归一化平衡梯度，结合GPU加速连续松弛与位精确局部搜索，实现稳健高效的求解。
2026-10-08 cs.AI cs.LG
Subsumption-driven clause learning with DPLL+restarts
LIB；Université de Bourgogne（勃艮第大学）
我们建议使用DPLL+重新启动解决SAT实例的基础上生产的条款，subcruise初始条款的连续简化。我们表明，这种方法可以反驳卵石公式在多项式时间和线性空间，有效地与CDCL求解器。
2019-06-18 cs.AI cs.LO
Variable and clause elimination for LTL satisfiability checking
研究了LTL公式子句范式的预处理技术。应用标记子句的机制，使我们能够重新解释LTL可满足性作为一组纯粹的命题问题，从而转移简化思想从SAT到LTL。我们证明了这一点，适应变量和子句消除，现代SAT求解器使用的一个非常有效的预处理技术。我们的实验证实，即使在时间设置的公式大小和随后的求解器运行时间的减少，可以实现大幅减少。
2013-09-30 cs.LO
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
我们给我们的新的并行SAT求解器Gimsatul的第一个帐户。它的关键特性是在内存中物理共享子句，而不是复制子句，这是其他最先进的多线程SAT求解器在逻辑上交换子句的方法。我们的方法保留了有关哪些文字在一个解决线程的本地子句中被关注的信息，但在所有解决线程之间全局共享子句的实际不可变文字。这种设计提供了相当显着的并行可扩展性，允许积极的条款共享，同时保持较低的内存使用率，并生成更紧凑的证明。
2022-07-29 cs.LO
Improving abcdSAT by At-Least-One Recently Used Clause Management Strategy
Donghua University（东华大学）
我们进一步改进了abcdSAT的2015年版本，通过各种算法，如至少一个最近使用的策略，学习子句数据库近似约简等。基于2016年SAT竞赛中不同赛道的需求，我们开发了三个版本的abcdSAT：drup，inc和lim，分别参加主（敏捷），增量库和无限制赛道的比赛。
2016-05-05 cs.AI cs.LO
Rethinking Clause Management for CDCL SAT Solvers
The Chinese University of Hong Kong（香港中文大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；National Center of Technology Innovation for EDA（EDA技术国家工程研究中心）
本文提出了一种新的子句减少机制，以改进CDCL SAT求解器在复杂算术电路验证中的性能，通过分离处理子句的内在血统和动态使用模式，实现效率提升。
2026-02-25 cs.LO
SATformer: Transformer-Based UNSAT Core Learning
The Chinese University of Hong Kong（香港中文大学）
本研究提出基于Transformer的SATformer方法，通过建模子句交互识别不可满足子问题，结合多任务学习训练，性能显著优于NeuroSAT，还能将现有SAT求解器运行时间平均缩短21.33%。
2024-03-12 cs.AI cs.LG cs.LO
Exponential separations using guarded extension variables
该研究聚焦无新变量的四类归结增强证明系统，通过构造分离公式、证明鸽巢原理的多项式规模SBC⁻证明等方式，厘清了它们之间近乎完整的相对强度关系。
2023-04-30 cs.CC cs.LO
Learned Clause Minimization in Parallel SAT Solvers
学习子句最小化（LCM）可以提高现代SAT求解器的性能，特别是在解决困难SAT实例。尽管LCM方法在顺序求解器中取得了成功，但它们并没有广泛地应用于并行SAT求解器中。在本文中，我们探讨了潜在的LCM并行SAT求解器定义多个LCM方法的基础上，子句vivification，比较它们在不同的SAT求解器的运行时间，并讨论性能的收益和损失的原因。结果表明，LCM只提高性能的并行SAT求解器的SAT实例的一小部分。更常见的是，应用LCM会降低性能。只有某些LCM方法能够提高并行SAT求解器的整体性能。
2019-08-05 cs.DS cs.LO
Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)
逻辑密码分析、电路验证和有界模型检验的验证通常可以简洁地表示为组合可满足性（SAT）问题，其中实例是传统子句和奇偶约束的组合。本文研究了如何通过在DPLL（XOR）框架中使用XOR推理模块来增强现代SAT求解器，从而有效地解决此类组合问题。提出了一种新的异或推理模块，它使用增量高斯-约当消去法推导出所有可能的隐含文字。一种分解技术，可以大大减少奇偶约束矩阵的大小，同时允许仍然推导出所有隐含的文字。它示出了如何消除变量只发生在奇偶约束，同时保持分解。所提出的技术进行了实验评估。
2012-09-08 cs.LO
An early sign of satisfiability
本文考虑命题子句集（SAT实例）的可满足性检查。结果表明，在求解SAT问题的过程中，子句的“单极集”（不包含肯定子句或否定子句）在所有子句满足之前提供了SAT实例可满足性的“早期信号”.在这个符号处，处理可以通过“单极集合终止”来终止，因此在它通常由SAT求解器完成之前UST（表1）。对SAT竞赛中使用的基准SAT实例的分析表明，UST可以加快解决源于许多现实问题的SAT实例。UST的效率随着被检查的SAT集合的“偏度”而增加，该偏度是集合中否定和非否定文字的概率之间的差异。许多现实世界的问题，由于它们的语义，是扭曲的（表2）。UST的效率可以通过揭示SAT集合的“隐藏偏度”来提高（表3）。
2016-12-15 cs.LO
Efficient Neural Clause-Selection Reinforcement
Czech Technical University in Prague（捷克技术大学布拉格分校）
本文提出一种高效神经网络子句选择评分架构，将其集成到 Vampire 证明器中通过强化学习训练，在 TPTP 基准上比基线策略多解决 20% 的未见问题。
2025-05-30 cs.AI cs.LO
Improved SAT models for NFA learning
LERIA（昂热大学信息学、机器人学与人工智能实验室）；University of Angers（昂热大学）
语法推理是研究从单词中学习自动机和语法的算法。我们专注于从单词样本中学习大小为k的非确定性有限自动机。为此，我们制定了一个SAT模型的问题。生成的SAT实例是巨大的，我们提出了一些模型的改进，无论是在变量的数量，条款的数量，条款的大小。这些改进显著减少了实例，但代价是生成时间更长。因此，我们试图平衡实例大小与生成和求解时间。我们还实现了一些实验比较，我们分析了我们的各种模型的改进。
2021-07-13 cs.AI cs.LO
A Non-CDCL SAT Solver with Early Conflict Detection: The Watched-Literal-Based CSFLOC Solver
Eszterh\'azy K\'aroly Catholic University Eger, Hungary
该研究提出基于监视文字的非-CDCL SAT求解器CSFLOC-WL3，通过早期冲突检测替换原CSFLOC的瓶颈搜索，实验显示其在近阈值随机3-SAT实例上优于对比求解器。
2026-08-26 cs.LO
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
本文提出加速驱动子句学习（ADCL）演算，利用循环加速避免递归 CHCs 在归结证明中的重复推导，从而缩短证明，并在 LoAT 中实现后与现有工具实证比较。
2023-07-14 cs.LO
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
Comon和Cortier使用一阶子句的新类$\mathcal C$定义并建模了具有单盲复制的密码协议。他们在3-DEXPTIME中证明了它的可满足性问题。我们改进了这一结果表明，满足这个类是NEXPTIME完全的，使用新的分辨率技术。我们证明了满足是DEXPTIME完整的，如果条款是霍恩，这是所需的建模加密协议。虽然翻译霍恩条款只给出了一个DEXPTIME上界的保密问题，这些协议，我们进一步表明，这个保密问题实际上是DEXPTIME完全的。
2005-11-03 cs.CR cs.LO
Generating clause sequences of a CNF formula
给定具有子句$C_1,\ldots,C_m$和变量$V=\{x_1,\ldots,x_n\}$的CNF公式$Φ$，$Φ$的真值赋值$a:V\rightarrow\{0,1\}$导致子句序列$σ_Φ(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m$，其中$C_i(a) = 1$ if子句$C_i$在赋值$a$下求值为$1$，否则为$C_i(a) = 0$。所有可能的子句序列的集合携带关于公式的大量信息，例如SAT、MAX-SAT和MIN-SAT可以根据找到具有极值属性的子句序列来编码。我们考虑在Dagstuhl研讨会19211“数据管理中的枚举”（2019）上提出的一个问题，关于生成给定的具有有界维数的CNF的所有可能的子句序列。我们证明了问题可以在增量多项式时间内解决。我们进一步给出了这类易处理CNF公式的多项式延迟算法。我们还考虑了最大子句序列和最小子句序列的生成问题，证明了最大子句序列的生成是NP-困难的，而最小子句序列的生成具有多项式延迟。
2020-02-17 cs.DM 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
Solving non-linear Horn clauses using a linear Horn clause solver
在本文中，我们表明，检查可满足性的一组非线性霍恩条款（也称为非线性霍恩条款计划）可以实现使用求解器的线性霍恩条款。我们实现这一点，通过交错的程序转换与线性霍恩条款（也称为线性霍恩条款求解器）的可满足性检查。程序转换是基于树维度的概念，我们将其应用于一组非线性子句，产生一组其派生树具有有界维度的集合。这样一套条款可以线性化。然后，主要的算法进行应用线性化变换和求解器的线性霍恩条款的一系列条款的连续增加的维度范围。然后，通过使用较低维度的条款解决方案来（部分）线性化较高维度的条款，进一步发展了该方法。我们构建了一个原型实现这种方法，并进行了一些实验上的一组验证问题，这表明了一些承诺。
2016-07-15 cs.LO cs.PL
Some notes on model rotation
模型旋转是一种有效的改进MUS发现算法的技术。在以前的工作中，我们已经研究了模型旋转作为一种算法，遍历一个图，这是由输入公式引起的。本文引入了阻塞边的概念，阻塞边是图中永远不能被遍历的边。我们证明了无冗余CNF公式的存在性，其中一些条款是无法达到的模型旋转。此外，我们证明了Belov，Lynce和Marques-Silva的一个猜想。
2014-01-29 cs.LO
Conflict-Driven XOR-Clause Learning (extended version)
现代冲突驱动子句学习（CDCL）SAT求解器在求解合取范式（CNF）公式方面非常出色。然而，一些应用问题涉及大量的奇偶校验（XOR）约束，如果转换为CNF，不一定有效地处理。本文研究了在DPLL（XOR）框架下求解含XOR子句的CNF公式，其中CDCL SAT求解器与单独的XOR推理模块相耦合。新技术的开发，用于分析XOR推理推导，允许一个获得较小的CNF子句的XOR隐含文字的解释，也派生和学习新的XOR子句。它被证明，这些新技术允许非常短的不可满足性证明的一些公式，其CNF翻译没有多项式大小的分辨率证明，即使是一个非常简单的异或推理模块，只能单位传播。一组具有挑战性的逻辑密码分析实例的效率进行评估所提出的技术。
2014-07-24 cs.LO
Exploiting Isomorphic Subgraphs in SAT (Long version)
虽然静态对称破缺在SAT社区已经探索了几十年，但直到2010年，研究才集中在动态地利用相同的对称性，在SAT求解器运行期间，通过学习额外的子句。这两种方法是不同的，不兼容。前者修剪解决方案，而后者不修剪-它只修剪没有解决方案的搜索区域，如标准冲突条款。然而，这两种方法都需要我们称之为\emph{full symmetry}的东西，即文字之间的命题一致的映射$σ$，使得$σ(φ) \equiv φ$，其中$\equiv$表示句法等价模子句排序和子句内的文字排序。在这篇文章中，我们表明，这样的完全对称性是不是一个必要条件，增加额外的条款：同构之间的可能重叠的子图的着色关联图是充分的。虽然找到这样的子图是一个计算困难的问题，但在许多情况下，通过分析CNF所源自的问题的高级结构，可以检测到它们。我们证明了这一原则与几个著名的问题，包括范德瓦尔登数，有界模型检验和布尔毕达哥拉斯三元组。
2021-08-12 cs.LO
Complete Trigger Selection in Satisfiability modulo first-order Theories
本文证明在SMT求解器中，当触发器函数与文字选择函数一致时，量词实例化对饱和子句集是完备的，并给出停机条件及Horn或2SAT情形的多项式时间求解。
2023-06-21 cs.LO
Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach
我们解决的问题，检查约束角子句（CHC）定义的代数数据类型（ADT），如列表和树的可满足性。我们提出了一种新的技术，用于将定义在ADT上的CHC转换为CHC，其中谓词的参数只有基本类型，如整数和布尔值。因此，我们的技术避免，在可满足性检查，明确使用的证明规则的基础上归纳的ADT。对以前的ADT去除技术的主要扩展是一个新的转换规则，称为差分替换，它允许我们引入辅助谓词，其定义对应于在进行归纳证明时使用的引理。我们提出了一个算法，执行自动删除ADT应用新的规则，连同传统的折叠/展开规则。我们证明了，在适当的假设下，转换条款的集合是可满足的当且仅当这样是原来的条款的集合。通过实验评估，我们表明，使用新的规则显着提高ADT删除的有效性。我们还表明，我们的方法是有竞争力的工具，使用归纳规则扩展CHC求解器。
2021-11-23 cs.LO cs.PL
Phase transition for Local Search on planted SAT
局部搜索算法（或爬山法，或迭代改进法）是解决可满足性和最大可满足性问题的最简单的算法之一。它是许多可满足性和最大可满足性求解器的一部分，用于为更复杂的算法找到一个好的起点，并改进候选解。本文分析了随机种植3-CNF公式的局部搜索问题。我们证明了如果k<7/6使得子句与变量的比率小于kln（n）（n是CNF中变量的数量），那么局部搜索whp找不到满意的分配，如果k>7/6使得子句与变量的比率大于kln（n）$，那么局部搜索whp找到满意的分配.作为一个副产品，我们还表明，对于任何常数r有g，使本地搜索应用到一个随机的（不一定种植）3-CNF与条款变量比r产生的分配，满足至少gn条款小于最大数量的可满足的条款。
2008-11-16 cs.DS cs.LO
A Fixed-Parameter Algorithm for #SAT with Parameter Incidence Treewidth
我们提出了一种有效的固定参数算法，用于#SAT，由关联树宽度参数化，即，二分图的树宽，其顶点是给定CNF公式的变量和子句;当且仅当变量出现在子句中时，变量和子句通过边连接。我们的算法运行时间为O（4^kklN），其中k表示关联树宽度，l表示最大子句的大小，N表示树分解的节点数。
2007-02-21 cs.CC cs.DS cs.LO
Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
University of Trento（特伦托大学）；University of Freiburg（弗赖堡大学）
本文提出两种新型求解器，结合CDCL与时间顺序回溯，实现高效且不相交的枚举。通过改进的implicant shrinking算法减少部分赋值数量，提升搜索效率，并在投影枚举和SMT推理中表现优异。
2024-11-21 cs.LO
Extending E Prover with Similarity Based Clause Selection Strategies
E prover是一个最先进的一阶逻辑等式定理证明器。E证明器是围绕饱和循环构建的，其中新的子句由来自先前导出的子句的推理规则导出。推理的子句选择提供了非确定性的主要来源和循环的重要选择点，其中正确的选择可以显着影响证明搜索。在这项工作中，我们扩展E证明与几个新的子句选择策略的基础上的相似性的一个子句的猜想。特别地，优选与猜想更相关的子句。我们实施不同的策略，以不同的方式定义与猜想的关系。我们提供了一个实施建议的选择策略，我们评估他们的效率在一个广泛的基准集。
2016-06-13 cs.LO
Core First Unit Propagation
自CDCL求解器开发以来，单位传播（也称为布尔约束传播）一直是每个现代CDCL SAT求解器的重要组成部分。一般来说，单元传播是通过在线性观察列表上顺序扫描每个子句来实现的。本文提出了一种新的单元传播技术，称为核心优先单元传播。其主要思想是在单元传播过程中优先选择核心子句而不是非核心子句，试图生成更短的学习子句。这里，核心子句被定义为文字块距离小于或等于7的子句。实证结果表明，核心第一单元传播提高了2018年SAT竞赛的获胜者MapleLCMDistChronoBT的性能。
2019-07-02 cs.LO
Solving Horn Clauses on Inductive Data Types Without Induction
基于归纳定义的数据结构，如列表和树，我们解决了约束Horn子句（CHC）的可满足性验证问题。我们提出了一种转换技术，其目标是删除这些数据结构的CHCs，从而减少其满足性的整数和布尔CHCs的可满足性问题。我们提出了一个转换算法，并确定了一类条款，它总是成功的。我们还考虑了该算法的扩展，它结合了子句转换与整数约束推理。通过实验评估，我们表明，我们的技术大大提高了Z3求解器的有效性，CHCs。我们还表明，我们的验证技术的基础上CHC转换，然后CHC解决方案，是有竞争力的CHC求解器与归纳扩展。本文件正在考虑被TPLP接受。
2018-04-24 cs.LO cs.PL
Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
本文定义了（一阶）冲突解决演算：现代SAT求解器中使用的技术启发的决议演算的扩展。决议推理被限制为（一阶）单位传播和演算扩展的机制，假设决策文字和一个新的推理规则的子句学习，这是一个一阶推广的命题冲突驱动的子句学习（CDCL）过程。微积分是可靠的（因为它可以被自然演绎模拟）和反驳完备的（因为它可以模拟归结），这些事实在这里得到了详细的证明。
2016-02-15 cs.LO
Life span of SAT techniques
该研究针对SAT求解器CaDiCaL的4项特性，在2009-2022年SAT竞赛基准上通过逐一激活/禁用的方式测试，最终未能证实“禁用特性总有害、技术生命周期有限、特性相互模拟”三个假设。
2024-02-02 cs.LO
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
Multiple Query Satisfiability of Constrained Horn Clauses
本文针对含多个查询的约束 Horn 子句可满足性问题，提出一种查询信息融合的变换技术，使新查询携带其他查询的相关信息，从而提升 CHC 求解算法对查询间关系的利用能力，并在列表和树等代数数据类型程序验证基准上验证了其有效性。
2024-01-11 cs.LO cs.PL cs.SE
Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
众所周知，命令式、函数式和逻辑程序的验证可以归结为约束Horn子句（CHC）的可满足性，并且这种可满足性检查可以通过使用CHC求解器（诸如Eldarica和Z3）来执行。这些求解器在处理简单的约束理论时表现良好，如线性代数和布尔理论，但当子句引用归纳定义的结构（如列表或树）上的约束时，它们的效率会大大降低。最近，我们提出了一种转换技术，用于消除那些归纳定义的数据结构，从而避免了将归纳原理纳入CHC求解器的需要。然而，这种技术可能会失败时，转换需要使用的lemmata的生成需要独创性。在本文中，我们通过一个例子，如何在转换CHCs消除归纳定义的结构的过程中，可以引入合适的谓词，称为差异谓词，其定义对应于引理被引入。通过第二个例子，我们表明，每当差异谓词不能介绍，我们可以介绍，而不是，辅助查询也对应于引理，这些引理的证明可以通过显示这些查询的可满足性。
2019-08-20 cs.LO cs.PL cs.SC
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
我们考虑QBF的最小不可满足核（MUC）的增量计算。为此，我们为增量QBF求解器DepQBF配备了一个新的API，以允许基于子句组的增量求解。子句组是一组子句，这些子句被递增地添加到先前求解的QBF中或从先前求解的QBF中移除。我们的新API的实现与基于选择器变量和假设的增量SAT求解有关。然而，API完全隐藏了用户的选择器变量和假设，这有利于DepQBF在其他工具中的集成。我们目前的实施细节，并首次报告相关的实验使用DepQBF的新条款组API的QBF的MUCs的计算。
2015-07-23 cs.LO
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
ENIGMA: Efficient Learning-based Inference Guiding Machine
Czech Technical University in Prague（布拉格捷克理工大学）
ENIGMA是一种基于学习的方法，用于指导基于饱和定理证明器中给定子句的选择。许多证明搜索中的子句根据它们在证明中的参与程度被分为肯定和否定。一个有效的分类模型是在这些数据上训练的，使用快速的基于特征的子句表征。然后，学习的模型与核心证明器紧密相连，并用作新的参数化评估启发式的基础，该启发式提供所有生成的子句的快速排名。该方法在E prover和CASC 2016 AIM基准上进行了评估，显示E的性能大幅提高。
2017-01-23 cs.AI cs.LG cs.LO
