ML Supported Predictions for SAT Solvers Performance
Federal Office for Information Security（德国联邦信息安全办公室）
为了对开源SAT求解器CryptoMiniSat在多线程模式下处理难以解决布尔可满足性问题实例时的不确定性终止行为进行分类，收集并分析了内部求解器运行时参数。这些参数的子集已被选择并用作特征向量，以成功地创建机器学习模型，用于对求解器的终止行为进行二进制分类，并对尚未求解的实例进行任何新的求解运行。该模型可用于早期估计的解决尝试属于或不属于类的候选人具有良好的机会快速终止。在这种情况下，运行时特性的活动配置文件的组合似乎反映了求解器的瞬时性能对求解器的解决过程的即时质量的影响。由于前两次求解迭代的运行时参数足以预测成功分数良好的尝试的终止，因此本工作的结果提供了一个有希望的基础，可以进一步开发，以丰富CryptoMiniSat或任何具有AI能力的现代SAT求解器。
2021-12-17 cs.AI cs.CR cs.LG
SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
CRIL；Artois University（阿尔图瓦大学）；Univ. Bordeaux（波尔多大学）；Bordeaux INP（波尔多国立理工学院）；CNRS（法国国家科学研究中心）
SAT研究有着悠久的源代码和二进制版本的历史，这要归功于每年组织的竞赛。然而，由于每个竞争周期都有自己的一套规则和发布源代码和二进制文件的特殊方式，编译甚至运行任何求解器可能比看起来更难。此外，到目前为止，已经有超过一千个求解器发布，其中一些是在90年代初发布的。如果SAT社区想要存档并能够跟踪所有创造历史的求解器，它迫切需要部署一项重要的工作。我们建议发起一个社区驱动的努力，存档并允许轻松编译和运行迄今为止发布的所有SAT求解器。我们依靠最好的工具来归档和构建二进制文件（感谢Docker，GitHub和Zenodo），并为此提供一致且简单的方法。多亏了我们的工具，从源代码（或二进制文件）构建（或运行）求解器可以在一行中完成。
2020-06-02 cs.AI
Proteus: A Hierarchical Portfolio of Solvers and Transformations
Insight Centre for Data Analytics（Insight数据分析中心）；University College Cork（科克大学学院）
近年来，解决SAT问题和CSP的组合方法越来越普遍。还有许多不同的编码用于将CSP表示为SAT实例。在本文中，我们利用SAT和CSP求解的进展，提出了一种新的分层投资组合为基础的方法来解决CSP，我们称之为Proteus，不纯粹依赖于CSP求解器。相反，它可以决定最好将CSP问题实例编码为SAT，选择适当的编码和相应的SAT求解器。我们的实验评估使用了一个实例的变形，涉及四个CSP求解器，三个SAT编码，和六个SAT求解器，评估最具挑战性的问题实例从CSP求解器的竞争，涉及全球和内涵的约束。我们表明，显着的性能改善，可以通过利用其他观点和求解器组合解决问题的变形。
2014-02-17 cs.AI
SATzilla: Portfolio-based Algorithm Selection for SAT
University of British Columbia（英属哥伦比亚大学）
人们已经广泛观察到，没有单一的“主导”SAT求解器;相反，不同的求解器在不同的实例上表现最好。我们主张根据每个实例在线做出此决定，而不是遵循为给定实例类选择最佳求解器的传统方法。在以前工作的基础上，我们描述了SATzilla，一种自动化方法，用于构建SAT的每个实例算法组合，使用所谓的经验硬度模型来选择其组成求解器。这种方法将问题实例的分布和一组组件求解器作为输入，并构造优化给定目标函数（例如平均运行时间、已解决实例的百分比或竞赛得分）的投资组合。SATzilla的卓越性能在2007年SAT竞赛中得到了独立验证，我们的SATzilla 07求解器赢得了三枚金牌，一枚银牌和一枚铜牌。在本文中，我们通过使组合构建可扩展和完全自动化，并通过集成本地搜索求解器作为候选求解器，通过预测性能得分而不是运行时，以及通过使用考虑不同类型SAT实例的分层硬度模型来改进它，从而远远超出了SATzilla 07。我们证明了这些新技术的有效性，在广泛的实验结果的数据集，包括最近的SAT比赛的实例。
2011-10-31 cs.AI
Fudge: A light-weight solver for abstract argumentation based on SAT reductions
University of Koblenz-Landau（科布伦茨-兰道大学）；University of Brescia（布雷西亚大学）；University of Huddersfield（哈德斯菲尔德大学）
我们提出了福吉，一个抽象的论证求解器，紧密结合可满足性求解技术来解决一系列抽象的论证问题。虽然福吉使用的大多数编码都来自标准的翻译方法，但福吉使用了全新的编码来解决怀疑推理问题。优选的语义和问题WRT。理想语义学
2021-09-07 cs.AI
Dsat: A Native SAT Solver for Discrete Logic
Department of Computer Science, University of California, Los Angeles（加州大学洛杉矶分校计算机科学系）
本文提出一种用于离散逻辑的原生SAT求解器，通过扩展布尔逻辑，允许变量取任意值，并通过与CSP求解器、布尔SAT求解器等的比较验证其有效性。
2026-05-10 cs.AI cs.LO
MatSat: a matrix-based differentiable SAT solver
National Institute of Informatics (NII)（国立情报学研究所）；Kyoto University（京都大学）
我们提出了一种新的方法来解决SAT问题，解决SAT问题在向量空间中的成本最小化问题的非负可微成本函数J^sat。在我们的方法中，解决方案，即，满足赋值，对于n个变量的SAT问题，由{0，1}^n中的二进制向量u表示，使J^sat（u）为零。我们通过成本最小化在向量空间R^n中搜索这样的u，即，从初始u_0开始，并在通过牛顿方法迭代更新u的同时将J最小化为零。我们实现了我们的方法作为一个基于矩阵的差分SAT求解器MatSat。虽然现有的主流SAT求解器一个接一个地决定解决方案分配的每个比特，无论是冲突驱动子句学习（CDCL）类型还是随机局部搜索（SLS）类型，但MatSat与它们的根本不同之处在于它在向量空间中连续地接近解决方案。我们进行了一个实验来测量MatSat的可扩展性与随机3-SAT问题，其中MatSat可以找到一个解决方案，n=10^5个变量。我们还使用SAT 2018竞赛的随机基准集和人工随机3-SAT实例集，将MatSat与四个最先进的SAT求解器进行了比较，其中包括2018年SAT竞赛和2019年SAT竞赛的获胜者。结果表明，MatSat在两个测试集上都排在第二位，优于所有CDCL类型的求解器。
2021-08-14 cs.AI
Solving Rubik's Cube Using SAT Solvers
Donghua University（东华大学）
魔方是一种简单易懂的益智游戏，最初被称为“魔方”。这是一个著名的规划问题，已经研究了很长时间。然而，许多简单的属性仍然未知。本文研究了现代SAT求解器是否适用于这个难题。据我们所知，我们是第一个将魔方转化为SAT问题的人。为了减少编码所需的变量和子句的数量，我们用3个或2个布尔变量的新方法代替了6个布尔变量的朴素方法来表示每个面元上的每种颜色。为了能够快速求解魔方，我们在6型圈的基础上，用18子类型圈的分层编码代替了18圈的直接编码。为了进一步加快求解速度，我们将两阶段算法的一些性质编码为附加约束，并通过添加约束子句来限制某些移动序列。仅使用有效编码无法解决这个难题。为此，我们改进了现有的SAT求解器，并开发了一个新的SAT求解器的基础上PrecoSAT，虽然它是只适用于魔方。新的SAT求解器用ALO（\emph{at-least-one}）求解策略取代了前视求解策略，并将原问题分解为多个子问题。每个子问题都由PrecoSAT解决。实验结果表明，我们的SAT翻译和新的解决技术是有效的。如果没有有效的SAT编码和新的求解技术，魔方将无法被任何SAT求解器求解。使用改进的SAT求解器，我们总是可以找到一个解决方案的长度为20在一个合理的时间。虽然我们的求解器比使用查找表的Kociemba算法慢，但不需要庞大的查找表。
2011-05-07 cs.AI
GpuShareSat: a SAT solver using the GPU for clause sharing
我们描述了一个SAT求解器使用GPU（CUDA）和CPU与一个新的子句交换策略。CPU运行经典的多线程CDCL SAT求解器。每个CPU线程将它学习的所有子句导出到GPU。GPU大量使用按位操作。它会注意到CPU线程何时使用了子句，并通知该线程，在这种情况下，它会导入该子句。这依赖于GPU针对数百个任务反复测试数百万个子句。所有子句都是彼此独立测试的（这允许GPU大规模并行方法），但是使用逐位操作同时针对所有赋值进行测试。这允许CPU线程只导入对它们有用的子句。我们的求解器是基于葡萄糖浆。实验表明，这导致了强大的性能提升，在SAT 2020竞赛中解决的实例比葡萄糖浆多22个。
2020-12-05 cs.AI
Local Consistency and SAT-Solvers
University of Oxford（牛津大学）
局部一致性技术，如k-一致性是约束满足问题的专用求解器的关键组成部分。在本文中，我们表明，使用k-一致性技术的权力，约束满足问题，正是通过使用一个特定的推理规则，我们称之为负超分辨率，标准的直接编码的问题，布尔子句。我们还表明，目前的子句学习SAT求解器将发现在预期的多项式时间的任何不一致，可以推断出从一组给定的子句使用负超解式的固定大小。我们结合这两个结果表明，没有明确设计这样做，目前的子句学习SAT求解器有效地模拟k-一致性技术，为所有固定值的k。然后，我们给出了一些实验结果表明，这个功能允许子句学习SAT求解器有效地解决某些家庭的约束问题，这是传统的约束编程求解器的挑战。
2014-01-18 cs.AI cs.LO
Implementing Efficient All Solutions SAT Solvers
University of Electro-Communications（电气通信大学）；Kobe University（神户大学）
所有解SAT（AllSAT）是命题可满足性问题的一个变种。尽管其重要性，AllSAT与其他变体相比相对未被探索。因此，我们调查和讨论AllSAT求解器的主要技术。我们忠实地实现它们，并使用大量的实例和各种类型的求解器（包括少数几个公共软件之一）进行全面的实验。实验结果表明了该算法的特点。我们实现的求解器是公开的，以便其他研究人员可以很容易地通过修改我们的代码来开发他们的求解器，并将其与现有的方法进行比较。
2015-10-02 cs.AI cs.DS cs.LO
Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis
University of California Los Angeles（加利福尼亚大学洛杉矶分校）；The Pennsylvania State University（宾夕法尼亚州立大学）；University of Virginia（弗吉尼亚大学）
基于CNF的SAT和MaxSAT求解器是逻辑综合和验证系统的核心。这些约束问题在电子设计自动化中的日益普及，鼓励了对不同SAT问题及其性质的研究，以进一步提高计算效率。现代的基于语法驱动的子句学习SAT求解器在理论和实践上都取得了成功，它允许在相对较短的时间内解决非常大的工业实例。最近，机器学习方法为解决这一具有挑战性的问题提供了新的维度。神经符号模型可以作为通用求解器，可以基于数据专门用于特定领域，而无需对模型的结构进行任何更改。在这项工作中，我们提出了一个单次模型来自Transformer架构来解决最大SAT问题，这是SAT的优化版本，其目标是满足最大数量的条款。我们的模型具有无标度结构，可以处理不同大小的实例。我们使用元路径和自我注意力机制来捕捉同构节点之间的交互。我们在二分图上采用交叉注意力机制来捕捉异构节点之间的交互。我们进一步应用迭代算法，我们的模型，以满足额外的条款，使解决方案接近的一个确切的SAT问题。注意力机制利用并行性来加速。我们的评估表明，改进的加速比相比，启发式方法和改进的完成率相比，机器学习方法。
2021-07-15 cs.AI cs.LG cs.NE
Online Search Cost Estimation for SAT Solvers
The University of New South Wales（新南威尔士大学）；NICTA（澳大利亚国家信息与通信技术研究院）
我们提出了两种不同的方法来估计解决SAT问题的成本。该方法侧重于回溯求解器的在线行为，以及问题的结构。现代SAT求解器提出了几个挑战，估计搜索成本，包括应对非时序回溯，学习和重新启动。我们的第一种方法采用现有的算法来估计搜索树的大小，以应对这些挑战。然后，我们提出了第二种方法，该方法使用在搜索开始时在线收集的数据上训练的线性模型。我们使用随机和结构化问题比较这两种方法的有效性。我们还表明，在早期重新启动的预测可以用来改善以后的预测。我们的结论表明，解决一组问题的成本可以通过选择一个解决方案，从投资组合的基础上，这样的成本估计减少。
2009-07-29 cs.AI
Evaluating SAT Solver Metrics as Predictors of Human-Perceived Nonogram Difficulty
University of Alberta（阿尔伯塔大学）；University of Toronto（多伦多大学）
该研究针对Nonogram谜题验证算法求解器工作量与人类感知难度的关联，通过用户研究发现二者无显著关联，且专业知识会调节该关系，同时揭示人类求解偏好与SAT求解器测量的复杂性存在差异。
2026-08-25 cs.AI cs.HC
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
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
Fast Set Bounds Propagation Using a BDD-SAT Hybrid
National ICT Australia（澳大利亚国家信息通信技术中心）；The University of Melbourne（墨尔本大学）；Cadence Design Systems（铿腾电子科技公司）
基于二叉决策图的集合边界传播是求解集合约束满足问题的一种有效方法.然而，现有的基于BDD的技术在搜索期间构造和操纵图的显著开销。我们提出了一个集约束求解器，它结合了BDD为基础的集边界传播与现代SAT求解器的学习能力。再加上一些改进的基本算法，这个求解器是非常有竞争力的现有的传播为基础的集合约束求解器。
2014-01-16 cs.AI
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
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
Using deep learning to construct stochastic local search SAT solvers with performance bounds
Porsche Digital GmbH（保时捷数字集团）
本文提出利用图神经网络作为或acles，提升SLS求解器性能，通过随机和伪工业SAT实例验证，显著提高求解效率和实例解决数量。
2026-04-16 cs.AI math.OC
Hardware Acceleration for Boolean Satisfiability Solver by Applying Belief Propagation Algorithm
University of Michigan（密歇根大学）
布尔可满足性（SAT）在计算机科学中有着广泛的应用领域，特别是在电子设计自动化中的应用。电路综合，优化和验证问题可以通过将原始问题转化为SAT问题来解决。然而，可满足性问题是NP完全问题，目前还没有有效的求解方法，因此需要一种有效的可满足性问题求解器来提高其性能。我们提出了一种硬件加速方法的SAT问题。通过对SAT问题和一类特殊的纠错码--低密度奇偶校验码（LDPC）的译码问题的研究，发现它们都是约束满足问题。置信传播算法已成功地应用于LDPC码的译码，并对相应的译码器硬件设计进行了广泛的研究。因此，我们提出了一种基于置信传播的算法来解决SAT问题。利用该算法，可满足性问题求解器可以通过硬件加速。通过软件仿真验证了算法的有效性，并对算法的性能改进进行了评估.我们的实验结果表明，时间复杂度不增加SAT问题的大小，所提出的方法可以实现至少30倍的速度比MiniSat。
2016-03-16 cs.AI cs.LO
AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems
Georgia Institute of Technology, USA（佐治亚理工学院）；University of Waterloo, Canada（滑铁卢大学）；University of Windsor, Canada（温莎大学）
AlphaMapleSAT通过结合MCTS与演绎反馈，改进了立方与征服SAT求解器，显著提升了解决难题组合问题的效率。
2026-01-20 cs.AI math.CO
Fast Analysis of the OpenAI O1-Preview Model in Solving Random K-SAT Problem: Does the LLM Solve the Problem Itself or Call an External SAT Solver?
University of Florence（佛罗伦萨大学）
本文分析了OpenAI O1-preview模型在求解随机K-SAT问题时的表现，发现其通过调用外部SAT求解器而非直接求解，且输出常含错误赋值，并提出方法量化其展现智能火花还是随机猜测。
2024-09-20 cond-mat.dis-nn cs.AI cs.CL
Using SMT Solvers to Validate Models for AI Problems
Alexandru Ioan Cuza University of Iaşi（雅西亚历山德鲁·伊万·库扎大学）
人工智能问题，从规划/调度到游戏控制，包括一个重要的关键步骤：描述一个模型，该模型准确定义了问题所需的数据，要求，允许的过渡和既定的目标。模型失败的方式有很多，并且通常会导致搜索策略无法提供快速、最佳甚至任何解决方案。本文提出使用SMT（可满足性模理论）求解器，如Z3，来检查模型的有效性。我们提出两个测试：检查最终（目标）状态是否存在于模型描述的问题空间中，并检查所描述的转换是否可以提供从所识别的初始状态到任何目标状态的路径（意味着已经找到解决方案）。使用SMT求解器进行AI模型检验的优点在于，它们替代了实际的搜索策略，并且它们处理模型的抽象表示，即一组逻辑公式。在抽象层面上进行推理并不像探索整个解决方案空间那样昂贵。SMT求解器使用有效的决策过程，为与AI模型相对应的逻辑公式提供证明。Z3最近添加的一个功能允许我们将转换序列描述为递归函数，因此我们可以检查是否可以在定义的模型中找到解决方案。
2019-03-22 cs.AI cs.LO
HordeQBF: A Modular and Massively Parallel QBF Solver
Karlsruhe Institute of Technology (KIT)（卡尔斯鲁厄理工学院）；Vienna University of Technology（维也纳工业大学）
最近开发的大规模并行可满足性（SAT）求解器HordeSAT是以模块化的方式设计的，允许在其核心中集成任何基于顺序CDCL的SAT求解器。我们将基于QCDCL的量化布尔公式（QBF）求解器DepQBF集成到HordeSAT中，得到了一个大规模并行的QBF求解器--HordeQBF。在本文中，我们描述了这种整合的细节和报告的结果HordeQBF的性能的实验评估。HordeQBF在2014 QBF Gallery的硬应用实例上实现了超线性平均和中值加速。
2016-04-13 cs.AI cs.LO
Local-search techniques for propositional logic extended with cardinality constraints
我们研究了局部搜索可满足性求解器扩展的基数原子命题逻辑，也就是说，表达式，提供明确的方式来模型的基数集的约束。将基数原子添加到命题逻辑的语言中有助于对搜索问题进行建模，并且通常会导致简洁的编码。我们提出了两个“本地”本地搜索求解器的理论在扩展语言。我们还描述了技术，以减少问题的标准命题可满足性，并允许我们使用现成的SAT求解器。我们对这些方法进行了实验研究。我们的总体发现是，专门为扩展语言设计的本地求解器比依赖于SAT求解器的间接方法执行得更好。
2003-10-31 cs.AI
Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver
School of Computing, Australian National University（澳大利亚国立大学计算机学院）
提出AFSAT，一个基于连续局部搜索的GPU加速伪布尔SAT求解器，通过JAX编译器实现大规模并行化，显著提升数值稳定性、运行速度和内存效率。
2026-06-04 cs.AI cs.LO
Decentralized Constraint Satisfaction
Hamilton Institute, National University of Ireland Maynooth（爱尔兰国立大学梅努斯分校汉密尔顿研究所）；University of Toulouse（图卢兹大学）
我们发现，在无线网络中的几个重要的资源分配问题适合在共同的框架内的约束满足问题（CSP）。这些应用程序的要求，其中变量位于不同的网络设备，可能无法通信，但可能会干扰的启发，我们定义了自然的标准，CSP求解器必须具备，以实用。我们将这些算法称为分散式CSP求解器。最著名的CSP求解器是为集中式问题而设计的，不符合这些标准。我们介绍了一个随机分散CSP求解器，并证明了它会找到一个解决方案，在几乎肯定有限的时间，如果存在，也表明它有许多实际可取的属性。我们基准的算法的性能上的一个良好的研究类的CSP，随机k-SAT，说明该算法需要找到一个令人满意的分配的时间是有竞争力的随机集中式求解器的问题，为了一千个变量，尽管其分散的性质。我们证明了求解器的实际效用的问题，激励它的引入，用它来找到一个非干扰的信道分配从曼哈顿市中心的数据形成的网络。
2012-10-09 cs.AI
Translating finite-domain integer constraint models to CP/SMT/ILP/PB/SAT solvers with CPMpy
KU Leuven（鲁汶大学）；Nonfiction Software；Flanders Make（弗兰德斯制造）；University of Western Macedonia（西马其顿大学）；UCLouvain（天主教鲁汶大学）
本研究提出基于CPMpy的模块化框架，将高级约束模型转换为CP、SMT等多种求解器形式，可跨求解技术对比，优化线性化对ILP/PB求解器关键。
2026-08-18 cs.AI
Deeply Optimizing the SAT Solver for the IC3 Algorithm
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Advanced Computing and Intelligence Engineering, Wuxi, China（无锡先进计算与智能工程学院）；Beijing Forestry University（北京林业大学）
针对IC3算法中SAT查询的独特特征，提出变量决策子集计算、桶替代VSIDS二元堆、支持无额外激活变量的临时子句三项优化，集成于轻量级CDCL求解器GipSAT，使基于它的IC3求解速度比基于MiniSat的版本平均提升3.61倍。
2025-05-21 cs.AI cs.LO
Cache Performance Study of Portfolio-Based Parallel CDCL SAT Solvers
Universidad Católica de la Santísima Concepción（康塞普西翁天主教圣母大学）；Universidad de Concepción（康塞普西翁大学）
并行SAT求解器正在成为主流。他们的表现使他们连续两次赢得SAT比赛，并成为研究和工业界的焦点。问题是，我们并不确切地知道需要什么才能让他们表现得更好;也就是说，如何让他们在更短的时间内解决更多的问题。此外，也不知道它们在大规模多核环境中的扩展情况如何，可以预见的是，这是新硬件出现的情况。在本文中，我们表明，缓存争用是一个减缓可扩展性的罪魁祸首，并提供经验的结果，对于某些类型的搜索，物理共享线程之间的子句数据库是有益的。
2013-09-12 cs.AI cs.DC
Search for developments of a box having multiple ways of folding by SAT solver
Department of Computer Science, Gunma Univ.（群马大学计算机科学系）
一个多角形被称为一个发展，如果它可以通过折叠形成多角形的单位正方形的边缘来制作一个盒子。众所周知，有些开发可以通过多种方式折叠到一个或多个盒子中。在这项工作中，我们进行了计算机搜索，通过使用SAT求解器找到这样的发展。结果，我们发现了数千个这样的发展，包括一个面积为52的polyomino，它可以用五种不同的方式折叠成一个$1 \times 2 \times 8$大小的盒子。
2020-05-06 cs.AI cs.CG cs.DM
Speeding up SAT solver by exploring CNF symmetries : Revisited
在过去的几年里，布尔可满足性求解器通过考虑对称性在性能和可扩展性方面取得了巨大的进步。已经表明，通过使用图对称性和生成对称性破缺谓词（SBP），有可能破缺合取范式（CNF）中的对称性。SBPs在不影响CNF公式的可满足性的情况下，将搜索空间缩减到空间的非对称区域。通过将公式表示为图，找到图对称性并使用某种对称性提取机制（Crawford等人）来创建对称性破缺谓词。在本文中，我们采取一个非平凡的CNF，并探讨其对称性。最后，我们生成SBPs并将其添加到CNF中，我们展示了它如何帮助修剪搜索树，以便SAT求解器花费较短的时间。在这里，我们提出了从头开始的搜索树的修剪过程，从CNF和它的图形表示。当我们通过一个重要的例子来探索整个机制时，它很容易理解。我们还提出了一种新的概念，即在CNF中产生对称性破缺谓词，而不是从Crawford条件导出。最后，我们提出了一个回溯SAT求解器与内置SBP发生器。
2011-02-01 cs.AI math.CO
Restart Strategy Selection using Machine Learning Techniques
重启策略是影响冲突驱动的Davis Putnam风格SAT求解器性能的重要因素。为问题实例选择好的重新启动策略可以提高求解器的性能。受最近成功应用机器学习技术来预测SAT求解器的运行时间的启发，我们提出了一种方法，该方法使用机器学习通过智能选择重新启动策略来提高求解器的性能。基于易于计算的特征，我们训练可满足性分类器和运行时模型。我们使用这些模型来选择重启策略。我们目前的实验结果比较这种技术与最常用的重新启动策略。我们的研究结果表明，机器学习是有效的，在提高求解器的性能。
2009-07-29 cs.AI
A Dynamic Phase Selection Strategy for Satisfiability Solvers
Donghua University（东华大学）
相位选择是基于冲突驱动DPLL的SAT解算器的一个重要环节。本文提出了一种新的相位选择策略，其中每个文字的权重被定义为其隐含文字静态权重之和。在搜索过程中，每个文字的隐含文字是动态计算的。因此，它被称为动态相位选择策略。通常，动态计算权重是耗时的。因此，到目前为止，没有SAT求解器成功地应用动态相位选择。由于我们的策略的隐含文字符合搜索过程，通常的两个观察文字方案可以应用在这里。因此，我们的动态相位选择的成本非常低。为了改进在SAT 2011竞赛中获得应用类金奖的Glucose 2.0，我们使用动态相位选择策略构建了五个相位选择方案。在SAT 2011的应用实例中，通过动态相位选择改进的Glucose明显优于原始Glucose。我们还在Lingeling上进行了实验，使用动态相位选择策略，并建立了两个相位选择方案。实验结果表明，改进的Lingeling算法优于原Lingeling算法。
2012-08-08 cs.AI cs.LO
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Department of Computer Science, Purdue University, IN, USA（计算机科学系，普渡大学）
本文提出KOCO-SMC，一种集成的精确模计数可满足性求解器，通过跟踪上下界和部分变量赋值实现早期估计，显著提升求解效率。
2025-06-17 cs.AI 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
Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
University of Helsinki（赫尔辛基大学）；KU Leuven（库尔勒文大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本研究首次将VeriPB证明格式的证明日志应用于多目标MaxSAT，利用其预序关系实现Pareto最优性证明，实验证明该方法可在合理开销下具备可扩展性。
2025-01-29 cs.AI
Relating Complexity-theoretic Parameters with SAT Solver Performance
University of Waterloo（滑铁卢大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）；Microsoft Research（微软研究院）；University of Toronto（多伦多大学）
多年来，复杂性理论家提出了许多结构参数来解释冲突驱动子句学习（CDCL）SAT求解器在各种大型工业布尔实例上的惊人效率。虽然这些参数中的一些已经进行了实证研究，但到目前为止，还没有一个统一的比较研究，其解释力的综合基准。我们通过对近7000个工业和精心制作的公式进行大规模的CDCL SAT求解器性能实证评估来纠正这种状况，这些公式针对几个结构参数，如后门，树宽，骨干和社区结构。我们的研究导致了几个结果。首先，我们表明，虽然这些参数与CDCL求解时间只有弱相关性，但它们的某些组合会产生更好的回归模型。其次，我们展示了一些参数如何可以作为一个“镜头”，以更好地了解不同的解决算法的效率。最后，我们提出了一个新的复杂性理论参数，我们称之为学习敏感的重启（LSR）后门，扩展了学习敏感（LS）后门的概念，将重启和讨论算法来计算它们。我们从数学上证明，对于某些类别的情况下，最小LSR后门是指数小于最小LS后门。
2017-06-26 cs.AI
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
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
University of California, Berkeley（加利福尼亚大学伯克利分校）
针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。
2023-10-18 cs.AI cs.LO cs.PL
From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero
Purdue University（普渡大学）
尽管深度神经网络最近在图像和语音识别、自然语言处理和强化学习等各个领域取得了成功，但在将数值优化的力量引入符号推理方面，我们仍然面临着巨大的挑战。研究人员已经提出了不同的途径，例如用于证明合成的神经机器翻译，用于表示符号模式的符号和表达式的矢量化，以及用于降维的神经后端与用于决策的符号前端的耦合。然而，这些初步的探索仍然只是点的解决方案，并承担其他缺点，如缺乏正确性保证。在本文中，我们提出了将符号推理转换为游戏的方法，并在符号问题上直接利用Alpha（Go）Zero风格的深度强化学习的力量。使用布尔可满足性（SAT）问题作为展示，我们证明了我们的方法的可行性，以及模块化，效率和正确性保证的优点。
2018-02-14 cs.AI
MCP-Solver: Integrating Language Models with Constraint Programming Systems
TU Wien（维也纳技术大学）
MCP-Solver通过MCP协议将大型语言模型与符号求解器集成，提供Minizinc、PySAT和Python Z3接口，并采用编辑与迭代验证方法确保模型一致性，从而弥补LLMs在形式化求解与推理上的缺陷。
2025-04-06 cs.AI cs.CL cs.LG
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
INESC-ID（INESC-ID（葡萄牙系统与计算机工程研究所））；Instituto Superior Técnico（高等技术学院）；Universidade de Lisboa（里斯本大学）
在过去的十年中，已经提出了大量的单目标布尔优化算法，这些算法依赖于高效的命题可满足性（SAT）求解器的迭代使用。但是SAT求解器在多目标组合优化（MOCO）算法中的应用还很少。由于缺乏有效的MOCO工具，许多现实世界的应用程序制定为多目标简化为单目标，使用线性组合或字典排序的目标函数进行优化。在本文中，我们扩展了最先进的MOCO求解器与两个新的不可满足性为基础的算法。第一个是核心引导的MOCO求解器。第二个是基于命中集的MOCO求解器。在广泛的基准测试实例中获得的实验结果表明，我们的新的不可满足性为基础的算法可以优于最先进的SAT为基础的算法MOCO。
2022-04-22 cs.AI
SAT-based Analysis of Large Real-world Feature Models is Easy
University of Waterloo（滑铁卢大学）；Institute of Mathematical Sciences（数学科学研究所）
现代冲突驱动子句学习（CDCL）布尔SAT求解器提供了从汽车到操作系统的系统的真实世界特征模型（FM）的有效自动分析。众所周知，基于求解器的分析现实世界的FM规模非常好，即使从这样的FM获得的SAT实例是大的，并且相应的分析问题是NP完全的。为了更好地理解为什么SAT求解器如此有效，我们系统地研究了一组具有代表性的大型现实世界FM的许多句法和语义特征。我们发现，大型真实世界FM易于分析的一个关键原因是这些模型中的绝大多数变量都是不受限制的，即，对于在当前部分分配下对这些变量的真和假分配，模型都是可满足的。鉴于这一发现和我们对CDCL SAT求解器的理解，我们表明求解器可以很容易地为这些模型找到满意的分配，而不会有太多相对于模型大小的回溯，这解释了为什么求解器的规模如此之大。进一步的分析表明，在这些真实世界模型中存在不受限制的变量可以归因于它们的高度可变性。此外，我们还尝试了一系列众所周知的非回溯简化，这些简化在解决FM时特别有效。简化后剩下的变量/子句（称为核心）非常少，即使使用回溯也很容易解决，进一步加强了我们的结论。
2015-07-29 cs.AI cs.SE
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
SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
University of Waterloo（滑铁卢大学）；Wilfrid Laurier University（威尔弗里德·劳雷尔大学）
在过去的几十年里，许多不同的研究方向都致力于数学自动化，包括用于数学建模的计算机代数系统（CAS）、用于一阶逻辑的自动定理证明器、用于程序验证的SAT/SMT求解器以及用于检查数学证明的高阶证明助手。最近，其中一些研究领域开始以互补的方式融合在一起。一个成功的例子是SAT求解器和CAS（SAT+CAS）的结合，旨在解决数学问题。在纯数学和应用数学中的许多命题都不能用传统的证明方法来证明。相反，它们最好通过涉及非常大的组合搜索空间的计算方法来解决。SAT求解器是搜索如此大的组合空间的强大方法-因此，来自各种数学领域的许多问题都被简化为SAT，试图解决它们。然而，求解器传统上缺乏对修剪如此大的搜索空间至关重要的数学领域知识的深层存储库。相比之下，CAS是数学知识的深层存储库，但缺乏有效的通用搜索能力。通过将SAT的搜索能力与CAS中的深厚数学知识相结合，我们可以解决许多其他已知方法似乎无法解决的数学问题。我们展示了SAT+CAS范式的成功，突出了许多已被证伪，验证，或部分验证使用我们的工具MathCheck。这些成功表明，该范式将成为解决需要大量搜索和深度数学推理的问题的标准方法。例如，最近Heule、Kauers和Seidl使用SAT+CAS范式来寻找$3\times3$矩阵乘法的许多新算法。
2019-09-16 cs.AI cs.LO cs.SC
Learning to Rank the Initial Branching Order of SAT Solvers
KTH Royal Institute of Technology（皇家理工学院）；Kempner Institute at Harvard University（哈佛大学肯普纳研究所）；Mohamed Bin Zayed University of Artificial Intelligence（穆罕默德·本·扎耶德人工智能大学）
本文提出利用图神经网络预测SAT求解器初始分支顺序，以提升求解效率，但发现其在复杂实例上效果受限。
2026-03-07 cs.AI cs.LO
On Dedicated CDCL Strategies for PB Solvers
Univ. Artois（阿尔图瓦大学）；CNRS（法国国家科学研究中心）；Centre de Recherche en Informatique de Lens (CRIL)（朗斯计算机科学研究中心）；LIX, Laboratoire d’Informatique de l’X, Ecole Polytechnique（巴黎综合理工学院信息科学实验室（LIX））
目前的实现工作在本地PB约束的伪布尔（PB）求解器是基于CDCL架构，赋予高效的现代SAT求解器。特别是，这样的PB求解器不仅实现了（切割平面为基础的）冲突分析程序，但也补充战略的组件，是至关重要的效率的CDCL，即分支算法，学习约束删除和重新启动。然而，这些策略大多数被PB求解器重用，而不考虑它们处理的PB约束的特定形式。在本文中，我们提出并评估了不同的方式来适应CDCL策略，以考虑到PB约束的特殊性，同时保留他们在从句设置的行为。我们在两个不同的求解器中实现了这些策略，即Sat4j（我们考虑三种配置）和RoundingSat。我们的实验表明，这些专用的策略可以提高，有时显着，这些求解器的性能，无论是决策和优化问题。
2021-09-02 cs.AI
On SAT Models Enumeration in Itemset Mining
频繁项集挖掘是数据分析和数据采掘的重要组成部分。最近的作品提出了有趣的SAT为基础的编码发现频繁项集的问题。在这项工作中，我们的目标是定义适应SAT求解器，以提高模型枚举这样的编码策略。在此背景下，我们深入研究了重启、分支策略和小句学习的影响。然后，我们进行基于SAT的项集挖掘实例的实验评估，以显示如何SAT求解器可以适应，以获得一个有效的SAT模型枚举。
2015-06-08 cs.AI
On Improving the Backjump Level in PB Solvers
LIX (Laboratoire d’Informatique de l’X), École Polytechnique（巴黎综合理工学院计算机实验室（LIX），巴黎综合理工学院）
当前PB求解器实现了许多受现代SAT求解器的CDCL体系结构启发的技术，从而受益于其实际效率。然而，他们还需要处理这样一个事实，即当考虑PB约束时，这种架构所利用的许多属性不再为真。在本文中，我们专注于这些属性之一，即所谓的第一个唯一蕴涵点（1-UIP）的最优性。虽然这是众所周知的，学习冲突分析过程中产生的第一个断言子句，确保在SAT求解器中执行尽可能高的backjump，我们表明，在PB约束的存在下，没有这样的保证。我们还介绍和评估不同的方法，旨在提高backjump的水平，在冲突分析过程中确定，允许继续分析后，达到1-UIP。我们的实验表明，次优backjumps是相当常见的PB求解器，即使他们的影响求解器是不清楚的。
2021-07-27 cs.AI
Augmented Electronic Ising Machine as an Effective SAT Solver
University of Rochester（罗切斯特大学）
针对传统伊辛机求解3-SAT问题加速不足的问题，研究添加立方相互作用架构支持并提出语义感知退火调度，构建的AIMS求解器性能远超现有软硬件SAT求解器数个数量级，且抗器件偏差与噪声。
2023-05-01 cs.AI cs.AR cs.ET
A high-performance analog Max-SAT solver and its application to Ramsey numbers
Babeş-Bolyai University（巴比什-波雅依大学）；Romanian Institute of Science and Technology（罗马尼亚科学技术研究所）；University of Notre Dame（圣母大学）；The College of Wooster（伍斯特学院）；Transylvanian Institute of Neuroscience（特兰西瓦尼亚神经科学研究所）
我们介绍了一个连续时间模拟求解器MaxSAT，一个典型的NP-难离散优化问题，其中的任务是找到一组布尔变量满足给定的逻辑约束的最大数量的真值分配。我们表明，缩放的不变量的求解器的动态，逃逸率，作为不满意的条款的数量的函数可以预测的全局最优值，往往在达到相应的状态。我们证明了求解器在硬MaxSAT竞争问题上的性能。然后，我们考虑双色拉姆齐数$R(m,m)$问题，将其转化为SAT，并将我们的算法应用于仍然未知的$R(5,5)$。我们发现边着色没有单色5-团的完全图高达42个顶点，而在43个顶点，我们发现着色只有两个单色5-团，迄今为止发现的最好的着色，支持猜想，$R(5,5) = 43$。
2018-01-28 cond-mat.stat-mech cs.AI cs.CC
Building a Truly Distributed Constraint Solver with JADE
The Robert Gordon University（罗伯特戈登大学）
现实生活中的问题，如调度会议之间的人在不同的位置可以建模为分布式约束满足问题（CSP）。然后可以使用约束满足算法找到合适的和满意的解决方案，该算法可以是穷举的（回溯）或其他的（局部搜索）。然而，在这一领域的大多数研究测试他们的算法模拟在一台PC上，一个单一的程序入口点。我们的工作的主要贡献是设计和实现了一个真正的分布式约束求解器的基础上，使用Java代理DEFERMEMENT框架（JADE）的本地搜索算法，使不同机器上的代理之间的通信。特别是，我们讨论了真正的分布式约束求解器，这可能不是关键时，在一台机器上模拟的设计和实现问题。评估结果表明，我们真正的分布式约束求解器的工作以及在所观察到的限制，当测试与各种分布式CSP。我们的应用程序也可以采用任何约束求解算法，只需很少的修改。
2015-09-03 cs.AI cs.DC
