Streamlined Constraint Reasoning via CNN Pattern Recognition on Enumerated Solutions
本文提出了一种新的方法，通过枚举可行解并训练卷积神经网络来识别结构模式，从而生成MiniZinc约束流式器，以提高约束编程中硬问题的求解效率。
2026-05-19 cs.AI
Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination
Aalto University（阿尔托大学）
我们介绍了新的方法编码的无环性和s-t-可达性约束的命题公式与底层有向图。它们基于顶点消除图，这使得它们适用于底层图稀疏的情况。与求解器与ad hoc约束传播的非循环性和可达性约束，如GraphSAT，我们的方法编码这些约束作为标准的命题子句，使它们直接适用于任何SAT求解器。一项实证研究表明，我们的方法与一个有效的SAT求解器可以优于这些约束的早期编码以及GraphSAT，特别是当底层图形稀疏。
2021-05-27 cs.AI
Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts (Extended Version)
University of Amsterdam, Institute for Logic Language and Computation（阿姆斯特丹大学，逻辑语言与计算研究所）；Aalborg University（奥尔堡大学）
研究如何将因子化任务编码为SAT问题，提出多种编码策略，并分析并行性和任务转换对SAT规划器性能的影响。
2026-05-28 cs.AI
Encoding Cryptographic Functions to SAT Using Transalg System
Matrosov Institute for System Dynamics and Control Theory of SB RAS（马特罗索夫系统动力学与控制理论研究所（SB RAS））
本文提出了构造离散函数命题编码的技术。它的目的是使用最先进的SAT求解器解决所考虑函数的求逆问题。我们以名为Transalg的软件系统的形式实现了这项技术，并使用它来构建SAT编码，以解决许多密码分析问题。通过将SAT求解器应用于这些编码，我们成功地反转了几个加密函数。特别是，我们使用了由Transalg产生的SAT编码来构建两块MD5冲突的族，其中前10个字节为零。此外，我们使用Transalg编码的广泛知名的A5/1密钥流生成器，解决了几十个密码分析实例中的分布式计算环境。在本文中，我们详细比较了Transalg与类似软件系统的功能。
2016-07-04 cs.AI cs.CR
On SAT Models Enumeration in Itemset Mining
频繁项集挖掘是数据分析和数据采掘的重要组成部分。最近的作品提出了有趣的SAT为基础的编码发现频繁项集的问题。在这项工作中，我们的目标是定义适应SAT求解器，以提高模型枚举这样的编码策略。在此背景下，我们深入研究了重启、分支策略和小句学习的影响。然后，我们进行基于SAT的项集挖掘实例的实验评估，以显示如何SAT求解器可以适应，以获得一个有效的SAT模型枚举。
2015-06-08 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
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
Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming
University of Kobe（神户大学）；University of Potsdam（波茨坦大学）；National Institute of Informatics（国立信息学研究所）；Simon Fraser University（西蒙弗雷泽大学）；Griffith University（格里菲斯大学）
将有限线性CSP编码为布尔公式并使用现代SAT求解器求解它们已被证明是非常有效的，获奖的糖系统就是一个例子。我们在这里开发了一种基于ASP的替代方法。这使我们能够使用一阶编码，为我们提供了高度的灵活性，便于不同实现的实验。由此产生的系统Escherame重新使用部分糖来解析和规范化CSP。然后将获得的事实集与ASP编码相结合，该编码可以由现成的ASP系统进行接地和解决。我们建立我们的方法的竞争力，通过经验对比甜和糖。
2013-12-20 cs.AI
Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
University of York（约克大学）
针对SAT编码选择难题，该研究用监督机器学习方法为伪布尔和线性约束选编码，设计专用特征集提升性能，在未见问题类和与AutoFolio对比中均表现良好。
2023-11-08 cs.AI cs.LG cs.LO
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
Extending Modern SAT Solvers for Enumerating All Models
本文讨论了在合取范式（CNF）中枚举布尔公式的所有模型的问题。我们提出了一个扩展的CDCL为基础的SAT求解器来处理这个基本问题。然后，我们提供了一个实验评估，我们提出的SAT模型枚举算法，从最后的SAT挑战，并从基于SAT的编码的序列挖掘问题的实例上的可满足的SAT实例。
2013-05-06 cs.AI
Generalized Totalizer Encoding for Pseudo-Boolean Constraints
Department of Computer Science, University of Oxford（牛津大学计算机科学系）；INESC-ID / Instituto Superior Técnico, Universidade de Lisboa（里斯本大学高等技术学院/INESC-ID（里斯本大学工程与计算机科学研究所））
伪布尔约束，也称为0-1线性约束，用于模拟许多现实世界的问题。解决这些约束的常见方法是将它们编码为SAT公式。SAT求解器在这样的公式上的运行时间对给定的伪布尔约束的编码方式敏感。在本文中，我们提出了广义累加器编码（GTE），这是一个弧一致性保持扩展的累加器编码伪布尔约束。与其他一些编码不同，GTE所需的辅助变量的数量不依赖于系数的大小。相反，它取决于这些系数的不同组合的数量。我们展示了GTE相对于其他编码的优越性时，大的伪布尔约束有低数量的不同的系数。我们的实验结果还表明，GTE仍然具有竞争力，即使伪布尔约束不具有这一特点。
2015-07-21 cs.AI cs.LO
Structure-Aware Encodings of Argumentation Properties for Clique-width
Data Science Group, Heinz Nixdorf Institute, Paderborn University（数据科学组、海因茨·尼克斯多夫研究所、帕德博恩大学）；CNRS, UMR 8188, Centre de Recherche en Informatique de Lens (CRIL), University of Artois（法国国家科学研究中心、UMR 8188、棱镜信息研究中心（CRIL）、阿鲁瓦大学）；Department of Computer and Information Science, Linköping University（利厄普堡大学计算机与信息科学系）
针对团块宽度编码研究空白，通过抽象论证框架设计线性保留团块宽度的有向分解引导归约至（Q）SAT，为所有论证语义（含计数）建立新结果，揭示编码开销下限。
2025-11-13 cs.AI cs.CC
Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
Amherst College（阿默斯特学院）
本研究通过在自研生成的多难度25x25大规模数独谜题上测试，对比了Z3、CVC5等现代SMT求解器与经典SAT求解器的性能，证实SMT求解器表现更优，展现了其在大规模约束满足问题中的应用价值。
2025-01-15 cs.AI cs.LO
Depth-Optimal Quantum Layout Synthesis as SAT
Department of Computer Science, Aarhus University, Denmark（丹麦阿arhus大学计算机科学系）；Kvantify Aps, DK-2300 Copenhagen S, Denmark（丹麦Kvantify公司）
提出一种面向量子电路布局综合的 SAT 编码，利用增量求解与并行方案实现电路深度或 CX 深度最优，并通过实验比较 OLSQ2、Q-Synth 及噪声表现。
2025-06-07 cs.AI quant-ph
On When and How to use SAT to Mine Frequent Itemsets
INESC-ID（葡萄牙系统与计算机工程研究所）；IST（高等技术学院）；Technical University of Lisbon（里斯本技术大学）
在过去的十年中，一个新的研究流诞生了，其目标是使用约束编程（CP）挖掘感兴趣的项集。这促进了以高度灵活的方式组合复杂约束的自然方式。虽然CP国家的最先进的解决方案制定的任务使用布尔变量，少数尝试采用命题可满足性（SAT）提供了一个不满意的性能。本文通过定义不同的编码方式和多个任务驱动的枚举选项以及搜索策略，深入研究了在频繁项集挖掘问题中何时以及如何使用SAT。虽然对于大多数情况下，基于SAT的解决方案似乎是非竞争性的CP同行，结果显示了各种有趣的情况下，SAT编码是最好的选择。
2012-07-26 cs.AI cs.DB cs.LG
On the Tour Towards DPLL(MAPF) and Beyond
Czech Technical University in Prague（布拉格捷克理工大学）
我们讨论了里程碑之旅对DPLL（MAPF），多智能体路径寻找（MAPF）求解器完全集成的戴维斯-普特南-洛格曼-洛夫兰（DPLL）命题可满足性测试算法通过可满足性模理论（SMT）。MAPF的任务是在无向图中以无冲突的方式导航代理，以便每个代理最终到达其唯一的目标顶点。一次最多只能有一个代理驻留在一个顶点中。代理可以通过遍历边来瞬间移动，只要移动不会导致碰撞。最近试图解决MAPF最佳w.r.t.基于MAPF到命题可满足性（SAT）约简的费用和或完工时间已经出现。最成功的方法依赖于通过SMT范例中启发的过程为给定的MAPF实例惰性地构建命题编码。然而，在现有的方法中，SAT求解器和编码的高级构造的可满足性测试的集成相对松散。因此，该方向研究的最终目标是构建DPLL（MAPF）算法，这是一种MAPF求解器，其中编码的构建与底层SAT求解器完全集成。我们讨论了当前最先进的MAPF解决方案和需要做什么步骤，以获得DPLL（MAPF）。DPLL（MAPF）的优点，在其潜在的交替参数化与MAPF $^R$，一个理论的连续MAPF的几何代理，也进行了讨论。
2019-07-11 cs.AI cs.MA
Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints
Rice University（莱斯大学）
针对量子计算中边着色图的受约束完美匹配问题，提出基于Tutte定理与优化技术的新型混合布尔约束编码，实验证明其扩展性显著优于竞争方法，凸显了设计特定问题编码的必要性。
2023-05-18 cs.AI cs.LO math.CO
Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat
CUNY Brooklyn College & Graduate Center（纽约市立大学布鲁克林学院及研究生中心）
许多约束满足问题涉及合成满足某些可达性约束的子图。本文介绍了四个问题，从最近的LP/CP编程比赛中选择的Picat程序。这些程序展示了Picat语言的建模能力和具有有效编码的尖端SAT求解器的求解效率。
2021-09-17 cs.AI cs.PL
On Explaining Random Forests with SAT
ANITI（图卢兹人工智能与自然智能研究所）；Univ. Toulouse（图卢兹大学）；IRIT（图卢兹信息学研究所）；CNRS（法国国家科学研究中心）
随机森林（Random Forest，RF）是最广泛使用的机器学习（Machine Learning，ML）分类器之一。即使RF是不可解释的，也没有专门的非启发式方法来计算RF的解释。此外，最近有关于解释ML模型的多项式算法的工作，包括朴素贝叶斯分类器。因此，一个问题是找到RF的解释是否可以在多项式时间内解决。本文否定地回答了这个问题，证明了计算RF的一个PI解释是D^P-完全的。此外，本文提出了一个命题编码计算RF的解释，从而使寻找PI解释与SAT求解器。这与早期解释提升树（BT）和神经网络（NN）的工作形成对比，后者需要基于SMT/MILP的编码。实验结果表明，在广泛的公开数据集上获得的，所提出的基于SAT的方法扩展到实际应用中常见的大小的RF。也许更重要的是，实验结果表明，对于绝大多数的例子，本文提出的基于SAT的方法显着优于现有的启发式方法。
2021-05-21 cs.AI cs.LG
Fuzzy Maximum Satisfiability
Cairo University（开罗大学）；Faculty of Science（理学院）；Department of Mathematics（数学系）
在本文中，我们扩展的最大可满足性（MaxSAT）的问题，Eukasiewicz逻辑。一组公式Φ的最大SAT问题是找到满足最大公式数的Φ中变量的分配问题。提出了三种可能的解决方案（编码）：（1）析取线性关系（DLRs），（2）混合线性规划（MILP）和（3）加权约束满足问题（WCSP）。像它的布尔对应，扩展的模糊MaxSAT将在优化问题中，涉及的最优性有许多应用。
2016-02-06 cs.AI cs.CC cs.LO
Learning a SAT Solver from Single-Bit Supervision
Stanford University（斯坦福大学）；Microsoft Research（微软研究院）
我们提出了NeuroSAT，一个消息传递神经网络，学习解决SAT问题后，只被训练为一个分类器，以预测可满足性。虽然它与最先进的SAT求解器没有竞争力，但NeuroSAT可以通过简单地运行更多的迭代来解决比训练过程中看到的更大、更困难的问题。此外，NeuroSAT还可以推广到新的分布;在仅对随机SAT问题进行训练后，在测试时，它可以解决SAT问题编码图着色，团检测，支配集和顶点覆盖问题，所有这些都是在小随机图上的分布范围内。
2019-03-12 cs.AI cs.LG cs.LO
SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints
Universitat de Girona（赫罗纳大学）；Aix Marseille Univ（艾克斯-马赛大学）；Université de Toulon（土伦大学）；University of York（约克大学）
在用命题可满足性（SAT）求解组合问题时，问题的编码是至关重要的。我们研究编码的伪布尔（PB）约束，一种常见的算术约束，出现在各种各样的组合问题，如排序，调度，和资源分配。在某些情况下，PB约束在其变量的子集上与至多一个（AMO）约束一起出现（形成PB（AMO）约束）。最近的工作表明，在使用决策图对PB约束进行编码时考虑AMOs可以显著提高求解器的效率。在本文中，我们扩展到其他国家的最先进的PB约束编码的方法，开发了几个新的PB（AMO）约束编码。此外，我们提出了一个更紧凑和有效的版本的流行的广义累加器编码，命名为减少广义累加器。这种新的编码也适用于PB（AMO）约束，以获得进一步的增益。我们的实验表明，PB（AMO）约束的编码可以大大小于PB约束。PB（AMO）编码允许在一定时间内解决更多的实例，并且在某些情况下，解决时间可以提高一个数量级以上。我们还观察到，在所考虑的编码中不存在单个总冠军，但是每个编码的效率可以取决于PB（AMO）特性，诸如系数值的幅度。
2021-10-15 cs.AI
Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning
研究单常数乘法问题的高效SAT编码，提出神经符号框架，用图神经网络预测运算符类型，利用置信分数修剪搜索选择，实验表明该方法能大幅提升编码的可扩展性与效率，减少时间、内存及分支。
2026-07-24 cs.AI
Towards Numerical TOHTN Planning with SMT-based HTN-SAT Encoding
Univ. Grenoble Alpes（格勒诺布尔大学）
本文针对HTN规划数值推理支持不足的问题，研究数值TOHTN规划，将SAT编码扩展结合SMT处理数值流，引入基准套件，实验表明该编码可作为有竞争力的基线，为更优HTN规划方法铺路。
2026-09-04 cs.AI
Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT
Matrosov Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences（俄罗斯科学院西伯利亚分院马特罗索夫系统动力学与控制论研究所）
在本文中，我们提出了Transalg系统，旨在产生SAT编码的离散函数，作为一个特定的语言编写的程序。将这些程序翻译成SAT是基于形式计算模型的命题编码方法和符号执行的概念。我们使用Transalg系统为许多加密函数进行SAT编码。
2015-10-29 cs.AI
Yet Another Comparison of SAT Encodings for the At-Most-K Constraint
CUNY Brooklyn College & Graduate Center（纽约市立大学布鲁克林学院与研究生中心）
至多k约束在组合问题中是普遍存在的，并且许多SAT编码可用于该约束。先前的实验已经示出了对于k $>$ 1的顺序计数器编码的竞争性，并且已经将比二进制加法器编码更紧凑的并行计数器编码排除在考虑之外，因为其不能通过单元传播来实施弧一致性。本文提出了一个实验，显示惊人的性能的二进制加法器编码的最多k约束。
2020-05-12 cs.AI cs.LO
Solving the Course-timetabling Problem of Cairo University Using Max-SAT
Cairo University（开罗大学）
由于现有的SAT（satisfiability）和Max-SAT（maximum satisfiability）求解器具有良好的性能，许多实际的优化问题如调度问题都可以通过将其编码成Max-SAT来求解。在本文中，我们解决了开罗大学数学系的课程编排问题，编码成Max-SAT。手工生成部门的时间表已被证明是繁琐的，生成的时间表几乎总是包含冲突。我们展示了如何约束可以建模为一个最大SAT实例。
2018-02-11 cs.AI
DES: a Challenge Problem for Nonmonotonic Reasoning Systems
美国的数据加密标准（DES）被提出作为非单调推理系统的一个有趣的基准问题，因为（i）它提供了一组工业相关的测试用例，这些测试用例具有随机生成问题和真实世界问题的特征，（ii）DES使用具有稳定模型语义的正常逻辑程序的表示简单且易于理解，和（iii）这个逻辑程序子类可以被看作是非单调推理的许多其他形式化的有趣的特殊情况。本文提出了DES作为逻辑程序的两种编码：一种是标准规范外的直接编码，另一种是扩展Massacci和Marraro工作的优化编码。利用Smodels系统作为稳定模型语义的实现，研究了编码的计算特性，并将其用于DES密钥搜索。结果表明，编码和S模型是相当有竞争力的：他们优于国家的最先进的SAT检查器与DES到SAT的优化编码工作，并与SAT检查器，是定制和优化的SAT编码调整。
2000-03-08 cs.AI
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
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
在过去的二十年中，模态和描述逻辑已被应用于计算机科学的许多领域，包括知识表示，形式化验证，数据库理论，分布式计算，以及最近的语义Web和本体。基于这个原因，模态逻辑和描述逻辑中的自动推理问题得到了深入的研究。特别地，已经提出了许多方法来有效地处理核心正规模态逻辑K（m）及其记法变体描述逻辑ALC的可满足性。虽然K（m）/ALC结构简单，但在计算上很难推理，它的可满足性是PSPACE完全的。在本文中，我们开始探索的想法，执行自动推理任务的模态和描述逻辑编码成SAT，以便处理的国家的最先进的SAT工具，与大多数以前的方法，我们开始我们的调查从满足性K（m）。我们提出了一个有效的编码，我们测试了一组广泛的基准，比较的方法与主要的国家的最先进的工具。虽然编码必然是最坏情况下的指数，从我们的实验中，我们注意到，在实践中，这种方法可以处理大多数或所有的问题，这是在其他方法的范围内，与性能相当，甚至更好，那些目前的国家的最先进的工具。
2014-01-15 cs.AI cs.LO
Efficient Encodings of Conditional Cardinality Constraints
CRIL-CNRS UMR 8188, Université d’Artois（法国国家科学研究中心联合研究单位8188-里尔信息学研究中心，阿尔图瓦大学）；SAMOVAR, Télécom SudParis, CNRS, Univ. Paris-Saclay（萨莫瓦尔实验室，南巴黎电信学院，法国国家科学研究中心，巴黎萨克雷大学）
在许多现实问题的命题可满足性编码中，基数约束是一个需要有效管理的递归约束。已经提出了几种有效的编码，但缺少这样的约束可以涉及到一个更一般的命题制定。为了避免组合爆炸，常用于将一般命题公式转化为合取范式（CNF）的Tseitin原理引入新的命题变量来表示子公式和/或复约束。由于Plaisted和Greenbaum的改进，考虑了子公式$Φ$的极性，导致形式为$y\rightarrow Φ$或$Φ\rightarrow y$的条件约束，其中$y$是新的命题变量。在$Φ$表示基数约束的情况下，这样的转换导致本论文的主题的条件基数约束。我们首先表明，当所有的条款编码的基数约束增加了一个额外的新变量，大多数著名的编码停止维护广义弧一致性属性。然后，我们考虑其中的一些编码，并展示如何扩展它们以恢复如此重要的属性。一个基于SAT的模式挖掘应用程序，这样的条件基数约束是一个基石，显示我们所提出的方法的相关性进行了实验验证。
2018-03-31 cs.AI
A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
CRIL；CNRS（法国国家科学研究中心）；Univ Artois（阿尔图瓦大学）
将伪布尔（PB）约束编码到SAT中时的两个主要考虑因素是编码的大小及其传播强度，即，保证其在单位传播下具有良好的行为。几种具有传播强度保证的编码依赖于约束到DNNF（可分解否定范式）、BDD（二进制决策图）或一些其他子变体的先前编译。然而，已经表明存在PB约束，其有序BDD（OBDD）表示以及因此推断的CNF编码都具有指数大小。由于DNNF比OBDD更简洁，因此更喜欢通过DNNF进行编码以避免大小爆炸似乎是一个合理的选择。然而，在本文中，我们证明了PB约束的存在性，其DNF都需要指数大小。
2021-01-06 cs.AI
When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)
本文提出一种部分 grounding 的 SAT 编码，在保持动作 lifted 的同时部分 grounding 预言，实现线性规模的规划效率，优于现有方法。
2026-03-19 cs.AI cs.LO cs.SC
Extracting Problem Structure with LLMs for Optimized SAT Local Search
TU Wien（维也纳技术大学）
本文提出利用大语言模型分析Python编码代码以提取SAT问题隐藏结构，并自动生成专用局部搜索算法来构造强初始赋值，从而加速CDCL求解器。
2025-02-04 cs.AI
Bayesian network learning by compiling to weighted MAX-SAT
University of York（约克大学）；York Centre for Complex Systems Analysis（约克复杂系统分析中心）；Department of Computer Science（计算机科学系）
从数据中学习离散贝叶斯网络的问题被编码为加权MAX-SAT问题，MaxWalkSat局部搜索算法用于解决它。对于每个数据集，在应用MaxWalkSat之前，计算不同父母选择（“家庭分数”）的（BDeu）边际似然的每个变量的和。每个变量的父母的每一个允许的选择被编码为一个不同的命题原子和相关的家庭得分编码为一个“软”加权单文字子句。两种方法来执行无环性被认为是：无论是通过编码的祖先关系，或通过附加一个总的顺序，每个图和编码。后一种方法效果更好。学习实验已经进行了21个合成数据集从7 BN采样。最大的数据集有10，000个数据点和60个变量，产生（对于“祖先”编码）具有19，932个原子和269，367个子句的加权CNF输入文件。对于大多数数据集，MaxWalkSat可以快速找到BDeu分数高于“真实”BN的BN。评估了添加先验信息的效果。它进一步表明，贝叶斯模型平均可以通过收集搜索过程中产生的BN的影响。
2012-06-13 cs.AI
Formally Verified SAT-Based AI Planning
我们提出了一个可执行的正式验证SAT编码的经典AI规划。我们使用定理证明器Isabelle/HOL进行验证。我们实验测试验证编码，并表明它可以用于合理大小的标准规划基准。我们还使用它作为参考来测试最先进的基于SAT的规划器，表明它有时会错误地声称问题没有一定长度的解决方案。
2023-03-07 cs.AI cs.LO
SAT Encoding of Partial Ordering Models for Graph Coloring Problems
Department of Computer Science, University of Bonn（波恩大学计算机科学系）；Adesso SE（Adesso公司）
该研究提出图着色问题与带宽着色问题的基于偏序的新型SAT编码，经理论与实验验证，该编码在稀疏图和部分基准实例上性能优于现有最优方法，还首次求解了多个带宽着色问题的公开未解决实例。
2024-08-14 cs.AI cs.DM cs.DS
Exploiting Structure in Weighted Model Counting Approaches to Probabilistic Inference
Autodesk Canada（欧特克加拿大公司）；University of Waterloo（滑铁卢大学）
以往的研究表明，将贝叶斯网络编码成SAT公式，然后使用回溯搜索算法进行加权模型计数可以是精确推理的有效方法。在本文中，我们提出了改进这种方法的贝叶斯网络与噪声或噪声最大的关系-两个关系，在实践中被广泛使用，因为它们可以显着减少的概率需要指定的数量。特别是，我们提出了两个SAT编码的噪声或和两个编码的噪声最大值，利用结构或语义的关系，以提高时间和空间效率，我们证明了编码的正确性。我们在大规模真实和随机生成的贝叶斯网络上对我们的技术进行了实验评估。在这些基准测试中，我们的技术对于具有噪声OR/MAX关系的网络和扩展到更大的网络的最佳先前方法的加速高达两个数量级。此外，我们的技术扩展了加权模型计数方法，用于精确推断以前难以处理的网络。
2014-01-16 cs.AI
Classical Planning as QBF without Grounding (extended version)
Aarhus University, Department of Computer Science（奥胡斯大学计算机科学系）
大多数经典规划器使用基础作为预处理步骤，本质上将规划简化为命题逻辑。然而，接地涉及到实例化所有的动作规则与具体的对象组合，并导致大的编码SAT/QBF为基础的规划。当行动具有许多参数时，这种严重的内存成本成为主要瓶颈，例如IPC 2018竞赛中的有机合成问题。我们提供了一个紧凑的QBF编码，是对数的对象的数量，并完全避免接地，通过使用对象组合的通用量化。我们表明，我们可以解决一些有机合成的问题，这是不能处理之前的任何SAT/QBF为基础的计划，由于接地。
2021-12-18 cs.AI
Transformation-based Feature Computation for Algorithm Portfolios
Insight Centre for Data Analytics（洞察数据分析中心）；University College Cork（科克大学学院）；Oracle America Inc.（甲骨文美国公司）
实例特定的算法配置和算法组合已被证明在各种应用领域中提供比单一算法方法显著的改进。在SAT和CSP领域，算法组合在过去五年中一直主导着这些领域的主要竞争。要使组合办法有效，必须满足两个关键条件。首先，需要一组互补的求解器来制作投资组合。其次，必须有一个问题特征的集合，可以准确地识别实例之间的结构差异。本文重点讨论后一个问题：特征表示，因为，与SAT不同，不是每个问题都有很好的研究特征。我们采用著名的SATzilla功能集，但计算不同的SAT编码的CSP的替代集。我们表明，无论使用什么编码转换的实例，保持足够的结构信息，以区分问题的实例，这可以被利用，使一个有效的投资组合为基础的CSP求解器。
2014-01-10 cs.AI
Heuristically Guided Compilation for Multi-Agent Path Finding
Czech Technical University in Prague（布拉格捷克理工大学）；Faculty of Information Technology（信息技术学院）
多智能体路径寻找（MAPF）是在共享环境中寻找连接智能体指定初始位置和目标位置的非冲突路径的任务。我们专注于基于编译的求解器，其中的MAPF问题表示在不同的良好建立的形式主义，如混合整数线性规划（MILP），布尔可满足性（SAT），或约束规划（CP）。由于这些形式主义的目标求解器充当黑盒，因此在基于MAPF编译的求解器中集成MAPF特定算法是具有挑战性的。在这项工作中，我们将展示如何建立一个MAPF编码的目标SAT求解器，在特定领域的启发式知识得到反映。通过为每个代理选择候选路径并仅为这些候选路径构建编码而不是为代理的所有可能路径构建编码，将启发式知识转移到SAT求解器。进行的实验表明，启发式指导编译优于基于SAT的MAPF求解器的香草变种。
2022-12-13 cs.AI cs.MA
A New Look at BDDs for Pseudo-Boolean Constraints
Technical University of Catalonia (UPC)（加泰罗尼亚理工大学）
伪布尔约束在实际应用中是无处不在的，因此一直致力于发展良好的SAT编码技术。这些编码中的一些首先构造约束的二元决策图（BDD），然后将BDD编码成命题公式。这些基于BDD的方法具有一些重要的优点，例如不依赖于系数的大小，或者能够共享相同的BDD来表示许多约束。我们首先关注所产生的BDD的大小，这被认为是我们研究界的一个公开问题。我们报告以前的工作，它被证明是伪布尔约束，没有多项式BDD存在。我们还给出了一个替代和更简单的证明假设NP是不同的Co-NP。更有趣的是，这里我们还展示了如何通过phcoefficient分解来克服BDD可能的指数爆破。这使我们能够给出第一个多项式广义弧一致的ROBDD编码的伪布尔约束。最后，我们专注于实际问题：我们展示了如何有效地构建这样的ROBDD，如何将它们编码成SAT，每个节点只有2个子句，并提出了实验结果，证实了我们的方法与其他编码和最先进的伪布尔解算器具有竞争力。
2014-01-23 cs.AI
Lossy source encoding via message-passing and decimation over generalized codewords of LDGM codes
我们描述了使用低密度生成矩阵（LDGM）码的有损信源编码的消息传递和抽取方法。特别是，本文解决了编码伯努利（0.5）源的问题：随机生成的LDGM码与适当的不规则度分布，我们的方法产生的性能非常接近率失真限制在一定范围内的速率。我们的方法的灵感来自调查传播（SP）算法，最初开发的Mezard等人。解决随机可满足性问题。Maneva等人先前的工作展示了如何将SP理解为可满足性问题的另一种表示的置信传播（BP）。类似于这种连接，我们的方法是定义一个家庭的马尔可夫随机场广义码字，从本地消息传递规则可以得出标准的方式。整个信源编码方法基于消息传递，将比特子集设置为它们的首选值（抽取），并减少代码。
2005-08-15 cs.AI cs.IT math.IT
CNOT-Optimal Clifford Synthesis as SAT
Department of Computer Science, Aarhus University（奥胡斯大学计算机科学系）；Kvantify Aps（Kvantify Aps公司）
本文提出将Clifford范式搜索纳入SAT编码以保证CNOT数量最优，并扩展至优化CNOT深度及处理硬件连接限制，在多项基准测试中显著优于现有SAT方法及主流编译器。
2025-04-01 cs.AI quant-ph
Learning with Logical Constraints but without Shortcut Satisfaction
State Key Lab of Novel Software Technology, Nanjing University（南京大学计算机软件新技术国家重点实验室）；The University of Hong Kong（香港大学）；Birkbeck, University of London（伦敦大学伯克贝克学院）
针对神经符号学习中逻辑约束被捷径空洞满足的问题，本文提出引入逻辑连接词对偶变量并构建兼容原始损失的变分分布式损失框架，提升了泛化能力与约束满足效果。
2024-03-01 cs.AI cs.LG
LinSATNet: The Positive Linear Satisfiability Neural Networks
Shanghai Jiao Tong University（上海交通大学）；Shanghai AI Laboratory（上海人工智能实验室）
本文提出基于扩展Sinkhorn算法的可微可满足性层，实现一次性神经网络求解约束问题，涵盖路由、图匹配和金融组合，无需最优解监督。
2024-07-18 cs.AI math.OC
Exact ASP Counting with Compact Encodings
National University of Singapore（新加坡国立大学）；Indian Institute of Technology Bombay（印度理工学院孟买分校）；University of Toronto（多伦多大学）
针对现有精确ASP计数器难以处理大规模输入、可扩展性差的问题，本文提出sharpASP框架，通过替代答案集定义迁移命题模型计数关键技术，在1470个基准上实现了显著性能提升。
2023-12-19 cs.AI cs.LO
Streamliners for Answer Set Programming
University of Klagenfurt（克雷格富特大学）
本文将StreamLLM方法应用于答案集编程，通过生成约束减少搜索空间，实验表明在三个基准测试中，虚拟最佳编码在速度上提升了4-5倍。
2026-07-24 cs.AI cs.LO
