parSAT: Parallel Solving of Floating-Point Satisfiability
本文提出parSAT方法，通过将浮点可满足性问题重新形式化并结合全局优化与多核并行执行，构建面向浮点算术的组合式半决策过程，以补充传统SMT求解器在非线性浮点约束求解中的不足。
2025-09-16 cs.LO
A Comparison of Logic Programming Approaches for Representation and Solving of Constraint Satisfaction Problems
许多基于逻辑编程的方法可以用来描述和解决组合搜索问题。一方面，有确定性程序和约束逻辑程序，它们计算解作为对包含约束满足问题的变量的查询的答案替换。另一方面，也有基于稳定模型语义、溯因和一阶逻辑模型生成的方法，这些方法将解计算为某些理论的模型。本文从知识表示（程序的声明性如何）和性能（它们在解决典型问题时的表现如何）的角度比较了这些不同的方法。
2000-03-08 cs.LO
Distributed Incremental SAT Solving with Mallob: Report and Case Study with Hierarchical Planning
本报告扩展了Mallob平台以支持增量SAT求解，并在层次规划案例中验证，通过并行处理587个规划实例，在多个领域显著加速了求解过程。
2025-05-24 cs.DC cs.LO
Solving SAT By Computing A Stable Set Of Points In Clusters
本文提出以簇为单位计算稳定点集（SSP）来求解SAT，避免逐点计算不可行的问题，从而更好地利用公式结构并促进并行SAT求解。
2025-07-17 cs.LO
Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution)
许多现代的求解器都提供了增量SAT求解的功能，这会在调用过程中保留求解器的状态。当需要将多个密切相关的SAT查询提供给求解器时，这是有益的。Pinaka是一个符号执行引擎，它积极使用增量SAT解决加上急切状态不可行性检查。它建立在CProver/Symex框架之上。Pinaka支持广度优先搜索和深度优先搜索作为状态探索策略，以及部分和完全增量模式。对于SVCOMP 2019，Pinaka被配置为使用部分增量模式和深度优先搜索策略。
2019-03-06 cs.LO
Finding Connections via Satisfiability Solving
TU Wien（维也纳工业大学）；University of Southampton（南安普顿大学）
本文提出了一种基于SAT的连接演算方法，通过编码证明搜索结构来提升一阶逻辑证明的自动化水平。
2026-03-06 cs.LO
Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming
Universidad Nacional de Río Cuarto（里奥夸尔托国立大学）；CONICET（阿根廷国家科学研究委员会）
本文提出SATFuL，一种用于模糊逻辑的可满足性求解器，利用MINLP求解器处理模糊公式，支持多种模糊逻辑变体，性能优于现有产品逻辑求解器。
2026-08-31 cs.LO
Solving Distributed Flexible Job Shop Scheduling Problem Using SAT
Faculty of Information Technology, VNU University of Engineering and Technology（信息技术学院，越南国立大学工程技术大学）
本文提出一种基于SAT的精确方法求解分布式柔性作业车间调度问题，在76个基准实例中使72个实例达到最优，部分实例改进了最佳完工时间，是有效的互补精确方法。
2026-11-04 cs.LO
Effectiveness of pre- and inprocessing for CDCL-based SAT solving
Universität zu Köln（科隆大学）
在搜索之前和搜索过程中应用预处理和内处理技术来简化CNF公式可以大大提高现代SAT求解器的性能。这些算法主要旨在减少公式中的子句、文字和变量的数量。然而，为了值得，它们的附加运行时间必须不超过在后续SAT求解器执行期间保存的运行时间。在本文中，我们调查的效率和实用性选择的简化算法的CDCL为基础的SAT求解。我们首先分析他们的CNF公式和SAT解决所有的预期影响。在现实世界和组合SAT实例上测试它们的同时，我们展示了哪些技术和它们的组合产生了理想的加速，哪些应该避免。
2013-10-17 cs.AI cs.LO
A Logical Approach to Efficient Max-SAT solving
加权Max-SAT是SAT的优化版本，许多重要问题可以自然编码。求解加权Max-SAT问题是一个重要的理论和实际问题。近年来，有相当大的兴趣，在寻找有效的解决技术。这项工作的大部分集中在良好的质量下限的计算中使用的分支和绑定DPLL类算法。大多数情况下，这些下限是以程序的方式描述的。因此，很难实现后面的{ \em逻辑}。在本文中，我们介绍了一个原始的Max-SAT框架，强调与经典SAT的并行性。然后，我们扩展了两个基本的SAT求解技术：{ \em search}和{ \em inference}。我们表明，许多算法{ \em技巧}中使用的国家的最先进的最大-SAT求解器很容易表达在{ \em逻辑}方面与我们的框架在一个统一的方式。此外，我们引入了一个原始的搜索算法，执行有限数量的{ \em加权分辨率}在每个访问节点。我们经验比较我们的算法与各种解决方案的几个基准。据我们所知，我们的实验构成了有史以来最全面的Max-sat评估报告，表明我们的算法通常比任何竞争对手快几个数量级。
2006-11-06 cs.AI cs.LO
Prioritized Unit Propagation with Periodic Resetting is (Almost) All You Need for Random SAT Solving
DeepMind（深度思维）；University of Pennsylvania（宾夕法尼亚大学）
我们提出了定期重置的优先单位传播，这是一个简单但令人惊讶的有效算法，用于解决随机SAT实例，这意味着很难。特别是，对2017年和2018年SAT竞赛的随机轨道的评估表明，这个简单想法的基本原型已经在这两年排名第二。我们分享这一观察结果，希望它能帮助SAT社区更好地理解竞赛中使用的随机实例的难度，并激发其他关于SAT求解的有趣想法。
2019-12-04 cs.AI cs.LG cs.LO
Scalable SAT Solving in the Cloud
以前的努力，使可满足性（SAT）解决适合高性能计算（HPC）导致超线性加速特定的公式，但大多数输入不能有效地利用大量的处理器。此外，作业调度的长延迟（几分钟到几天）使得大规模SAT按需求解对于大多数应用程序来说是不切实际的。我们用Mallob解决这两个问题，Mallob是一个在SAT求解的背景下进行作业调度的框架，它利用了延展性，即，在作业的计算过程中增加或减少其处理能力的能力。Mallob包括一个基于Hordesat的大规模并行，分布式和可延展的SAT求解引擎，具有更简洁和通信效率更高的子句共享方法，并对其前身进行了许多进一步的改进。例如，在640个内核上的Mallob性能优于在2560个内核上更新和改进的Hordesat配置。此外，Mallob还可以并行求解许多公式，同时动态地适应分配的资源，并且到达系统的作业通常在几分之一秒内启动。
2022-05-13 cs.DC cs.LO
A novel approach of solving the CNF-SAT problem
本文讨论了CNF-SAT问题（NP-Complete problem），分析了两种解决该问题的方法：PL-Resolution算法和WalkSAT算法。PL-归结是一个可靠的、完备的算法，可以用来确定可满足性和不可满足性。如果WalkSAT找到了一个模型，它可以确定可满足性，但即使存在模型，它也不能保证找到一个模型。然而，WalkSAT比PL-Resolution快得多，这使得WalkSAT更实用;并且我们分析了这两种算法的性能，如果问题不是很难，WalkSAT的性能是可以接受的。
2013-07-24 cs.AI cs.LO
GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
University of Maryland（马里兰大学）；NVIDIA Research（英伟达研究院）；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Michigan（密歇根大学）
本文提出GaloisSAT，一种结合GPU和CPU的新型SAT求解器，利用可微SAT求解引擎和传统CDCL方法，显著提升SAT竞赛指标PAR-2性能。
2026-03-25 cs.AI cs.LO
A novel algorithm for solving the Decision Boolean Satisfiability Problem without algebra
本文描述了一个算法，解决决策布尔可满足性问题的一个特殊的决策可满足性问题的二进制数值性质，并行执行，面向对象，和短终止。用扩展和简化这两种操作来解释为什么使用代数增加了分辨率步骤。证明了该问题的复杂度有一个上界为$2^{n-1}$，其中$n$是给定问题的逻辑变量数.
2018-04-14 cs.CC cs.DS cs.LO
diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
National University of Ireland, Galway（爱尔兰国立高威大学）
本文介绍了diff-SAT，一个答案集和SAT求解器，它结合了经常使用概率条款，事实和规则的能力，解决和采样的最佳世界观（满足布尔变量分配或答案集的多集）受用户提供的概率约束。采样过程使用称为可微可满足性求解（$\partial\mathrm{SAT}$）或可微答案集编程（$\partial\mathrm{ASP}$）的基于梯度下降的优化方法来最小化用户定义的可微目标函数。用例是i.a.概率逻辑编程（以概率答案集编程的形式），概率布尔可满足性求解（PSAT）和模型多集（答案集或布尔解释）的分布感知采样。
2021-01-03 cs.AI cs.LO
Orthologic for SAT Solving
EPFL（苏黎世联邦理工学院）
本文提出一种新的正交逻辑公式蕴含判定算法，避免了先前方法的高成本预处理阶段，同时保持相同的最坏复杂度。通过合成SAT基准测试，展示了正交逻辑归一化在某些难题中的提升效果。
2026-05-14 cs.AI cs.LO
Machine Learning Methods in Solving the Boolean Satisfiability Problem
Shanghai Jiao Tong University（上海交通大学）
本文综述了利用机器学习求解布尔可满足性问题（SAT）的最新进展，涵盖从手工特征分类器到端到端求解器（如NeuroSAT）以及CDCL和局部搜索与机器学习的结合，并指出了当前局限与未来方向。
2022-03-02 cs.AI cs.LG cs.LO
Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability
本文描述了多常数乘法（MCM）问题到伪布尔可满足性（PBS）的三种编码，并介绍了一种最优求解MCM问题的算法。据我们所知，所提出的编码和优化算法是第一次正式的MCM问题在PBS的方式。该报告评估了问题大小的复杂性和几个PBS求解器在三种编码上的性能。
2011-05-17 cs.LO math.LO math.OC
Solving MaxSAT by Successive Calls to a SAT Solver
Cairo University（开罗大学）
最大可满足性（MaxSAT）问题是在合取范式（CNF）中找到使给定布尔公式的满足子句的数目最大化的真值分配的问题。近年来，MaxSAT的许多精确求解器已经开发出来，其中许多都在著名的SAT会议上发表。MaxSAT的算法一般分为两类：（1）分支定界算法和（2）连续调用SAT求解器的算法（基于SAT的），在实际问题中，基于SAT的算法被证明是更有效的。本文提供了一个实验研究，以比较最近的SAT为基础的分支定界算法的MaxSAT评估基准的性能。
2016-03-11 cs.AI cs.CC cs.LO
SAT-Solving the Poset Cover Problem
National Taiwan Normal University（台湾师范大学）；Academia Sinica（中央研究院）
针对偏序集覆盖问题，提出一种基于交换图的SAT归约方法，利用现代SAT求解器高效求解中等规模实例，实验验证了有效性。
2026-06-16 cs.DM cs.LO
Industrial-Strength Formally Certified SAT Solving
University of Southampton（南安普顿大学）；University College Dublin（都柏林大学学院）
布尔可满足性（SAT）求解器现在经常用于大型工业问题的验证。然而，它们在安全关键领域（如铁路、航空电子和汽车行业）的应用需要某种形式的结果保证，因为求解器可能（有时确实）有错误。不幸的是，现代的，高度优化的SAT求解器的复杂性，使不切实际的直接形式证明其正确性的发展。本文提出了一种替代方法，其中一个不可信的，工业强度，SAT求解器插入到一个可信的，正式认证，SAT证明检查提供工业强度认证的SAT解决方案。我们的方法的主要新颖性和特点是：（一）检查器是自动提取的正式开发，（二），组合系统可以作为一个独立的可执行程序独立于任何支持定理证明，及（iii）检查器证明任何SAT求解器尊重商定的格式可满足性和不可满足性索赔。该系统的核心是一个经过认证的检查器，用于检查在Coq中正式设计和验证的不可满足性声明。我们提出了它的形式化设计和大纲的正确性证明。实际的独立检查器是从Coq开发中自动提取的。一个有代表性的一组工业基准从SAT竞赛的认证检查器的评估表明，虽然它是慢于未经认证的SAT检查器，它是显着快于认证的检查器上实现的交互式定理证明。
2009-12-17 cs.AI cs.LO
Generalizing Unit Commitment Problem Solving via SAT-based Decoupling
School of Software Engineering, South China University of Technology（华南理工大学软件学院）；School of Software Engineering, Sun Yat-sen University（中山大学软件学院）；Department of Mathematics, College of Science, Shantou University（汕头大学理学院数学系）
本文提出基于SAT的解耦方法，使单一算法能解决多种单位调度问题变体，提升求解质量和泛化能力。
2026-04-13 cs.CE cs.LO
Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
Rice University（莱斯大学）；Indian Institute of Technology, Bombay（印度理工学院孟买分校）；University of California, Berkeley（加州大学伯克利分校）；IBM Research（IBM研究院）；Princeton University（普林斯顿大学）
约束抽样和计数是人工智能中的两个基本问题，具有广泛的应用范围，跨越概率推理和规划到约束随机验证。虽然这些问题的理论在20世纪80年代被彻底研究，但以前的工作要么没有扩展到工业规模的实例，要么放弃了正确性保证以实现可扩展性。最近，我们提出了一种新的方法，它结合了通用哈希和SAT求解，并扩展到具有数十万个变量的公式，而不放弃正确性保证。本文概述了该方法的关键要素，并讨论了处理更大的现实世界实例需要克服的挑战。
2015-12-21 cs.AI cs.LO
On Continuous Local BDD-Based Search for Hybrid SAT Solving
Rice University（莱斯大学）
我们探讨了连续局部搜索（CLS）在SAT求解的潜力，提出了一种新的方法来寻找一个混合系统的布尔约束的解决方案。该算法是基于CLS结合置信传播二叉决策图（BDD）。我们的框架接受所有的布尔约束，承认紧凑的BDD，包括对称布尔约束和小系数伪布尔约束作为有趣的家庭。我们提出了一种新的算法，有效地计算CLS所需的梯度。我们研究我们的多功能CLS求解器，GradSAT的能力和局限性，通过将其应用于许多基准测试实例。实验结果表明，GradSAT可以是一个有用的除了现有的SAT和MaxSAT求解器解决布尔可满足性和优化问题的投资组合。
2021-06-12 cs.AI cs.IT cs.LG
Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
Department of Computer Science, Rice University（计算机科学系，里士大学）；Department of Applied Mathematics and Statistics, Colorado School of Mines（应用数学与统计系，科罗拉多矿业学院）；Department of Mathematics, University of California, Los Angeles（数学系，加州大学洛杉矶分校）
本文针对混合SAT求解问题，提出基于惩罚项的无约束连续优化公式，并通过理论与实验证明Adam等无约束优化器能有效提升混合基准上的SAT求解性能。
2025-05-31 cs.AI cs.LG cs.LO
Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
Purdue University（普渡大学）
提出XOR-SMC算法，通过随机化XOR约束将NP^PP-完全的模计数可满足性问题转化为SAT问题，在多项式时间内提供常数近似保证，并在AI向善实验中优于基线。
2023-12-30 cs.AI cs.CC cs.LO
Boolean Equi-propagation for Optimized SAT Encoding
Ben Gurion University of the Negev（本古里安大学）；Cadence Design Systems（楷登电子设计系统公司）；The University of Melbourne（墨尔本大学）
我们提出了一种基于传播的解决方法，布尔等传播，其中的约束建模为传播布尔文字之间的平等的信息。基于传播的求解将此信息作为部分评估的形式应用，从而得到优化的SAT编码。我们证明了各种基准测试，我们的方法在较小的CNF编码的结果，并导致加快解决时间。
2011-04-24 cs.AI cs.DS cs.LO
Effective problem solving using SAT solvers
University of Waterloo（滑铁卢大学）；Maplesoft（Maplesoft公司）；Wilfrid Laurier University（劳里埃大学）
在这篇文章中，我们将演示如何使用计算机代数系统Maple的内置SAT求解器来解决各种问题和谜题。一旦问题被编码到布尔逻辑中，就可以自动找到解决方案（或显示不存在），而不需要实现任何搜索算法。特别是，我们描述了如何解决$n$ -皇后问题，如何生成和解决数独难题，如何解决像爱因斯坦之谜这样的逻辑难题，如何解决15-难题，如何解决最大集团问题，以及寻找希腊-拉丁方。
2019-09-16 cs.AI cs.LO cs.SC
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 the Computational Complexity of Satisfiability Solving for String Theories
可满足性求解器在软件验证中发挥着越来越重要的作用，特别是在安全漏洞分析中的有效使用。字符串处理是许多软件应用程序（如浏览器和Web服务器）的关键部分。这些应用程序容易受到通过网络接收的恶意数据的攻击。因此，用于分析此类应用程序安全性的自动化工具需要对字符串进行推理。出于效率的原因，最好有一个将字符串视为第一类类型的求解器。在本文中，我们提出了一些理论的字符串，是有用的软件安全的背景下，并分析了计算复杂性的理论。我们使用这种复杂性分析，激发字节爆炸的方法，采用布尔编码的字符串约束相应的布尔可满足性问题。
2009-03-16 cs.CC cs.LO cs.PL
Can Transformers Reason Logically? A Study in SAT Solving
University of YYY（YYY大学）；Institute of WWW（WWW研究院）
本文通过理论构造与实证训练，研究仅解码器Transformer在3-SAT求解中的逻辑推理能力，证明其可通过思维链进行回溯与演绎，并发现训练模型分布外泛化强但长度泛化有限。
2025-02-08 cs.AI cs.LG cs.LO
An attack on Zarankiewicz's problem through SAT solving
Zarankiewicz函数给出了，对于一个选定的矩阵和子矩阵，在一个不包含全一子矩阵的二进制矩阵中的最大1个数。此函数的小参数表已经编译，但其中存在已知错误。我们都纠正错误，并扩展这些表的情况下，平方未成年人表示的问题，找到一个特定的点作为一系列的布尔可满足性问题的值，利用置换对称性显着减少所需的工作。当环境矩阵也是正方形，我们也给所有非同构的例子矩阵达到最大值，到上述对称性;它被发现，最大的矩阵有某种形式的对称性。
2022-04-19 cs.DM cs.LO math.CO
FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints
Rice University（莱斯大学）
布尔可满足性问题（SAT）是计算机科学中的一个重要问题.虽然SAT被认为是NP完全的，但在工程方面的进展，特别是基于子句驱动的子句学习（CDCL）和局部搜索SAT求解器，已经取得了显着的进展。然而，虽然旨在以合取范式（CNF）求解工业规模基准的SAT求解器已经变得相当成熟，但是对其他类型的约束有效的SAT求解器，例如，基数约束和异或的研究较少;处理非CNF约束的一般方法仍然缺乏。此外，以前的工作表明，对于特定类别的基准测试，现有的SAT求解器的运行时间在很大程度上取决于公式的属性和编码的细节，而不是基准测试的规模，这增加了不确定性的预期运行时间。为了解决上述问题，我们设计了FourierSAT，一个不完全SAT求解器的基础上傅立叶分析的布尔函数，一种技术来表示布尔函数的多线性多项式。通过这种连续优化的减少，我们提出了一个代数框架，用于解决由不同类型的约束组成的系统。这个想法是利用梯度信息来引导搜索过程中的局部改进的方向。实证结果表明，傅立叶SAT是更强大的比其他求解器在某些类的基准。
2020-02-24 cs.IT cs.LG cs.LO
