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 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
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
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
Extending Modern SAT Solvers for Enumerating All Models
本文讨论了在合取范式（CNF）中枚举布尔公式的所有模型的问题。我们提出了一个扩展的CDCL为基础的SAT求解器来处理这个基本问题。然后，我们提供了一个实验评估，我们提出的SAT模型枚举算法，从最后的SAT挑战，并从基于SAT的编码的序列挖掘问题的实例上的可满足的SAT实例。
2013-05-06 cs.AI
Extending SMT Solving with Non-Ground Clause Learning
Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）；Graduate School of Computer Science, Saarland Informatics Campus（萨尔兰信息学园区计算机科学研究生院）
本文提出一种结合基实例化、CDCL(T)风格规则与非基冲突分析的演算，通过非基子句学习生成更一般的子句，并支持时间回溯，可模拟多种SMT求解方法。
2026-09-11 cs.AI cs.LO
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
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
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
Driving CDCL Search
Università della Calabria（卡拉布里亚大学）；Alpen-Adria-Universität Klagenfurt（克拉根福阿尔卑斯-亚得里亚大学）
CDCL算法是最先进的SAT、SMT、ASP等求解器采用的领先解决方案。实验表明，嵌入特定领域的算法可以显着提高CDCL求解器的性能，特别是在大型现实世界的问题。然而，在现成的CDCL实现中适当地集成这样的标准并不明显。在本文中，我们提取的关键成分，驱动搜索的CDCL求解器，并提出了一个通用的框架，设计和实施新的算法。我们在ASP求解器中实现了我们的策略，并在两个工业领域进行了实验。在困难的问题实例中，最先进的实现无法在可接受的时间内找到任何解决方案，而我们的实现非常成功，可以找到所有解决方案。
2016-11-16 cs.AI
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
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
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
IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses
Hamburg University of Technology (TUHH)（汉堡工业大学（TUHH））
本文提出IGMaxHS，一种支持XOR约束的增量MaxSAT求解器，通过高斯消元与接口扩展实现量子纠错所需的求解能力，并在模糊测试中表现最优，可解码量子颜色码。
2024-10-21 cs.AI
AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
Fudan University（复旦大学）；paradigm Inc.（第四范式公司）；Tsinghua University（清华大学）
本文提出 AutoSAT 框架，利用大型语言模型在模块化搜索空间中自动优化 CDCL SAT 求解器的启发式方法，实验证明其能提升求解器性能，并在多个数据集上超越 MiniSat 和 Kissat。
2024-11-13 cs.AI
Automation of Triangle Ruler-and-Compass Constructions Using Constraint Solvers
Faculty of Mathematics, University of Belgrade（贝尔格莱德大学数学学院）
本文提出用 MiniZinc 有限域约束求解器自动求解三角形尺规作图问题，在 74 个 Wernick 问题上与 ArgoTriCS 对比，证明其实现更省力且常能找到更短作图过程。
2024-01-22 cs.AI
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
Machine Learning for SAT: Restricted Heuristics and New Graph Representations
St. Petersburg State University（圣彼得堡国立大学）；Steklov Institute of Mathematics at St. Petersburg（圣彼得堡斯捷克洛夫数学研究所）
针对机器学习改进SAT求解启发式时存在的运行慢问题，提出先用ML模型执行初始步再交回控制权的策略，还改进了适配跨领域SAT的Graph-Q-SAT，经随机和工业算例验证可行。
2023-07-18 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
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
Concurrent Cube-and-Conquer
Delft University of Technology（代尔夫特理工大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）；Johannes Kepler University Linz（约翰内斯·开普勒大学林茨分校）
最近的工作介绍了立方体和征服的技术来解决硬SAT的情况下。它使用前瞻求解器将搜索空间划分为立方体。每个立方体处理的冲突驱动的条款学习（CDCL）解决方案。对于强大的性能至关重要的是决定何时从前瞻切换到CDCL的截止启发式。然而，这种离线启发式方法远非理想。在本文中，我们提出了一种新的混合求解器，同时适用于立方体和征服步骤。前瞻和CDCL求解器在每个立方体上一起工作，而通信仅限于同步。我们的并行立方体和征服求解器可以解决许多实例比纯前瞻，纯CDCL和离线立方体和征服，并可以提前中止有利于一个纯CDCL搜索，如果一个实例是不适合立方体和征服技术。
2014-02-18 cs.AI cs.DS
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
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
A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
University of Waterloo（滑铁卢大学）
本文将CDCL SAT求解器的重置触发问题建模为多臂老虎机问题，提出基于UCB和Thompson sampling的强化学习自适应重置策略，并引入部分重置概念，实验证明该方法显著提升了求解性能。
2024-04-19 cs.AI cs.LG cs.LO
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning
Barcelogic
本文将 SAT 求解中的冲突驱动子句学习技术扩展到整数线性规划，提出 IntSat 方法并给出基础实现，证明其可作为现有 ILP 求解器的有效补充。
2024-02-16 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
Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship
Clermont Auvergne University（克莱蒙奥弗涅大学）；CNRS（法国国家科学研究中心）
子句学习是冲突驱动子句学习（CDCL）SAT求解器的重要组成部分之一，在工业实例中非常有效。由于在最坏的情况下，学习子句的数量被证明是指数的，所以有必要识别最相关的子句来保持和删除不相关的子句。据文献报道，已经提出了几种学习子句删除策略。然而，在每个缩减步骤中要删除的子句的数量以及使用每个策略获得的结果的多样性造成了确定哪个标准更好的混乱。因此，在搜索步骤期间选择要移除哪些学习子句的问题仍然非常具有挑战性。在本文中，我们提出了一种新的方法来确定最相关的学习条款，而不赞成或排除任何建议的措施，但通过采用这些措施之间的优势关系的概念。我们的方法绕过了结果多样性的问题，并在对这些措施的评估之间达成了妥协。此外，所提出的方法还避免了另一个非平凡的问题，这是在学习子句数据库的每次减少要删除的子句的量。
2017-05-31 cs.AI
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
G-CSEA: A Graph-Based Conflict Set Extraction Algorithm for Identifying Infeasibility in Pseudo-Boolean Models
Sprinklr AI
提出基于图的冲突集提取算法G-CSEA，通过构建蕴含图追踪冲突约束，高效识别伪布尔排班模型中的不可行性，并可结合QuickXplain生成不可约不可行子集。
2025-09-16 cs.AI
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
The University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出 NeuroBack，通过离线 GNN 一次性预测变量相位并增强 Kissat，仅用 CPU 即可在 SATCOMP-2022/2023 上分别多求解 5.2% 和 7.4% 的问题。
2024-05-08 cs.AI cs.LG
Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
National University of Singapore（新加坡国立大学）；Rice University（莱斯大学）
提出FastFourierSAT，一种基于FFT卷积并行计算初等对称多项式的GPU加速混合SAT求解器，梯度计算速度提升100倍以上，并在大规模实例上表现优异。
2023-08-29 cs.AI cs.DC cs.IT
Community Structure in Industrial SAT Instances
UdL（莱里达大学）；UPC（加泰罗尼亚理工大学）；Universidad de Granada（格拉纳达大学）；CSIC（西班牙国家研究委员会）；Univ. Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）；Bordeaux INP（波尔多国立理工学院）
现代SAT求解器在解决工业实例方面取得了显着进展。大多数技术都是经过密集的实验过程开发出来的。据信，这些技术利用了工业实例的底层结构。然而，很少有作品试图准确地描述这种结构的主要特征。复杂网络研究界已经开发出分析技术和算法来研究可供SAT社区使用的真实世界图。最近，已经有一些尝试来分析复杂网络方面的工业SAT实例的结构，目的是解释SAT解决技术的成功，并可能改进它们。在本文中，复杂网络的结果的启发，我们研究的社区结构，或模块化，工业SAT实例。在一个具有清晰社区结构或高模块化的图中，我们可以找到一个将其节点划分为社区的分区，使得大多数边连接同一社区的变量。在我们的分析中，我们表示SAT实例的图形，我们表明，大多数应用程序的基准测试的特点是高模块化。相反，随机SAT实例更接近经典的Erdös-Rényi随机图模型，其中没有结构可以观察到。我们还分析了这种结构如何演变的CDCL SAT求解器的执行的影响。特别是，我们使用社区结构来检测求解器在搜索过程中学习到的新子句有助于破坏公式的原始结构。也就是说，习得性从句倾向于包含不同社区的变量。
2019-07-17 cs.AI cs.SI
Constrained optimization under uncertainty for decision-making problems: Application to Real-Time Strategy games
LS2N, Université de Nantes（南特大学LS2N实验室）；JFLI, CNRS, National Institute of Informatics（日本信息学研究所，法国国家科学研究中心JFLI实验室）
决策问题可以建模为组合优化问题与约束规划形式主义，如约束优化问题。然而，很少有约束规划的形式主义可以同时处理优化和不确定性，他们都不方便，我们在本文中处理的模型问题。在这里，我们提出了一种方法来处理组合优化问题的不确定性的经典约束优化问题的形式主义，通过注入秩相关效用从决策理论。我们还提出了我们方法的概念证明，以证明它是可实现的，可以使用常规约束求解器解决具体的决策问题，并提出了一个赢得2018年μRTS AI竞赛部分可观察轨道的机器人。我们的研究结果表明，它是可以处理不确定性与定期约束编程求解器，而不必定义一个新的形式主义，也不开发专用的求解器。这为约束程序设计中处理不确定性问题带来了新的视角。
2019-04-23 cs.AI
XCSP3-core: A Format for Representing Constraint Satisfaction/Optimization Problems
本文提出XCSP3-core格式用于表示约束满足/优化问题，聚焦主流框架与约束，提供Java和C++解析器，并为约束求解器竞赛定义核心比较格式。
2024-08-29 cs.AI
ViTSP: A Vision Language Models Guided Framework for Solving Large-Scale Traveling Salesman Problems
Purdue University（普渡大学）
ViTSP利用预训练视觉语言模型指导大规模TSP求解，通过识别子问题提升全局解的质量，实验表明其在大规模实例上优于现有方法。
2026-03-01 cs.AI
Sparsification for Fast Optimal Multi-Robot Path Planning in Lazy Compilation Schemes
Czech Technical University in Prague（布拉格捷克理工大学）
多机器人路径规划（MRPP）是指为机器人寻找从初始位置到指定目标位置的无碰撞路径。该问题通常使用无向图建模，其中机器人在顶点之间跨边缘移动。当代的最优求解算法包括直接解决问题的基于搜索的专用方法，以及将MRPP简化为不同形式的基于编译的算法，对于该不同形式的MRPP存在有效的求解器，例如约束编程（CP）、混合整数编程（MIP）或布尔可满足性（SAT）。在本文中，我们加强现有的SAT为基础的算法MRPP通过spartification的候选路径为每个机器人的目标布尔编码派生的集合。建议的路径集的稀疏化导致更小的目标布尔公式，可以更快地构造和求解，同时保持方法的最优性保证。
2021-03-08 cs.AI cs.RO
Bespoke Solvers for Generative Flow Models
Weizmann Institute of Science（魏茨曼科学研究所）；Meta
本文提出Bespoke solvers框架，为预训练流模型定制参数高效的ODE求解器，以极低训练成本和少量NFE显著提升生成质量，在CIFAR10和ImageNet-64上接近真实数据FID。
2023-10-29 cs.AI cs.CV cs.LG
Compilation-based Solvers for Multi-Agent Path Finding: a Survey, Discussion, and Future Opportunities
Faculty of Information Technology（信息技术学院）；Czech Technical University in Prague（捷克理工大学）
多智能体路径寻找（MAPF）在人工智能领域以及机器人领域和仓储物流等领域都受到了广泛的关注。标准MAPF中的任务是找到路径，通过该路径，智能体可以从其起始位置导航到指定的各个目标位置。两个额外要求的组合使得问题在计算上具有挑战性：（i）代理必须不相互碰撞，以及（ii）路径必须相对于某些目标是最优的。最佳MAPF求解的两种主要方法包括（1）直接求解MAPF的专用基于搜索的方法，以及（2）将MAPF实例简化为不同的良好建立的形式主义中的实例的基于编译的方法，对于该方法存在有效的求解器。基于编译的MAPF求解可以受益于目标求解器开发过程中积累的进步，通常长达数十年。我们总结和比较当代基于编译的求解器MAPF使用ASP，MIP和SAT等形式主义。我们展示了从过去的发展和当前的趋势中吸取的教训，并讨论了其更广泛的影响。
2021-04-23 cs.AI cs.MA
Scaling Neuro-symbolic Problem Solving: Solver-Free Learning of Constraints and Objectives
LAAS-CNRS（法国国家科学研究中心系统分析与架构实验室）；Université de Toulouse（图卢兹大学）；CNRS（法国国家科学研究中心）；INSA（国立应用科学学院）；Télécom-Paris（巴黎高等电信学院）；TBI（图卢兹生物技术研究所）；INRAE（法国国家农业、食品与环境研究院）；ANITI（图卢兹人工智能与自然智能跨学科研究所）
本文提出了一种可微神经符号架构和损失函数，用于高效学习解决NP难推理问题，通过概率损失同时学习约束和目标，实现可扩展训练和高精度推断。
2025-12-18 cs.AI cs.LO cs.SC
Clingcon: The Next Generation
Kobe University（神户大学）；University of Potsdam（波茨坦大学）；Simon Fraser University（西蒙弗雷泽大学）；Griffith University（格里菲斯大学）；INRIA Rennes（法国国家信息与自动化研究所雷恩分部）
我们提出了第三代的约束答案集系统clingcon，结合答案集编程（ASP）和有限域约束处理（CP）。虽然它的前辈依靠黑盒方法通过集成CP求解器gecode来混合求解，但新的clingcon系统采用了一种懒惰的方法，使用专用的约束传播器来扩展底层ASP求解器clasp中的传播。不需要对clingcon的混合建模语言进行解析和基础扩展，因为ASP grounder gringo的新通用理论处理能力可以容纳这两种语言。作为一个整体，clingcon 3是ASP系统clingo 5的扩展，clingo 5本身依赖于grounder gringo和solver clasp。clingcon的新方法提供了CP传播到ASP求解的无缝集成，这得益于卡环推理模式的整个频谱，包括例如多镜头求解和高级优化技术。这是通过一种惰性方法来实现的，该方法展开约束的表示，并仅在需要时将其添加到逻辑程序的表示中。虽然展开通常由求解过程中的约束传播器决定，但它可以在预处理过程中部分（甚至全部）完成。此外，clingcon的约束预处理和传播结合了几种成熟的CP技术，大大提高了其性能。我们证明了这一点，通过一个广泛的实证评估对比，第一，CSP解决方案的背景下，第二，新的clingcon系统与其他混合ASP系统的各种技术。逻辑程序设计理论与实践（Theory and Practice of Logic Programmin…
2017-05-12 cs.AI
Accelerating ODE-Based Neural Networks on Low-Cost FPGAs
Keio University（庆应义塾大学）
ODENet是一种深度神经网络架构，其中ResNet的堆叠结构是用常微分方程（ODE）求解器实现的。它可以减少参数的数量，并通过选择合适的求解器在精度和性能之间取得平衡。还可以在资源有限的边缘设备上保持相同数量的参数的同时提高精度。本文采用欧拉方法作为ODE求解器，在PYNQ-Z2等低成本FPGA（Field-Programmable门阵列）板上实现了ODENet的部分专用逻辑。作为ODENet的变种，减少ODENets（rODENets），其中每一个都大量使用的ODENet层的一部分，并减少/消除一些层不同的低成本FPGA实现提出和分析。它们的参数大小，精度，执行时间和FPGA上的资源利用率方面进行评估。结果表明，与纯软件执行相比，rODENet变体的总体执行时间提高了2.66倍，同时保持了与原始ODENet相当的准确性。
2023-03-10 cs.AI cs.LG
