The Complexity of Satisfiability for Sub-Boolean Fragments of ALC
基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。所有这些片段都以这样或那样的方式限制了布尔运算符的使用。我们着眼于系统的和更一般的限制的布尔运算符，并建立复杂的概念可满足性问题的存在公理。我们把易处理的和难处理的病例分开。
2010-03-29 cs.CC cs.LO
Inverse Intersections for Boolean Satisfiability Problems
针对布尔可满足性（SAT）问题，研究提出矩阵表示方法及基于子句逆求解矩阵交集的简单算法，可得到有效可满足变量赋值，且证明全部解集规模相对矩阵呈指数级。
2025-05-16 cs.CC
A Critique of Kumar's "Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and Its Implications on P versus NP problem."
本文分析了Kumar在技术报告《CNF中布尔公式可满足的充分必要条件及其对P vs. NP问题的启示》中提出的论点。“该论文声称提出了一个决定CNF-SAT的多项式时间算法。我们表明，该文件的分析是有缺陷的，其算法的基本支撑需要在无限多的输入指数的步骤。
2021-12-11 cs.CC
Projective cofactor decompositions of Boolean functions and the satisfiability problem
给出了一个CNF公式$F$，给出了一个判定$F$的可满足性（SAT）和计算所有赋值解的新算法.该算法基于文献中已知的\emph{cofactors}的概念。本文是作者以前的工作布尔可满足性\cite{sul1, sul2,sude}的一个后果，但该算法基本上是独立的正交扩展概念，以前的论文是基于。该算法通过将搜索空间投影到满足公式中CNF的集合上，递归地选择一个具体的余因子。该辅因子称为\emph{projective cofactor}。这样的计算的优点是，它递归地分解成独立的子问题在每一个选择的投影余因子的可满足性问题。这导致了一个并行算法，以确定可满足性和计算所有解决方案的可满足公式。
2017-05-08 cs.CC
Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and its Implications on P versus NP problem
布尔可满足性问题在各个领域都有应用。求解可满足性问题的一个有效算法可以用来有效地解决许多其他问题。可满足性问题的输入是一个有限子句集。本文研究了小句的性质。已经定义了一种类型的子句，称为完全填充子句，它只包含一次每个变量。定义了两个不相等的完全填充子句之间的关系，称为兄弟子句。已经发现，如果一个完全填充的子句对于一个真值赋值为假，那么它的所有兄弟子句对于同一个真值赋值都将为真。这导致了一个布尔公式可满足的必要和充分条件，在CNF。利用这个充要条件，提出了一个求解布尔可满足性问题的多项式时间算法，即P = NP。此外，已经提供了一些优化，其可以与算法集成以获得更好的性能。
2021-05-24 cs.CC
A Linear Algebra Formulation for Boolean Satisfiability Testing
在文章\The State of SAT”中，作者询问是否可以找到与DPLL截然不同的过程来处理不可满足的实例。本研究提出了一种新的线性规划方法来有效地解决这个问题。实验结果表明，该方法适用于许多不满意的情况。然而，我们必须承认，这种方法应该是不完整的;否则，它将意味着P=co-NP。
2018-08-17 cs.CC
Linear Programming Formulation of the Boolean Satisfiability Problem
在本文中，我们提出了一种新的，基于图的建模方法和多项式规模的线性规划（LP）制定的布尔可满足性问题（SAT）。最后通过一个数值例子说明了该方法。
2016-10-20 cs.CC cs.DM
The Connectivity of Boolean Satisfiability: Dichotomies for Formulas and Circuits
对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。2006年，Gopalan等人研究了CSP的解图的连通性和相关的复杂性问题，主要是基于对可满足性算法和可满足性阈值的研究。他们证明了连通分量的直径和st-连通性问题的复杂性的二分法，并为连通性问题建立了一个二分法。最近，我们能够建立切除术[arXiv：1312.4524]。在这里，我们认为可满足性问题的布尔电路和命题公式，使用门，分别定义的连接问题。连接词，从一组固定的布尔函数。我们得到的直径和两个连通性问题的二分法：一方面，直径是线性的变量的数量，这两个问题是在P，而在另一边，直径可以是指数，和问题是PSPACE-完全的。对于部分量化的公式，我们显示了类似的二分法。
2015-10-25 cs.CC cs.LO
The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies
布尔可满足性问题是研究复杂性、算法、数学和阈值现象的重要基准。最近的工作，可满足性的阈值已集中在结构和连通性的解决方案空间。受这项工作的启发，我们研究了布尔可满足性问题的解空间的结构和连通性相关的性质，并在Schaefer的框架下建立了各种二分法。在结构方面，我们得到的二分法的超立方体的子图，可以引起的解决方案的布尔公式，以及直径的连通组件的解决方案空间。在计算方面，我们建立二分法定理的复杂性的连接性和st-连接性问题的图形的解决方案的布尔公式。我们的研究结果断言，计算二分法的棘手的一面是PSPACE-完全的，而易处理的一面-这包括但不限于所有问题的多项式时间算法的可满足性-是在P的ST-连接问题，并在coNP的连接问题。对于PSPACE完备的情况，组件的直径可以是指数的，而在所有其他情况下，它是线性的;因此，小直径和连通性问题的易处理性是显着一致的。我们的结果的关键是一个可表达性定理表明，在易处理的情况下，由解空间诱导的子图具有一定的良好的结构性质，而在棘手的情况下，子图可以是任意的。
2007-10-03 cs.CC
A novel algorithm for solving the Decision Boolean Satisfiability Problem without algebra
本文描述了一个算法，解决决策布尔可满足性问题的一个特殊的决策可满足性问题的二进制数值性质，并行执行，面向对象，和短终止。用扩展和简化这两种操作来解释为什么使用代数增加了分辨率步骤。证明了该问题的复杂度有一个上界为$2^{n-1}$，其中$n$是给定问题的逻辑变量数.
2018-04-14 cs.CC cs.DS cs.LO
Necessary and sufficient conditions for Boolean satisfiability
该研究作为P与NP复杂度类关系系列研究的第二篇，借助集合特殊覆盖概念证明其与布尔可满足性问题等价，得出布尔可满足性的充要算法条件，还能得到满足可满足性的变量取值。
2023-11-05 cs.CC cs.DM
A Computational Trichotomy for Connectivity of Boolean Satisfiability
对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。2006年，Gopalan等人研究了CSP的解图的连通性和相关的复杂性问题，主要是基于对可满足性算法和可满足性阈值的研究。他们证明了连通分量的直径和st-连通性问题的复杂性的二分法，并为连通性问题建立了一个二分法。在这项工作的基础上，我们在这里证明了连通性：连通性是在P，coNP-完全，或PSPACE-完全。此外，我们纠正了Gopalan等人的一个小错误，这导致边界向硬侧轻微移动。
2015-10-25 cs.CC cs.LO
Complexity of the CNF-satisfiability problem
本文研究布尔可满足性问题的复杂性。我们考虑这个问题的一个版本，其中的布尔公式指定的合取范式。我们证明了一个意想不到的结果，CNF-可满足性问题可以解决的确定性图灵机在多项式时间。
2018-07-20 cs.CC math.CO math.LO
The Complexity of Boolean Constraint Isomorphism
1978年，Schaefer证明了他著名的广义可满足性问题的二分法。他定义了无限多的命题可满足性问题（现在通常称为布尔约束满足问题），并表明，所有这些可满足性问题要么在P或NP完全。近年来，对于布尔约束的其他一些问题也得到了类似的结果，这些问题几乎都是可满足性问题的变形。在本文中，我们解决了一个问题，这不是一个变化的可满足性，即同构问题的布尔约束。Böhler等人先前的工作表明同构问题要么是coNP-难的，要么可简化为图同构问题（一个NP问题，但不知道是NP-难的），从而区分了困难情况和较容易的情况。然而，他们没有分类哪些情况是真正容易的，即，在P中，这篇论文正是这样做的。证明了布尔约束同构是coNP-困难的（和GI-困难的），或等价于图同构，或在P中，并给出了判断哪种情况成立的简单准则。
2004-04-12 cs.CC cs.LO
Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty
随机布尔可满足性（Stochastic Boolean Satisfiability，SSAT）是一种逻辑形式主义，用于建模具有不确定性的决策问题，例如用于概率系统验证的部分可观察马尔可夫决策过程（Partially Observable Markov Decision Process，POMDP）。然而，SSAT受限于其在PSPACE复杂性类中的描述能力。更复杂的问题，如NEXPTIME完全分散POMDP（Dec-POMDP），不能用SSAT简洁地编码。为了提供这样的问题的逻辑形式主义，我们扩展的依赖量化布尔公式（DQBF），在NEXPTIME-完全类的代表性问题，其随机变量，命名为依赖SSAT（DSSAT），并显示DSSAT也是NEXPTIME-完全的。我们展示了DSSAT的潜在应用的概率和近似设计的电路综合。此外，为了研究DSSAT的描述能力，我们建立了从Dec-POMDP到DSSAT的多项式时间约简。随着这项工作的理论基础，我们希望鼓励DSSAT解算器的发展，为潜在的广泛应用。
2021-02-25 cs.CC cs.LO
Gap theorems for robust satisfiability: Boolean CSPs and beyond
当两个不相交的实例集之间没有易处理的边界时，计算问题表现出“间隙性质”。我们建立了一个缺口三分定理的家庭的约束问题的变种，完全分类的复杂性可能的${\bf NP}$ -硬缺口的情况下，布尔域。因此，我们得到了一些二分法的约束满足问题的特定变体的复杂性：所有的多项式时间易处理或$\mathbf{NP}$完成。Schaefer最初对$\textsf{SAT}$变体的二分法是一个值得注意的特例。通用代数方法已中央最近的努力，在分类的复杂性约束满足问题。第二个贡献的文章是发展方面的代数方法的上下文中的一些变种的约束满足问题。特别是，这使我们能够将我们在布尔域上的结果提升到非布尔域上的许多模板。
2017-03-26 cs.CC math.CO math.LO
The Connectivity of Boolean Satisfiability: No-Constants and Quantified Variants
对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。Gopalan等人在Schaefer的框架下，受可满足性和可满足性阈值研究的启发，于2006年研究了解图的连通性和约束满足问题的相关复杂性问题。他们发现了连通分量的直径和st连通性问题的复杂性的二分法，并为我们最近能够证明的连通性问题提出了一个二分法。虽然Gopalan等人考虑了带常数的CNF（S）-公式，但我们在这里研究两个重要的变体：不带常数的CNF（S）-公式和部分量化公式。对于直径和ST-连通性问题，我们证明二分法类似于Gopalan等人。在这些设置。虽然我们还不能给出一个完整的分类的连接问题，我们确定的片段，它是在P，它是coNP完全的，它是PSPACE完全的，在类比Gopalan等人。的脊髓切除术。
2015-10-23 cs.CC cs.LO
Efficient Solution of Boolean Satisfiability Problems with Digital MemComputing
布尔可满足性是多个领域感兴趣的命题逻辑问题，例如，物理学、数学和计算机科学。在研究领域之外，SAT问题的实例，如已知的，在各种应用中需要有效的解决方法。它是决定布尔公式是否具有令人满意的赋值的决策问题，被认为需要指数增长的时间来求解最坏情况的算法。然而，许多类布尔公式的有效解决方案甚至回避了最成功的算法，不仅对于最坏的情况下，而且对于典型的情况下的实例。在这里，我们介绍了一个内存辅助的物理系统（一个数字memcomputing机），当它的非线性常微分方程的数值积分，证明多项式有界的可扩展性，同时解决“硬”种植解决方案的SAT，已知需要指数时间来解决在典型情况下的完整和不完整的算法。此外，我们分析表明，物理系统可以有效地解决SAT问题在连续的时间，而不需要引入混沌或指数增长的能量。模拟的效率与原始物理系统的集体动力学性质有关，这些性质在数值积分中持续存在，即使在存在数值误差的情况下也能鲁棒地引导解搜索。我们预计我们的研究结果，以拓宽物理启发的计算范式的研究方向，从理论到应用，从模拟到硬件实现。
2020-11-12 cond-mat.stat-mech cs.CC cs.ET
Intermediate problems in modular circuits satisfiability
在arXiv：1710.08163中，引入了布尔回路到任意有限代数的推广，并应用于从同余模簇中绘制代数上回路可满足性的P与NP完全边界。然而，幂零代数（尚未被证明是NP-困难的）而非超幂零代数（已被证明是多项式时间的）的问题仍然是开放的。在本文中，我们提供了一个广泛的类别的例子，躺在这个灰色地带，并表明，在指数时间假设和强指数规模假设下，（也就是说布尔电路需要指数级多个模计数门来产生任意元的布尔合取），这些代数上的可满足性具有介于$Ω(2^{c\log^{h-1} n})$和$O(2^{c\log^h n})$之间的中间复杂性，其中$h$度量幂零代数在多大程度上不是超幂零的。我们还概述了如何将这些例子作为范例，以填补一般的幂零与超幂零的差距。我们的例子是惊人的，鉴于电路可满足性和约束满足问题的二分法已被布拉托夫和朱克之间的自然强连接。
2020-05-29 cs.CC
A Polynomial Time Bounded-error Quantum Algorithm for Boolean Satisfiability
本文的目的是回答一个长期存在的开放问题NP和BQP之间的关系。本文通过对MAX-E3-SAT问题这一基本NP难问题的BQP量子算法的提出，证明了BQP包含NP。给定一个E3-CNF布尔公式，MAX-E3-SAT问题的目标是找到最大化满足子句数量的变量分配。对于带有$m$子句的E3-CNF布尔公式，该算法在$O(m^2)$中运行，而对于带有$n$输入的E3-CNF布尔公式，在最坏情况下，该算法在$O(n^6)$中运行。该算法使用一种新的迭代部分否定和部分测量技术最大化满足条款的集合。该算法实现了任意高概率的成功$1-ε$小$ε>0$使用多项式资源。该算法除了求解MAX-E3-SAT问题外，还可以根据满足子句的最大数目来判定E3-CNF布尔公式是否可满足，这是一个NP完全问题。
2015-07-27 cs.CC cs.DS
Connectivity of Boolean Satisfiability
对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。对于这个隐式定义的图，我们在这里研究st-连通性和连通性问题。基于Gopalan et al.（“The Connectivity of Boolean Satisfiability：Computational and Structural Dichotomies”，2006/2009），我们首先研究了由CSP给出的可满足性问题，更确切地说是由带常数的CNF（S）-公式给出的可满足性问题（如Schaefer在1978年著名的二分法定理中所考虑的）;我们证明了ST-连通性问题的计算二分法，断言它要么在多项式时间内可解，要么是PSPACE-完全的，并且是对齐的结构二分法，断言，连接组件的最大直径是线性的变量的数量，或者可以是指数;此外，我们显示了一个连通性问题的剖分，断言它是在P，CONP-完全，或PSPACE-完全。接下来，我们调查两个重要的变种：CNF（S）-公式没有常数，部分量化的公式;在这两种情况下，我们证明了类似的二分法的ST-连接和直径;对于连接问题，我们显示了一个二分法的情况下，量化的公式，而在没有常数的公式的情况下，我们确定一个可能的二分法的片段。最后，我们考虑B-公式的连通性问题，这是任意嵌套的公式建立从一些固定的连接词集B，和B-电路，这是布尔电路的门是从一些有限…
2015-10-22 cs.CC cs.LO
Boolean Satisfiability using Noise Based Logic
在本文中，我们提出了一种新的算法来解决布尔可满足性（SAT）问题，使用基于噪声的逻辑（NBL）。与名称所暗示的相反，NBL不是一个随机/模糊逻辑系统。实际上，它是一个完全确定性的逻辑系统。NBL的一个关键特性是，它允许我们将许多输入向量的叠加同时应用于SAT实例，从而绕过了传统方法中求解SAT的关键限制和假设。通过利用NBL的叠加特性，我们的基于NBL的SAT算法可以确定一个实例是否SAT或不是在一个单一的操作。可以通过迭代地执行SAT检查操作多达n次来找到令人满意的解决方案，其中n是SAT实例中的变量的数量。虽然本文不关注基于NBL的SAT引擎的实现，但可以使用模拟电路（宽带放大器、加法器和乘法器）、FPGA或ASIC来构思这样的引擎。此外，我们还讨论了我们的方法，它可以适用于NBL一般的可扩展性。本文所描述的基于NBL的SAT引擎已经在软件中进行了仿真验证。
2011-10-04 cs.CC cs.DS
Balanced incomplete block designs and exact satisfiability
本文通过用布尔公式的子句和布尔变量区组识别区组设计的点，探讨了平衡不完全区组设计（BIBD）与某些线性CNF公式之间的对应关系。BIBD中的并行类对应于相应公式中的XSAT解决方案。这种对应关系允许将结果从一个字段转移到另一个字段。作为一个新的结果，我们从已知的可满足性定理推导出，在部分平衡的不完全区组设计中寻找平行类的问题是NP完全的。
2020-10-05 cs.CC cs.LO math.CO
Satisfiability in multi-valued circuits
布尔电路的可满足性是理论计算机科学中最著名和最重要的问题之一。这个问题一般是NP完全的，但当限制为单调门或线性门时，就变成了多项式时间。我们去外面的布尔领域，并考虑电路建立的任何固定的一组门在一个任意大的有限域。从复杂性的角度来看，这是严格连接的问题，解决方程（或方程组）的有限代数。在这项工作中的研究报告的动机是希望知道有限代数$\mathbf A$有一个多项式时间的算法，决定如果一个方程在$\mathbf A$有一个解决方案。我们还在寻找多项式时间算法，以确定有限代数上的两个电路是否计算相同的函数。虽然我们还没有设法解决这些问题，在最一般的设置，我们已经获得了这样一个表征一类非常广泛的代数同余模品种。这类代数包括最著名和研究最充分的代数，如群，环，模（及其推广，如拟群，环，近环，非结合环，李代数），格（及其扩展，如布尔代数，海廷代数或其他与多值逻辑连接的代数，包括MV-代数）。本文似乎是第一个系统地研究有限代数上非布尔电路可满足性和解方程的计算复杂性。本文给出的刻画结果是根据代数的良好结构性质给出的，使得问题在多项式时间内可解。
2017-10-23 cs.CC
From Hall's Marriage Theorem to Boolean Satisfiability and Back
受Hall婚姻定理在各种LP舍入问题中的应用的启发，我们引入了经典婚姻问题（CMP）的推广，我们称之为分数婚姻问题。我们证明了分数婚姻问题是NP-完全的减少从布尔可满足性（SAT）。我们表明，当我们看到经典的婚姻问题（a.k.a.二分匹配）作为SAT的子类，我们得到了一类新的多项式时间可满足SAT实例，我们称之为CMP-SAT，它不同于经典的多项式时间可满足SAT实例2-SAT，Horn-SAT和XOR-SAT。接下来，我们转向识别CMP-SAT实例的问题，首先使用SAT嵌入，然后在分数婚姻问题（FMP）的范围内使用它们的嵌入。在这个过程中，我们导致另一个推广的CMP，我们称之为对称婚姻问题，这是多项式时间判定，并导致轻微扩大的CMP-SAT类。我们开发了一个框架，用于简化FMP问题，以确定CMP实例，我们称之为片段逻辑。最后，我们给出了一个结果，揭示了如何表达的FMP需要仍然是NP完全的。结果给出了FMP的第二个NP完全约简，这次是三分匹配。最后，我们提出了各种各样的其他问题。
2019-05-07 cs.CC math.CO
On Theoretical Complexity and Boolean Satisfiability
The American University in Cairo（开罗美国大学）
理论复杂性是计算机科学的一个重要分支，它使我们能够从数学上研究计算并回答许多关于计算问题本质的有趣问题。它提供了理论工具来评估计算的时间和空间要求，以及评估问题的难度-相应地对它们进行分类。它也收藏在其核心的一个最重要的问题，在数学，即，$\textbf{P vs. NP}$千年问题。从本质上讲，这个问题问的是解决方案和验证是否存在于两个不同的难度水平上。在这篇论文中，我们介绍了计算理论中的一些最核心的概念，概述了如何使用图灵机来抽象计算。此外，我们介绍了两个最著名的问题复杂性类$\textbf{P}$和$\textbf{NP}$以及它们之间的关系。此外，我们阐述了问题减少的概念，以及它是如何在不同问题之间进行硬度比较的重要工具。随后，我们提出了问题的布尔可满足性（SAT），这是在NP完全问题的中心。然后，我们探讨它的一些易处理的，以及棘手的变种，如角SAT和3-SAT，分别。最后，我们建立了从3-SAT到一些著名的NP-完全图问题的多项式时间约简，即团发现，Hamilton圈发现和3-着色。
2021-12-22 cs.CC cs.CL
Pairs of SAT Assignment in Random Boolean Formulae
我们调查的几何性质的随机K-可满足性问题使用的概念x-可满足性：一个公式是x-可满足的，如果存在两个SAT分配不同的Nx变量。我们证明了存在一个尖锐的阈值作为子句密度的函数，这个属性。对于足够大的K，我们证明了存在一个区域的子句密度，低于可满足性阈值，其中SAT分配之间的汉明距离的景观经历了一个间隙：SAT分配对存在于小x，和周围x=1/2，但它们不存在于中间值的x。这一结果是一致的聚类方案，这是在最近的启发式分析的可满足性，使用统计物理分析（空腔方法），其算法（调查传播算法）的核心。该方法使用基本的概率参数（一阶矩和二阶矩方法），并可能是有用的，在其他问题的计算和物理感兴趣的类似现象出现。
2007-09-19 cond-mat.dis-nn cs.CC
On the Hardness of Satisfiability with Bounded Occurrences in the Polynomial-Time Hierarchy
$ \newcommand{\eps}ε \newcommand{\NP}{\mathsf{NP}} \newcommand{\YES}{\mathsf{YES}} \newcommand{\NO}{\mathsf{NO}} \newcommand{\myminus}{\text{-}}\newcommand{\Bsat}{\mathsf{B}} \newcommand{\threesat}{\rm{3}\myminus\mathsf{SAT}} \newcommand{\gapthreesat}{\mathsf{\forall\exists}\myminus{\rm{3}}\myminus\mathsf{SAT}} $在1991年，Papadimitriou和Yannakakis给出了一个减少意味着$\NP$ -硬度近似问题$\threesat$有界的发生。他们的减少是基于扩展图。我们提出了一个模拟的多项式时间层次结构的基础上超集中器图的第二个层次的结果。这解决了Ko和Lin（1995）的一个未解决的问题，并且在导出多项式时间层次中的不可逼近性结果时应该是有用的。更准确地说，我们表明，给定一个$\gapthreesat$的实例，其中每个变量最多出现$\Bsat$次（对于某个绝对常数$\Bsat$），它是$Π_2$ -很难区分以下两种情况：$\YES$实例，其中对于对泛变量的任何赋…
2018-06-11 cs.CC
EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness
已知乘积逻辑K4 xS 5和S4 xS 5的可满足性问题是NEXPTIME-困难的，子集空间的逻辑SSL的可满足性问题是PSPACE-困难的。我们提高这些问题的复杂性的下限，表明这三个问题是EXPSPACE-硬下的对数空间减少。在另一篇论文中，我们表明，这些问题是在ESPACE。这表明这三个问题都是EXPSPACE完备的。
2019-08-09 cs.CC cs.LO math.LO
Polynomial Time Algorithm for Boolean Satisfiability Problem
本文证明集合特殊覆盖相关算法过程具有多项式时间复杂度，并提出一个判定 CNF 布尔函数可满足性的多项式时间算法，其复杂度以输入长度立方为上界，且在 Python 实现中通过了数万变量和从句规模的测试。
2023-10-28 cs.CC
The Complexity of Planar Counting Problems
我们证明了与各种可满足性，图形和组合问题，当限制到平面的情况下，计数问题的#P-硬度。这些问题包括\begin{romannum} \item[{}] {\sc 3Sat, 1-3Sat, 1-Ex3Sat, Minimum Vertex Cover, Minimum Dominating Set, Minimum Feedback Vertex Set, X3C, Partition Into Triangles, and Clique Cover.} \end{romannum}我们还证明了{\sf NP}-完备性的{ \sc Ambiguity Satisfiability}问题\cite{Sa80}和{ \sf D $^P$ }-完备性（相对于随机多项式约简）的唯一可满足性问题\cite{VV85}与上述几个问题，当限制到平面的情况。以前，很少{ \sf #P}-硬度的结果，没有{ \sf NP}-硬度的结果，没有{ \sf D $^P$ }-完整性的结果是已知的计数问题，模糊的可满足性问题和唯一的可满足性问题，分别限制到平面的实例。假设{ \sf P $\neq $ NP}，上述结果的一个推论是：对于整数上线性不等式约束的平面线性目标函数的最大化或最小化问题，没有$ε$ -近似算法.
1998-09-11 cs.CC cs.DM
The 2CNF Boolean Formula Satisfiability Problem and the Linear Space Hypothesis
研究以变量总数为参数的2CNF布尔公式可满足性问题，提出线性空间假设（LSH），指出特定2CNF问题无法在多项式时间内用亚线性空间求解，并借助短归约概念证明相关问题类的封闭性。
2023-03-07 cs.CC
Hardness of equations over finite solvable groups under the exponential time hypothesis
Goldmann和Russell（2002）开始研究有限群中方程可满足性问题的复杂性，证明了对于幂零群它是在P中，而对于不可解群它是NP-完全的。从那时起，出现了几个结果表明，该问题可以解决在多项式时间在某些可解群的拟合长度为2。在这项工作中，我们提出了有限可解群中方程可满足性问题的第一个下界：在指数时间假设的假设下，我们证明了对于任何Fitting长度至少为4的群和某些Fitting长度为3的群，它不能在P中。此外，同样的困难的结果适用于方程恒等式问题。
2020-10-26 cs.CC math.GR
NEXP-completeness and Universal Hardness Results for Justification Logic
我们提供了一个较低的复杂性约束的多智能体的理由逻辑的可满足性问题，建立从我们以前的工作一般NEXP上限是紧的。然后，我们使用一个简单的修改相应的减少证明，满足所有多代理的理由逻辑从那里是很难的西格玛2 p类的第二层次的多项式-给定某些合理的条件。我们的方法改进了这些所需的条件，为同一个下界的单代理的理由逻辑，证明了巴斯和库兹涅茨在2009年，从而回答了他们的一个开放的问题。
2015-03-01 cs.CC cs.LO
Satisfiability of commutative vs. non-commutative CSPs
本研究将布尔CSP的经典与算子可满足性间隙分类推广到任意有限域，证明NP难CSP存在间隙，有界宽度易解CSP无间隙，无界宽度易解CSP可模拟素数阶阿贝尔群线性方程并产生间隙。
2025-09-11 cs.CC cs.LO quant-ph
Generalized Satisfiability for the Description Logic ALC
基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。我们分类的复杂性标准可满足性问题的所有可能的布尔和量词片段的ALC中存在的一般公理。
2011-03-04 cs.CC cs.LO
Boolean PCSPs through the lens of Fourier Analysis
Jagiellonian University（雅盖隆大学）；University of Warsaw（华沙大学）
本文通过傅里叶分析研究布尔承诺约束满足问题，发现坐标影响的保持性和尖锐阈值现象，揭示了布尔矿工的硬度与可处理性。
2026-10-30 cs.CC
The number system hidden inside the Boolean satisfiability problem
本文给出了一种更深入分析SAT问题的新方法。首先，我定义了布尔公式的新元素，如主导变量，决策链和链耦合器。通过分析SAT问题的元素，我证明了我们可以构建一个k-SAT（k>2）的例子，其中的切割平面的系数采取指数大的值在输入大小。这种指数性质是由系数计算形成的数字系统引起的。另外，本文还证明了2-SAT不构成数制，而Horn-SAT根据主导变量的可行值部分地构成数制。割平面证明中的割平面系数是否多项式有界一直是一个悬而未决的问题。许多研究人员认为，具有大系数的切割平面证明是非常不直观的20。然而，我们可以构造一个k-SAT（k>2）实例，其中切割平面采用指数大系数的数字系统。此外，这种指数性质是如此强大，它给出了几个问题的明确答案：为什么Horn-SAT具有2-SAT和3-SAT之间的中间性质;为什么随机SAT如此容易;为什么k-SAT（k>2）不能用线性规划技术解决。2-SAT是NL-完全的，Horn-SAT是P-完全的，k-SAT（k>2）是NP-完全的。本文从计算复杂性的角度给出了一个明确的数学性质，并以此区分三类SAT问题。
2018-01-24 cs.CC math.LO
Optimal Testing for Planted Satisfiability Problems
研究了随机可满足性公式中种植解的检测问题。采用统计分析中假设检验的形式，描述了极小极大最优检测率。我们的分析依赖于满意的分配，我们证明了新的结果的数量的研究。我们还解决了算法问题，并给出了一个计算效率的测试与最佳的统计性能。这一结果相比，平均情况下的假设的硬度反驳随机公式的可满足性。
2015-02-08 cs.CC math.PR math.ST
When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames
Universität Tübingen（蒂宾根大学）；Leibniz Universität Hannover（汉诺威莱布尼茨大学）
本文证明了在S5框架下，受限于XOR和1连接词的仿射ML-SAT问题为NP难性。
2025-12-19 cs.CC cs.LO
Efficient Analog Circuits for Boolean Satisfiability
NP完全问题的有效解决方案将使科学和工业都受益匪浅。然而，这样的问题在基于冯·诺依曼体系结构的数字计算机上是难以处理的，因此产生了对解决这样的问题的替代解决方案的需要。最近，提出了确定性连续时间动力系统（CTDS）（Nat.Phys. { \bf 7}（12），966（2011））以解决代表性NP完全问题，布尔可满足性（SAT）。该求解器显示了多项式模拟时间复杂性，即使是最难的基准$k$ -SAT（$k \geq 3$）公式，但通过指数驱动的辅助变量的能量成本。本文提出了一种新的模拟硬件SAT求解器，AC-SAT，实现CTDS通过纳入新的，模拟电路设计思想。AC-SAT旨在用作协处理器，并可编程以处理不同的问题规格。这是特别有效的解决硬$k$ -SAT问题的情况下，是具有挑战性的算法在数字机器上运行。此外，凭借其模块化设计，AC-SAT可以很容易地扩展到解决更大规模的问题，而电路的大小与变量的数量和条款的数量的乘积线性增长。该电路基于32 nm CMOS工艺进行了设计和仿真。SPICE模拟结果显示，与数字计算机上的最先进的SAT求解器相比，即使是最难的3-SAT问题，$\sim$ 10 $^4$的加速因子。例如，对于具有$N=50$变量和$M=212$子句的难题，在几个$ns$到几百个$ns$内找到解决方案。
2018-02-11 cs.CC cs.ET physics.ins-det
Satisfiability Parsimoniously Reduces to the Tantrix(TM) Rotation Puzzle Problem
Holzer和Holzer（Discrete Applied Mathematics 144（3）：345- 358，2004）证明了TanjetTM旋转难题是NP完全的。他们还表明，对于无限旋转难题，这个问题变得不可判定。我们研究这个问题的计数版本和唯一版本。我们证明了可满足性问题简约地归结为Tanjanet（TM）旋转难题。特别是，这种约简保持了解的唯一性，这意味着唯一TanjetTM旋转难题与唯一可满足性问题一样困难，并且在多项式时间随机约简下也是DP完全的，其中DP是NP上布尔层次的第二层。
2008-06-09 cs.CC
The complexity of counting solutions to Generalised Satisfiability Problems modulo k
广义可满足性问题（或称布尔约束满足问题）是由Schaefer于1978年提出的一种广义可满足性问题，它允许系统地研究具有不同类型约束的可满足性问题的复杂性。1979年，Valiant引入了复杂性类奇偶性P，即计算模2的NP问题的解的个数的问题。其他人已经考虑了对其他整数取模计数的问题。我们给出了一个二分法定理的复杂性计数的解决方案的数量的广义可满足性问题模整数。这是从早期的结果Credilu和赫尔曼这给了计数二分法这些类型的问题，和二分法本身几乎是相同的。具体地说，如果所有的关系都是仿射的，那么计算广义可满足性问题的解的个数可以在多项式时间内完成。否则，除了k = 2的特殊情况外，它是#_kP-完全的。
2008-09-10 cs.CC
Dichotomy Theorems for Alternation-Bounded Quantified Boolean Formulas
1978年，Schaefer证明了他著名的广义可满足性问题的二分法。他定义了无限多的命题可满足性问题，表明所有这些问题要么在P或NP-完全，并给出了一个简单的标准，以确定这两种情况下举行。根据拉德纳定理，这个结果是令人惊讶的，拉德纳定理意味着在P和NP完全之间有无限多的复杂性类（假设P不等于NP）。Schaefer还提出了一个量化的广义布尔公式的二分法定理，但这一定理最近才被Creamou、Khanna和Sudan证明，并由Dalmau独立证明：确定量化的布尔公式的真值要么是PSPACE-完全的，要么是P中的。在其不受限制的形式，这些问题是典型的问题完成的多项式层次的水平。本文证明了交替有界量化广义布尔公式的二分法，证明了这些问题是$Σ_i^p$ -完全的或在P中的，并给出了判定哪种情况成立的简单准则.这是第一个结果，获得二分法的无限数量的类一次。
2004-06-02 cs.CC cs.LO
Polynomial-time satisfiability for a special case of Positive$\wedge$Negative
Department of Mathematical Sciences, University of Stellenbosch（斯泰伦博斯大学数学科学学院）
针对一类子句互不相交的正负CNF（DisjointPositive∧DisjointNegative），提出二次时间可满足性判定算法，并能在多项式总时间内输出所有模型，该结果适用于Horn∧AntiHorn型CNF及单调布尔网络不动点问题。
2026-06-27 cs.CC math.LO
Detection of Planted Solutions for Flat Satisfiability Problems
University of Cambridge（剑桥大学）；University of Wisconsin, Madison（威斯康星大学麦迪逊分校）
我们研究了在随机情况下的平面可满足性问题，布尔可满足性公式的推广寻找种植解决方案的检测问题。我们描述的属性的随机情况下，平坦的可满足性，以及相关的假设检验问题的最佳检测率。我们还研究了算法有效的测试过程的性能。我们介绍了我们的模型的修改，光种植的解决方案，并表明，这是很难的学习奇偶噪声的问题。这强烈暗示了检测种植平坦可满足性对于广泛的测试类的困难。
2019-03-06 cs.CC cs.LG math.ST
New Algorithms and Hardness Results for Robust Satisfiability of (Promise) CSPs
UC Berkeley（加州大学伯克利分校）；TU Graz（格拉茨工业大学）；Simons Institute and UC Berkeley（西蒙斯研究所和加州大学伯克利分校）；University of Chicago（芝加哥大学）；University of Oxford（牛津大学）
本文提出了针对承诺CSPs鲁棒可满足性的新算法，并在UGC假设下证明了相关结果。
2026-02-10 cs.CC cs.DS cs.LO
Three complete deterministic polynomial algorithms for 3SAT
给出了三种判定3SAT布尔可满足性表达式满足赋值存在性的算法。一个算法是确定一个令人满意的分配的情况下，这样的存在。每个算法都是确定性的和多项式的复杂性。确定存在性的算法是完整的，因为每个算法都产生一个不可满足性证书，例如不存在满意的分配，并且这种分配的可满足性确实存在。
2019-12-13 cs.CC
Special Coverings of Sets and Boolean Functions
本文引入集合的特殊分解与特殊覆盖概念，证明布尔可满足性问题与集合特殊覆盖存在性多项式等价，后者为NP完全问题，并研究可满足函数的生成关系与等价类划分。
2025-03-29 cs.CC
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
What makes normalized weighted satisfiability tractable
We consider the weighted antimonotone and the weighted monotone satisfiability problems on normalized circuits of depth at most $t \geq 2$ , abbreviated { \sc wsat $^-[t]$ } and { \sc wsat $^+[t]$ }, respectively. These problems model the weighted satisfiability of antimonotone and monotone propositional formulas (including weighted anitmonoone/monotone { \sc cnf-sat}) in a natural way, and serve as the canonical problems in the definition of the parameterized complexity hierarchy. We characterize the parameterized complexity of { \sc wsat $^-[t]$ } and { \sc wsat $^+[t]$ } with respect to the…
2011-12-05 cs.CC
The Satisfiability Threshold for Non-Uniform Random 2-SAT
命题可满足性是计算机科学中最基本的问题之一。它的最坏情况困难是计算复杂性理论的核心，例如NP-困难和（强）指数时间假设。然而，在实践中，SAT实例通常可以有效地解决。这种矛盾的行为已经引起了人们对SAT平均情况分析的兴趣，并引发了复杂的严格和非严格技术的发展，用于分析随机结构。尽管有很长的研究和实质性的进展，大多数关于随机SAT的理论工作都假设变量均匀分布。相比之下，真实世界的实例经常在变量出现时表现出很大的波动。这可以通过变量的非均匀分布来建模，这可能导致分布更接近工业SAT实例。本文研究了具有$n$变量和$m$子句的非均匀随机$2$-SAT的可满足性阈值，以及具有任意概率分布的$(p_i)_{i\in[n]}$和n个变量上的$p_1 \ge p_2 \ge \ldots \ge p_n > 0$的可满足性阈值。我们证明了$p_1^2=Θ(\sum_{i=1}^n p_i^2)$的渐近可满足性阈值是在$m=Θ( (1-\sum_{i=1}^n p_i^2)/(p_1\cdot(\sum_{i=2}^n p_i^2)^{1/2}) )$，它是粗糙的。对于$p_1^2=o(\sum_{i=1}^n p_i^2)$，我们表明，有一个尖锐的可满足性阈值在$m=(\sum_{i=1}^n p_i^2)^{-1}$。这一结果推广了Chvatal和Reed [FOCS 1992]和Goerdt…
2022-08-31 cs.CC cs.DM
What makes a phase transition? Analysis of the random satisfiability problem
在过去的30年里，人们发现许多组合系统都经历了相变。其中一个最重要的例子可以在随机k-可满足性问题（通常称为k-SAT）中找到，询问是否存在满足布尔公式的布尔值的赋值，该布尔公式由每个子句具有k个随机变量的子句组成。随机3-SAT问题在子句数与变量数之比的不同临界值下表现出不同的相变。其中最著名的是当找到可满足实例的概率突然从1下降到0时。这种转变与问题的硬度上升有关，但到目前为止，所提出的任何相变与硬度之间的相关性还不完全清楚。在本文中，我们将首先数值表明，解决方案的数量普遍遵循对数正态分布，从而解释了令人困惑的问题，为什么解决方案的数量仍然是指数在临界点。此外，我们提供的证据表明，硬度的密切相关的问题，计数的解决方案的总数并没有表现出任何相变样的行为。这就提出了一个问题，即找到一个可满足实例的概率是否真的是一个相变的序参量，或者它是否更有可能只是显示一个简单的尖锐阈值现象。更一般地说，本文旨在开始讨论一个简单的尖锐的阈值现象变成一个真正的相变。
2010-02-01 cs.CC physics.comp-ph physics.data-an
Learning-Augmented Algorithms for Boolean Satisfiability
Institute for Data, Econometrics, Algorithms, and Learning (IDEAL)（数据、计量经济学、算法和学习研究所）；University of Illinois at Chicago（伊利诺伊大学芝加哥分校）；Toyota Technological Institute at Chicago（芝加哥丰田技术研究所）
本文在学习增强框架下研究布尔可满足性（SAT）判定与优化问题，利用子集建议和标签建议两种形式，加速了PPSZ算法的指数运行时间，并以黑盒方式改进了任意α-近似算法的近似比，在MAX-2-SAT等问题上取得更优表现。
2025-05-30 cs.CC cs.DS cs.LG
