Generating clause sequences of a CNF formula
给定具有子句$C_1,\ldots,C_m$和变量$V=\{x_1,\ldots,x_n\}$的CNF公式$Φ$，$Φ$的真值赋值$a:V\rightarrow\{0,1\}$导致子句序列$σ_Φ(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m$，其中$C_i(a) = 1$ if子句$C_i$在赋值$a$下求值为$1$，否则为$C_i(a) = 0$。所有可能的子句序列的集合携带关于公式的大量信息，例如SAT、MAX-SAT和MIN-SAT可以根据找到具有极值属性的子句序列来编码。我们考虑在Dagstuhl研讨会19211“数据管理中的枚举”（2019）上提出的一个问题，关于生成给定的具有有界维数的CNF的所有可能的子句序列。我们证明了问题可以在增量多项式时间内解决。我们进一步给出了这类易处理CNF公式的多项式延迟算法。我们还考虑了最大子句序列和最小子句序列的生成问题，证明了最大子句序列的生成是NP-困难的，而最小子句序列的生成具有多项式延迟。
2020-02-17 cs.DM cs.LO
Conflict-Driven XOR-Clause Learning (extended version)
现代冲突驱动子句学习（CDCL）SAT求解器在求解合取范式（CNF）公式方面非常出色。然而，一些应用问题涉及大量的奇偶校验（XOR）约束，如果转换为CNF，不一定有效地处理。本文研究了在DPLL（XOR）框架下求解含XOR子句的CNF公式，其中CDCL SAT求解器与单独的XOR推理模块相耦合。新技术的开发，用于分析XOR推理推导，允许一个获得较小的CNF子句的XOR隐含文字的解释，也派生和学习新的XOR子句。它被证明，这些新技术允许非常短的不可满足性证明的一些公式，其CNF翻译没有多项式大小的分辨率证明，即使是一个非常简单的异或推理模块，只能单位传播。一组具有挑战性的逻辑密码分析实例的效率进行评估所提出的技术。
2014-07-24 cs.LO
Simulating Parity Reasoning (extended version)
命题可满足性（SAT）求解器以合取范式（CNF）为代表，在许多领域都有着广泛的应用。然而，在诸如电路验证、有界模型检验和逻辑密码分析之类的一些应用领域中，实例可能具有许多奇偶校验（XOR）约束，如果将其转换为CNF，则可能无法有效地处理这些约束。因此，扩展CNF驱动的搜索与各种奇偶性推理引擎，从等价推理增量高斯消除已被提出。本文研究了如何更强的奇偶校验推理技术的DPLL（XOR）框架可以模拟更简单的系统：分辨率，单位传播，奇偶校验的解释。这样的模拟是有趣的，例如，开发下一代SAT求解器能够有效地处理奇偶约束。
2013-11-18 cs.LO
Solving SAT By Computing A Stable Set Of Points In Clusters
本文提出以簇为单位计算稳定点集（SSP）来求解SAT，避免逐点计算不可行的问题，从而更好地利用公式结构并促进并行SAT求解。
2025-07-17 cs.LO
Small unsatisfiable $k$-CNFs with bounded literal occurrence
本文研究了有界出现次数的 $k$-CNF 子类中最小不可满足公式，结合理论论证与基于 SMS 的对称性破缺穷举搜索，确定了 3-CNF 子类的最小规模并改进了 4-CNF 的已知结果，为 MaxSAT 不可近似性提供了更强依据。
2024-07-19 cs.CC cs.DM cs.LO
Decision versions of optimization problems: cardinality constraint (lower bound) as a CNF Horn formula for Maximum Matching
我们以$|F| \ge K$的形式提供了一个下界公式，使得未加权非二分匹配的决策版本可以在多项式时间内求解。~参数$K$可能因实例而异。我们假设定义域，即顶点集和边集是有序的。据我们所知，没有多项式可解的可满足性表达式已经开发了这个问题，到目前为止，或就此而言，任何决策问题，来自优化。因此，对于这些问题，这为解决它们开辟了一条新途径。
2014-10-23 cs.LO
On the Satisfaction Probabilities of $k$-CNF Formulas
本文针对 $k$CNF 公式满足概率问题 $k$SAT-Pr$_{>p}$ 给出完整三分法刻画，证明其属于 AC$^0$、NL-完全或 NP-完全，并基于最大满足概率公式的存在性建立核化、后门集和局部性等关键性质。
2024-08-09 cs.CC cs.LO
Almost 2-SAT is Fixed-Parameter Tractable
我们考虑以下问题。给定一个2-CNF公式，是否可以最多删除$k$子句，以使得到的2-CNF公式是可满足的？这个问题在理论计算机科学的不同研究团体中被称为“几乎2-SAT”、“除了$k$ 2-SAT之外的所有”、“2-CNF删除”、“2-SAT删除”。该问题的固定参数可处理性是参数化复杂性领域长期存在的问题。我们解决了这个问题，提出了一个算法，解决了这个问题，在$O(15^k*k*m^3)$，因此，我们表明，这个问题是固定参数听话。
2008-04-18 cs.CG cs.DS cs.LO
Phase transition for Local Search on planted SAT
局部搜索算法（或爬山法，或迭代改进法）是解决可满足性和最大可满足性问题的最简单的算法之一。它是许多可满足性和最大可满足性求解器的一部分，用于为更复杂的算法找到一个好的起点，并改进候选解。本文分析了随机种植3-CNF公式的局部搜索问题。我们证明了如果k<7/6使得子句与变量的比率小于kln（n）（n是CNF中变量的数量），那么局部搜索whp找不到满意的分配，如果k>7/6使得子句与变量的比率大于kln（n）$，那么局部搜索whp找到满意的分配.作为一个副产品，我们还表明，对于任何常数r有g，使本地搜索应用到一个随机的（不一定种植）3-CNF与条款变量比r产生的分配，满足至少gn条款小于最大数量的可满足的条款。
2008-11-16 cs.DS cs.LO
Reified unit resolution and the failed literal rule
Université de Bourgogne（勃艮第大学）
单元分解可以简化CNF公式或通过重复分配单元子句中出现的变量来检测不一致。给定任何CNF公式西格玛，我们表明，存在一个可满足的CNF公式psi的大小多项式相关的大小西格玛，使单位分辨率psi模拟所有的影响，将其应用到西格玛。公式psi被认为是sigma的具体对应物。这种方法可以用来证明失败的文字规则，这是一个推理规则，使用一些SAT求解器，可以完全模拟单位分辨率。更一般地说，它揭示了单位分辨率的表达能力。
2010-11-12 cs.AI cs.LO
On Tackling the Limits of Resolution in SAT Solving
布尔可满足性（SAT）求解器的实际成功源于SAT求解的CDCL方法。然而，从命题证明复杂性的角度来看，CDCL并不比解决证明系统更强大，因为存在许多困难的例子。提出了一种新的问题变换，将合取范式（CNF）公式的判定问题转化为求解Horn公式的最大可满足性问题.给出了新的变换，证明了鸽洞公式MaxSAT分解步数的多项式界.这一结果是在明显的对比与早期的结果的长度证明的MaxSAT分辨率鸽子公式。本文还建立了相同的多项式约束的情况下，现代核心引导MaxSAT求解器。实验结果表明，CNF公式已知是很难CDCL SAT求解器，这些可以有效地解决与现代MaxSAT求解器。
2017-07-05 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
Covered Clause Elimination
TU Delft（代尔夫特理工大学）；Univ. Helsinki（赫尔辛基大学）；JKU Linz（林茨约翰·开普勒大学）
推广[M. Heule，M. Järvisalo和A.比尔CNF公式的子句删除程序。在Proc. LPAR-17，LNCS的第6397卷，第357-371页中。Springer，2010年]，我们介绍了显式（CCE），隐藏（HCCE），和非对称（ACCE）的程序，从CNF公式消除覆盖条款的变种。我们表明，这些程序是更有效地减少CNF公式比各自的变种阻塞子句消除，因此可能是有趣的SAT解决新的预处理/简化技术。
2010-11-23 cs.AI cs.LO
Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas
HSE University（高等经济大学）
研究在Rocq中首次形式化验证罗马诺夫三元组逻辑，实现滑动窗口3-CNF的已验证过滤器，给出正确性边界，开发VFR原型并通过基准测试验证，完整工具链已公开。
2026-08-26 cs.AI cs.CC cs.LO
SAT Solving Using XOR-OR-AND Normal Forms
本文提出逻辑公式的 XOR-OR-AND 范式（2-XNF），给出 CNF/ANF 到 2-XNF 的转换方法，并设计基于 DPLL 的求解器，在 ASCON-128 密码实例上优于现有方法。
2024-09-26 cs.LO math.AC math.LO
Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
University of Louisiana at Lafayette（路易斯安那州立大学拉斐特分校）
提出配对公式协议和准确区分率（ADR）来评估大语言模型在SAT问题上的推理能力，发现传统指标具有误导性，而ADR能更忠实、跨表示鲁棒地评估模型。
2026-05-27 cs.AI cs.CL cs.LO
Are You Satisfied by This Partial Assignment?
University of Trento（特伦托大学）
SAT和SAT相关问题的许多程序-特别是那些需要满足真值分配的完整枚举的程序-依赖于检测满足输入公式的部分分配的效率。在本文中，我们分析了部分分配可满足性的概念-特别是在处理非CNF和存在量化公式时-提出了关于这个概念的模糊性和微妙性的标志，并调查其实际后果。这可能会推动更有效的分配枚举算法的发展。
2020-02-28 cs.AI cs.LO
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
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
National University of Singapore（新加坡国立大学）；Indian Institute of Technology, Bombay（印度理工学院孟买分校）
给定n个变量的CNF公式F，模型计数或#SAT的问题是计算F的满足赋值的数量。模型计数是计算机科学中的一个基本而又困难的问题，有着广泛的应用。近年来，人们对开发有效的算法技术进行了大量的努力，这些技术将经典的2-universal hashing与过去十年中SAT求解的显着进步相结合。这些技术增加了CNF公式F与随机XOR约束，并调用NP预言反复对所得CNF-XOR公式。在实践中，对NP oracle调用的调用被SAT求解器取代，SAT求解器的运行时性能受到XOR约束的大小的不利影响。2-通用散列函数的标准构造选择概率p = 1/2的每个变量，从而导致期望大小为n/2的XOR约束。因此，挑战在于设计稀疏散列函数，其中可以以较小的概率选择变量并导致较小大小的XOR约束。在本文中，我们从理论和实践的角度来应对这一挑战。首先，我们正式放松的通用散列，称为集中散列，并建立一个新的和美丽的连接，这些散列函数的浓度措施和布尔超立方体上的等周不等式。这允许我们获得方差和分散指数的（log m）紧界，并表明p = O（log（m）/m）足以设计从{0，1}^n到{0，1}^m的稀疏散列函数。然后，我们使用稀疏散列函数属于这个集中的哈希家庭开发新的近似计数算法。我们的算法在1893基准测试的综合实验评估表明，稀疏散列函数的使用可以导致显着的加速。
2020-04-30 cs.DS cs.LG cs.LO
A Real World Mechanism for Testing Satisfiability in Polynomial Time
命题演算公式F的可满足性是否能在多项式时间内确定是一个公开问题。我提出了一个简单的程序，基于一些现实世界的机制来解决这个问题。主要结果是一个机器的蓝图，它能够测试任何公式的合取范式（CNF）的可满足性在线性时间。该设备使用光和一些电化学特性来发挥作用。它适应问题的范围，而不会随着公式的大小而呈指数增长。相反，它要求其组成部分具有无限的精度。
2010-01-19 cs.CC cs.LO
A criterion for "easiness" of certain SAT problems
一个广义的1-in-3SAT问题的定义和发现是在复杂性类P时，限制到某个子集的CNF表达式。特别地，当被限制为具有相等数目的子句（m）和变量（n）并且没有纯文字的精确READ-3公式时，可以在多项式时间内判定对每个子句的文字数目没有限制的1-in-kSAT。也可以检查单个实例是否容易相对于给定的SAT问题。通过识别整个类的公式是可有效解决的方法也可能是感兴趣的互补搜索硬的情况。
2017-07-01 cs.CC cs.LO
SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme
该研究针对F₂上的矩阵乘法SAT基准，发现10个预期不可满足的Challenge-2公式实际可满足，还构造了无3型项的秩23方案，生成了21个实例的SAT证书且可快速复现。
2026-08-03 cs.LO cs.SC
Removal of Quantifiers by Elimination of Boundary Points
我们考虑从布尔CNF公式中消除存在量词的问题。我们的方法基于以下观察。通过增加F的预解式子句消除边界点，可以消除量化CNF公式F对一组变量的依赖性。这种方法类似于[9]中描述的量词消去方法。本论文中描述的方法的差异是双重的：{ \bullet }分支仅在量化变量上执行，{ \bullet }通过调用SAT求解器来执行边界点的显式搜索。尽管我们在此之前发表了论文[9]，但从时间上讲，本报告的方法首先开发。在[10]、[11]中对该方法进行了初步介绍。由于准备专利申请，我们推迟了这种方法的出版[8]。
2012-06-05 cs.DM cs.LO
