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
Set Constraint Model and Automated Encoding into SAT: Application to the Social Golfer Problem
Université d’Angers（昂热大学）；Université de Nantes（南特大学）；Pontificia Universidad Católica de Valparaiso（瓦尔帕莱索天主教大学）；Universidad Finis Terrae（芬尼斯泰拉大学）；Universidad Autónoma de Chile（智利自治大学）
一方面，约束满足问题允许一个声明模型的问题。另一方面，命题可满足性问题（SAT）求解器可以处理巨大的SAT实例。因此，我们提出了一种技术，声明式建模集约束问题，并将它们自动编码成SAT实例。我们将我们的技术应用于社会高尔夫问题，我们也用它来打破对称的问题。我们的技术是更简单，更声明性，更不容易出错，比直接和改进的手建模。我们自动生成的SAT实例比改进的手写实例（如[20]）包含更少的子句，并且通过单元传播，它们也包含更少的变量。此外，它们非常适合SAT求解器，并且在解决社交高尔夫问题的困难实例时，它们可以更快地解决。
2014-06-30 cs.AI
SATViz: Real-Time Visualization of Clausal Proofs
Karlsruhe Institute of Technology (KIT)（卡尔斯鲁厄理工学院）；Institute of Theoretical Informatics（理论信息学研究所）
SATViz是一款采用力导向布局算法、基于变量交互图的可视化工具，可实时可视化SAT实例的子句证明，用于研究SAT实例的社区结构及相关特性。
2026-08-03 cs.AI
Multi-Instance Dynamic Ordinal Random Fields for Weakly-supervised Facial Behavior Analysis
Pompeu Fabra University（庞培法布拉大学）；MIT Media Lab（麻省理工学院媒体实验室）；Imperial College London（帝国理工学院）；University of Twente（特文特大学）
针对弱监督学习问题，提出了一种多实例学习（MIL）方法，训练集由袋（特征向量或实例集）组成，只提供袋级的标签。具体来说，我们考虑多实例动态有序回归（MI-DOR）设置，其中实例标签自然表示为有序变量，袋子结构为时间序列。为此，我们提出了多实例动态有序随机场（MI-DORF）。在这个框架中，我们将实例标签视为无向图模型中的时间依赖潜变量。不同的MIL假设建模通过新引入的高阶潜力相关的袋和实例标签内的能量函数的模型。我们还扩展了我们的框架，以解决部分观测MI-DOR问题，其中在训练过程中可以使用实例标签的子集。我们在弱监督面部行为分析，面部动作单元（DISFA数据集）和疼痛（UNBC数据集）强度估计的任务上表明，所提出的框架优于其他学习方法。此外，我们表明，MIDORF可以用来减少大规模的数据注释工作在这种情况下。
2018-03-01 cs.AI cs.CV
Breaking Instance-Independent Symmetries In Exact Graph Coloring
University of Michigan（密歇根大学）；American University in Sharjah（沙迦美国大学）
代码优化和高级综合可以归结为约束满足和优化问题，如寄存器分配中的图着色。图着色还用于对与AI相关的更传统的CSP进行建模，例如计划，时间表和调度。可证明的最优解决方案对于商业和国防应用可能是期望的。此外，对于诸如寄存器分配和代码优化之类的应用，自然发生的图着色的实例通常很小，并且可以最优地解决。最近一波布尔可满足性（SAT）和0-1线性规划（ILP）算法的改进建议使用通用的问题归约方法，而不是问题特定的算法，因为（1）算法可能会被新的约束打乱，（2）算法往往忽略结构，（3）许多相关问题是不可证明的。问题简化通常会导致高度对称的SAT实例，而对称性会降低SAT求解器的速度。在这项工作中，我们比较了几种对称性破缺的途径，特别是当某些类型的对称性存在于所有生成的实例。我们专注于将CSP减少到SAT，这使我们能够利用SAT求解器最近的巨大改进，并自动从未来的进展中受益。我们可以使用各种黑盒SAT求解器而无需修改它们的源代码，因为我们的破解技术是静态的，即，我们在预处理期间检测对称性并添加对称性破坏谓词（SBP）。我们工作的一个重要结果是，在我们研究的实例独立SBPs类型及其组合中，最简单和最不完整的构造是最有效的。我们的实验也清楚地表明，实例独立的对称性大多应该与实例特定的对称性一起处理，而不是在规范级别，与文献中所建议的相反。
2011-09-11 cs.AI
How the Landscape of Random Job Shop Scheduling Instances Depends on the Ratio of Jobs to Machines
Carnegie Mellon University（卡内基梅隆大学）
我们描述了随机实例的作业车间调度问题（JSP）的搜索景观。具体来说，我们调查的期望值（1）骨干网的大小，（2）接近最优的时间表之间的距离，（3）随机调度的最大完工时间作为一个函数的工作机器比（N/M）的变化。对于N/M接近0和N/M接近无穷大的极限情况，我们提供了分析结果，而对于N/M的中间值，我们进行实验。我们证明了当N/M接近0时，骨架尺寸接近100%，而当N/M接近无穷大时，骨架消失。在这个过程中，我们表明，随着N/M接近0（分别为）。N/M接近无穷大），简单的优先级规则几乎必然产生最优调度，为车间调度中典型实例难度的“易-难-易”模式提供了理论证据。我们还绘制了我们的理论结果和JSP景观的“大山谷”图片之间的连接。
2011-09-30 cs.AI
Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem
Institute for System Dynamics and Control Theory SB RAS（俄罗斯科学院西伯利亚分院系统动力学与控制论研究所）
在本文中，我们提出的方法来构造划分的硬变量的布尔可满足性问题（SAT）。这样的划分可以用于并行求解对应的SAT实例。对于同一个SAT实例，可以构造不同的分区，每个分区都是原始SAT实例的简化版本的集合。任意划分的有效性取决于从任意划分中求解所有SAT实例的总时间，本文提出了一种基于Monte Carlo方法的任意划分处理时间估计方法。每一个分区，我们在特殊的有限搜索空间中的一个点。特定划分的有效性的估计是该空间的对应点中的预测函数的值。搜索有效划分的问题可以用公式表示为预测函数的优化问题。我们使用元启发式算法（模拟退火和禁忌搜索）从点移动到点的搜索空间。在我们的计算实验中，我们发现了SAT实例编码的一些密码函数的逆问题的划分。这些SAT实例中有几个具有现实的预测求解时间，在计算集群和志愿者计算项目SAT@home中成功求解。求解时间与所提出的方法得到的估计吻合得很好。
2015-07-03 cs.AI
Backbone Fragility and the Local Search Cost Peak
University of Edinburgh（爱丁堡大学）；University of St. Andrews（圣安德鲁斯大学）
局部搜索算法WSat是求解可满足性问题的最成功的算法之一。它在解决所谓的“可满足性阈值”附近的硬随机3-SAT实例时特别有效，但在阈值附近的搜索成本中仍然显示出峰值，并且不同实例的成本变化很大。我们作出了一些重大贡献的分析WSAT的高成本的随机实例，使用最近推出的概念的主干SAT实例。主干是实例所包含的文字的集合。我们发现，解决方案的数量预测成本以及小骨干实例，但相关性小得多的大型骨干实例出现在阈值附近，并在过度约束区域占主导地位。我们显示了一个非常强的相关性搜索成本和汉明距离最近的解决方案早期WSAT的搜索。这个模式引导我们引入一个实例的主干脆弱性的度量，它表明当子句被删除时主干的持久性。我们建议，本地搜索的高成本随机实例是那些具有非常大的骨干，骨干脆弱。我们认为，在满足性阈值以上的成本衰减是由于增加骨干的鲁棒性（骨干脆弱性的相反）。我们的假设做出了三个正确的预测。首先，在控制其他因素的情况下，实例的主干鲁棒性与局部搜索成本呈负相关。第二，最小主干实例（即3-SAT实例，经过修改，使其主干更脆弱）对于WSAT来说异常困难。第三，在搜索过程中最经常不满足的子句是那些删除对主干影响最大的子句。在了解局部搜索方法的病理学，我们希望有助于新的和更好的技术的发展。
2011-06-01 cs.AI
Instance-level Randomization: Toward More Stable LLM Evaluations
Meituan Group（美团集团）；Fudan University（复旦大学）
针对大语言模型评估中因随机因素微小变化导致的不稳定性与不公平比较问题，本文提出实例级随机化（ILR）方法，通过对每个实例随机化所有评估因素并取多次实验平均分，有效降低了方差并以不到一半的计算成本实现了与以往方法相似的鲁棒性。
2025-09-16 cs.AI cs.LG
W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs
本文提出 W2SAT 框架，通过学习加权文字关联图（WLIG）的内在结构来生成高质量 SAT 实例，并利用最优权重覆盖（OWC）方法解码，有效缓解了工业级 SAT 数据匮乏问题。
2024-09-24 cs.AI cs.LG
Where the Really Hard Quadratic Assignment Problems Are: the QAP-SAT instances
Université du Littoral Côte d’Opale (ULCO)（滨海加来海峡大学（ULCO））；Edinburgh Napier University（爱丁堡龙比亚大学）
针对二次分配问题（QAP）的相变现象，提出基于子模性的QAP-SAT设计以刻画问题难度，经分支定界与禁忌搜索实验验证，两类临界参数高度相关，可预测困难实例。
2024-03-05 cs.AI
DeepSAT: An EDA-Driven Learning Framework for SAT
The Chinese University of Hong Kong（香港中文大学）
我们提出了DeepSAT，这是一种用于布尔可满足性（SAT）问题的新型端到端学习框架。与现有的解决方案在随机SAT实例上训练相对较弱的监督不同，我们建议将成熟的电子设计自动化（EDA）领域的知识应用于SAT求解。具体来说，我们首先诉诸逻辑合成算法预处理SAT实例到优化和逆变器图（AIG）。通过这样做，可以显着减少各种SAT实例之间的分布差异，这有利于提高学习模型的泛化能力。其次，我们认为SAT解的分布是条件伯努利分布的乘积。基于这一观察，我们近似的SAT求解过程与条件生成模型，利用一种新的有向无环图神经网络（DAGNN）与两个极性原型的条件SAT建模。为了有效地训练生成模型，我们借助逻辑仿真工具，得到AIG中节点为逻辑“1”的概率作为富监督。我们对各种SAT问题进行了综合实验。我们的研究结果表明，与最先进的基于学习的SAT解决方案相比，DeepSAT实现了显着的准确性提高，特别是当推广到相对较大或具有不同分布的SAT实例时。
2023-01-20 cs.AI
FLIPS: Instance-Fingerprinting for LLMs via Pseudo-random Sequences
Inria（法国国家信息与自动化研究所）
提出FLIPS方法，利用生成的二进制随机序列中的偏差，在237个模型实例上实现96%（闭集）和90%（开集）的识别准确率，解决了现有指纹识别技术无法区分同一LLM不同配置的问题，为AI监管提供了实例级指纹识别新范式。
2026-06-02 cs.AI cs.CR cs.LG
Simple Algorithm Portfolio for SAT
M. Nikoli\'c Faculty of Mathematics, University of Blegrade, Belgrade, Serbia Tel.: +381648650064 F. Mari\'c Faculty of Mathematics, University of Blegrade, Belgrade, Serbia P. Jani ci\'c Faculty of Mathematics, University of Blegrade, Belgrade, Serbia
算法组合技术对于SAT的重要性早已被注意到，并且已经设计出了许多非常成功的系统，包括最成功的一个-- SATzilla。然而，所有这些系统都相当复杂（要理解、重新实现或修改）。在本文中，我们提出了一个新的算法组合SAT，这是非常简单的，但在同一时间如此有效，它优于SATzilla。对于一个新的SAT实例，我们的投资组合从训练集中找到它的k-最近邻居，并调用一个在这些实例中表现最好的求解器。我们的算法组合的主要特点是选择过程的局部性-SAT求解器的选择仅基于与输入类似的少数实例。
2011-12-13 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
Extending Modern SAT Solvers for Enumerating All Models
本文讨论了在合取范式（CNF）中枚举布尔公式的所有模型的问题。我们提出了一个扩展的CDCL为基础的SAT求解器来处理这个基本问题。然后，我们提供了一个实验评估，我们提出的SAT模型枚举算法，从最后的SAT挑战，并从基于SAT的编码的序列挖掘问题的实例上的可满足的SAT实例。
2013-05-06 cs.AI
LLM-Based Instance-Driven Heuristic Bias In the Context of a Biased Random Key Genetic Algorithm
Artificial Intelligence Research Institute (IIIA-CSIC)（西班牙国家研究委员会人工智能研究所）；University of Concepcion（康塞普西翁大学）
本研究提出将LLM与偏置随机键遗传算法结合，通过人机协作设计实例特定度量并生成定制启发式偏置，有效解决了NP-hard最长游程子序列问题，并在1050个实例上验证了其相比基线的显著提升。
2025-09-05 cs.AI cs.CL cs.NE
Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem
DSO National Laboratories（DSO国家实验室）；National University of Singapore（新加坡国立大学）
调查传播（SP）算法已被证明是工作良好的随机3-SAT问题的相变附近的大型实例。结果表明，SP估计边际覆盖，代表集群的解决方案。SP-y算法将SP算法推广到了最大可满足性（Max-SAT）问题，但SP算法的覆盖解释并没有推广到SP-y算法。在本文中，我们制定了放松调查传播（RSP）算法，该算法扩展了SP算法以应用于加权Max-SAT问题。我们表明，RSP有一个解释，估计边缘覆盖违反了一组条款，最小的重量。这自然概括了SP的覆盖解释。从经验上讲，我们表明RSP优于SP-y和其他最先进的Max-SAT求解器的随机Max-SAT实例。RSP在随机加权Max-SAT实例上的性能也优于最先进的加权Max-SAT求解器。
2014-01-15 cs.AI
Improved SAT models for NFA learning
LERIA（昂热大学信息学、机器人学与人工智能实验室）；University of Angers（昂热大学）
语法推理是研究从单词中学习自动机和语法的算法。我们专注于从单词样本中学习大小为k的非确定性有限自动机。为此，我们制定了一个SAT模型的问题。生成的SAT实例是巨大的，我们提出了一些模型的改进，无论是在变量的数量，条款的数量，条款的大小。这些改进显著减少了实例，但代价是生成时间更长。因此，我们试图平衡实例大小与生成和求解时间。我们还实现了一些实验比较，我们分析了我们的各种模型的改进。
2021-07-13 cs.AI cs.LO
Collaborative Management of Benchmark Instances and their Attributes
Karlsruhe Institute of Technology (KIT)（卡尔斯鲁厄理工学院）
实验评估是算法设计过程中不可或缺的一部分。公开可用的基准实例被广泛用于评估SAT求解中的方法。对于结果的解释和算法组合的设计，它们的属性是至关重要的。通过我们对基准实例标识符的规范，捕获基准实例及其属性的相互关系被大大简化。因此，我们的工具通过提供按属性管理和检索基准实例的方法来提高两者的可用性，反之亦然。像这样，它方便了SAT实验的设计和分析以及结果的交流。
2021-09-09 cs.AI cs.DB cs.LO
GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection
McGill University（麦吉尔大学）
针对现有SAT求解器选择方法依赖人工特征、忽略图结构与领域知识的问题，提出融合三部图表示、定制化异质GNN及运行时敏感损失的GraSS方法，在两类基准上实现7个顶尖求解器池的运行时提升。
2024-05-17 cs.AI cs.LG
Hiding Satisfying Assignments: Two are Better than One
不完全可满足性求解器的评价关键取决于硬可满足实例的可用性。这种情况的一个合理来源是随机k-SAT公式，其子句是从满足某个随机选择的真值分配A的所有子句中均匀选择的。不幸的是，以这种方式生成的实例往往相对容易，并且可以通过实际的算法有效地解决。粗略地说，随着公式密度的增加，对于许多不同的算法，A充当越来越强的吸引子。最近的结果的空间上的几何满足随机k-SAT和NAE-k-SAT公式的真理分配的启发，我们介绍了一个简单的扭曲这个基本模型，这似乎大大增加了它的硬度。也就是说，除了禁止被隐藏赋值A违反的子句外，我们还禁止被它的补语违反的子句，使得A和A的补语都是令人满意的。似乎在这种“对称化”下，两个吸引子的影响在很大程度上抵消了，使得算法更难找到任何真值分配。我们给出了支持这一论断的理论和实验证据。
2005-03-20 cond-mat.dis-nn cond-mat.stat-mech cs.AI
Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits
ITMO University（ITMO大学）
在本文中，我们研究如何估计布尔可满足性（SAT）编码的逻辑等价性检查问题（LEC）的硬度。在常规SAT求解器无法在合理的时间内求解SAT实例的情况下，有意义的硬度估计非常重要。我们表明，可以估计\textit{w.r.t.}一些SAT分区的LEC实例的SAT编码的硬度。我们还证明了一个专门定义的随机变量与考虑分区的概率特性的估计的准确性的依赖。本文提出了几种构造划分的方法，在实践中使用时，可以很好地估计LEC的SAT编码的难度。在实验部分中，我们提出了一类可扩展的LEC测试，给出了一个相对较小的输入大小$n$所考虑的电路非常复杂的情况。例如，对于$n = 40$，没有一个最先进的SAT求解器可以在合理的时间内处理所考虑的测试。然而，这些测试可以使用所提出的分区方法并行解决。
2022-10-04 cs.AI
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
Decomposing Hard SAT Instances with Metaheuristic Optimization
ITMO University（圣彼得堡国立信息技术机械与光学大学）
本文在SAT问题框架下提出分解难度（d-hardness）概念，将其表示为随机变量期望，用蒙特卡洛方法计算、进化算法优化最小d-hardness的变量子集，验证了该方法在困难不可满足SAT实例求解中的适用性。
2023-12-16 cs.AI cs.DS
Ensembles of Random Sphere Cover Classifiers
University of East Anglia（东英吉利大学）
我们提出了一个新的基于实例的学习分类器，随机球覆盖（RSC）分类器，并评估替代集成方案。RSC将实例融合到球体中，然后基于到球体的距离而不是到实例的距离进行分类。RSC的随机性使其非常适合用于合奏。我们提出了两个集成方法定制的RSC分类器; $αβ$ RSE，集成的基础上的实例rescue和$α$ RSSE，子空间集成。我们比较了$αβ$ RSE和$α$ RSSE的树为基础的合奏一组UCI数据集，并证明RSC合奏执行显着优于这些合奏中的一些，并没有显着比其他更差。我们通过一个案例研究表明，六个基因表达数据集，$α$ RSSE可以优于其他子空间集成方法的高维数据时，与属性过滤器一起使用。最后，我们进行了一组偏差/方差分解实验，以分析与基础分类器相比的改进来源。
2014-09-17 cs.AI cs.LG stat.ML
New Inference Rules for Max-SAT
Université de Picardie Jules Verne（皮卡第儒勒·凡尔纳大学）；Artificial Intelligence Research Institute（人工智能研究所）；Spanish National Research Council（西班牙国家研究委员会）；Universitat de Lleida（莱里达大学）
与SAT求解器相比，精确Max-SAT求解器在证明树的每个节点上应用很少的推理。常用的SAT推理规则（如单位传播）会产生一个保留可满足性的简化公式，但不幸的是，解决简化公式的Max-SAT问题并不等同于解决原始公式。在本文中，我们定义了一些原始的推理规则，除了被有效地应用，转换的Max-SAT实例到等价的Max-SAT实例，更容易解决。规则的合理性，可以被看作是适应最大SAT的单位分辨率的改进，通过整数规划变换以一种新颖而简单的方式被证明。为了找出推理规则在实践中的强大功能，我们开发了一个新的Max-SAT求解器，称为MaxSatz，它包含了这些规则，并进行了实验研究。结果提供了经验证据，MaxSatz是非常有竞争力的，至少在随机Max-2SAT，随机Max-3SAT，Max-Cut和Graph 3着色实例上，以及在Max-SAT Evaluation 2006的基准测试中。
2011-10-31 cs.AI
Learning Branching Heuristics for Propositional Model Counting
University of Toronto（多伦多大学）；UC Berkeley（加州大学伯克利分校）；Vector Institute（向量研究所）
命题模型计数（Propositional Model Counting），或#SAT，是计算布尔公式的满意赋值的数量的问题。来自不同应用领域的许多问题，包括许多离散概率推理问题，可以转化为模型计数问题，由#SAT求解器来解决。然而，精确的#SAT求解器通常不能扩展到工业规模的实例。在本文中，我们提出了Neuro#，一种用于学习分支算法的方法，以提高给定问题族实例上的精确SAT求解器的性能。我们的实验表明，我们的方法减少了类似的分布式举行了实例的步骤数，并推广到更大的实例，从同一个问题的家庭。它是能够实现这些结果对一些不同的问题家庭具有非常不同的结构。除了步数改进之外，Neuro#还可以在某些问题族中的较大实例上实现比vanilla求解器高出几个数量级的挂钟加速，尽管查询模型的运行时开销很大。
2022-09-08 cs.AI cs.LG cs.LO
SATfeatPy -- A Python-based Feature Extraction System for Satisfiability
Insight Centre for Data Science and Analytics（洞察数据科学与分析中心）；University College Cork（科克大学学院）；SFI Centre for Research Training in AI（SFI人工智能研究培训中心）；School of Computer Science & IT（计算机科学与信息技术学院）
特征提取是应用机器学习方法求解可满足性问题的一项基本任务。它用于求解器组合和可满足性分类的算法选择和配置。已经提出了许多方法从CNF实例中提取有意义的属性。其中大多数缺乏工作/更新的实施，有限的描述缺乏清晰度，影响了再现性。此外，文献中没有对这些特征进行比较。本文介绍了SATfeatPy，一个库，提供特征提取技术的SAT问题的CNF形式。该软件包提供了该领域主要论文的所有结构和统计功能的实现。该库以最新的、易于使用的Python包的形式提供，并附有详细的功能描述。我们展示了SAT/UNSAT和问题类别分类的高准确性，使用我们的库从3000个SAT和UNSAT实例的数据集生成的五组功能，超过十个不同类别的问题。最后，我们比较的有用性的功能和重要性预测SAT实例的原始结构中的消融研究。
2022-04-29 cs.AI
Resource-Constrained Heuristic for Max-SAT
SRI International（SRI国际）
提出一种资源受限的 Max-SAT 启发式方法，通过内外循环分解问题，支持传统求解器或 QUBO 专用硬件优化，并优于现有方案。
2024-10-11 cs.AI
Should Algorithms for Random SAT and Max-SAT be Different?
Microsoft Research（微软研究院）；Rutgers University（罗格斯大学）
我们分析了在何种程度上的随机SAT和最大SAT问题在其属性的不同。我们的研究结果表明，对于比率在一定范围内的随机$k$ -CNF，Max-SAT可以用任何具有次指数减速的SAT算法求解，而对于比率大于某个常数的公式，随机游走框架下的算法需要实质上不同的算法。根据这些结果，我们提出了一种新的概率方法随机Max-SAT称为ProMS。实验结果表明，ProMS优于许多国家的最先进的局部搜索求解器的随机最大SAT基准。
2018-11-02 cs.AI
A Two-Stage Algorithm for Cost-Efficient Multi-instance Counterfactual Explanations
Bielefeld University（比勒费尔德大学）；University of Cyprus（塞浦路斯大学）；Cyprus University of Technology（塞浦路斯理工大学）
针对现有反事实解释多仅支持单实例、难以满足多实例同时适配需求的问题，提出一种灵活的两阶段算法，可查找实例组并生成成本高效的多实例反事实解释，经对比验证性能优于主流方法。
2024-05-21 cs.AI cs.LG
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
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
The Configurable SAT Solver Challenge (CSSC)
University of Freiburg（弗莱堡大学）；University of Ulm（乌尔姆大学）；University of British Columbia（不列颠哥伦比亚大学）
众所周知，不同的解决策略适用于不同类型的组合难题。因此，大多数命题可满足性问题（SAT）的求解器都暴露了参数，这些参数允许它们针对特定的实例族进行自定义。在国际SAT竞赛系列中，这些参数被忽略：求解器使用给定轨道中所有基准实例的单个默认参数设置（由作者提供）运行。虽然这种竞赛形式奖励具有鲁棒默认设置的求解器，但它并不反映仅关心一个特定应用程序上的性能并且可以投入一些时间来调整该应用程序的求解器参数的从业者所面临的情况。新的可配置SAT求解器竞赛（CSSC）比较了后一种设置中的求解器，通过完全自动化配置步骤后实现的性能对每个求解器进行评分。本文更详细地描述了CSSC，并报告了迄今为止在CSSC 2013和2014两个实例中获得的结果。
2016-08-02 cs.AI cs.LG
