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
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
The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies
布尔可满足性问题是研究复杂性、算法、数学和阈值现象的重要基准。最近的工作，可满足性的阈值已集中在结构和连通性的解决方案空间。受这项工作的启发，我们研究了布尔可满足性问题的解空间的结构和连通性相关的性质，并在Schaefer的框架下建立了各种二分法。在结构方面，我们得到的二分法的超立方体的子图，可以引起的解决方案的布尔公式，以及直径的连通组件的解决方案空间。在计算方面，我们建立二分法定理的复杂性的连接性和st-连接性问题的图形的解决方案的布尔公式。我们的研究结果断言，计算二分法的棘手的一面是PSPACE-完全的，而易处理的一面-这包括但不限于所有问题的多项式时间算法的可满足性-是在P的ST-连接问题，并在coNP的连接问题。对于PSPACE完备的情况，组件的直径可以是指数的，而在所有其他情况下，它是线性的;因此，小直径和连通性问题的易处理性是显着一致的。我们的结果的关键是一个可表达性定理表明，在易处理的情况下，由解空间诱导的子图具有一定的良好的结构性质，而在棘手的情况下，子图可以是任意的。
2007-10-03 cs.CC
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
The Boolean SATisfiability Problem in Clifford algebra
我们提出了一个制定的布尔可满足性问题的旋量语言，允许给一个必要和充分条件的不可满足性。有了这个结果，我们概述了一个算法来测试可能有趣的理论性质的不可满足性。
2018-05-17 cs.CC math-ph math.MP
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
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
Necessary and sufficient conditions for Boolean satisfiability
该研究作为P与NP复杂度类关系系列研究的第二篇，借助集合特殊覆盖概念证明其与布尔可满足性问题等价，得出布尔可满足性的充要算法条件，还能得到满足可满足性的变量取值。
2023-11-05 cs.CC cs.DM
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
A Computational Trichotomy for Connectivity of Boolean Satisfiability
对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。2006年，Gopalan等人研究了CSP的解图的连通性和相关的复杂性问题，主要是基于对可满足性算法和可满足性阈值的研究。他们证明了连通分量的直径和st-连通性问题的复杂性的二分法，并为连通性问题建立了一个二分法。在这项工作的基础上，我们在这里证明了连通性：连通性是在P，coNP-完全，或PSPACE-完全。此外，我们纠正了Gopalan等人的一个小错误，这导致边界向硬侧轻微移动。
2015-10-25 cs.CC cs.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
Satisfiability in multi-valued circuits
布尔电路的可满足性是理论计算机科学中最著名和最重要的问题之一。这个问题一般是NP完全的，但当限制为单调门或线性门时，就变成了多项式时间。我们去外面的布尔领域，并考虑电路建立的任何固定的一组门在一个任意大的有限域。从复杂性的角度来看，这是严格连接的问题，解决方程（或方程组）的有限代数。在这项工作中的研究报告的动机是希望知道有限代数$\mathbf A$有一个多项式时间的算法，决定如果一个方程在$\mathbf A$有一个解决方案。我们还在寻找多项式时间算法，以确定有限代数上的两个电路是否计算相同的函数。虽然我们还没有设法解决这些问题，在最一般的设置，我们已经获得了这样一个表征一类非常广泛的代数同余模品种。这类代数包括最著名和研究最充分的代数，如群，环，模（及其推广，如拟群，环，近环，非结合环，李代数），格（及其扩展，如布尔代数，海廷代数或其他与多值逻辑连接的代数，包括MV-代数）。本文似乎是第一个系统地研究有限代数上非布尔电路可满足性和解方程的计算复杂性。本文给出的刻画结果是根据代数的良好结构性质给出的，使得问题在多项式时间内可解。
2017-10-23 cs.CC
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
Complexity of the CNF-satisfiability problem
本文研究布尔可满足性问题的复杂性。我们考虑这个问题的一个版本，其中的布尔公式指定的合取范式。我们证明了一个意想不到的结果，CNF-可满足性问题可以解决的确定性图灵机在多项式时间。
2018-07-20 cs.CC math.CO math.LO
Polynomial Time Algorithm for Boolean Satisfiability Problem
本文证明集合特殊覆盖相关算法过程具有多项式时间复杂度，并提出一个判定 CNF 布尔函数可满足性的多项式时间算法，其复杂度以输入长度立方为上界，且在 Python 实现中通过了数万变量和从句规模的测试。
2023-10-28 cs.CC
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
The 2CNF Boolean Formula Satisfiability Problem and the Linear Space Hypothesis
研究以变量总数为参数的2CNF布尔公式可满足性问题，提出线性空间假设（LSH），指出特定2CNF问题无法在多项式时间内用亚线性空间求解，并借助短归约概念证明相关问题类的封闭性。
2023-03-07 cs.CC
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
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
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
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
Three complete deterministic polynomial algorithms for 3SAT
给出了三种判定3SAT布尔可满足性表达式满足赋值存在性的算法。一个算法是确定一个令人满意的分配的情况下，这样的存在。每个算法都是确定性的和多项式的复杂性。确定存在性的算法是完整的，因为每个算法都产生一个不可满足性证书，例如不存在满意的分配，并且这种分配的可满足性确实存在。
2019-12-13 cs.CC
Order-to-chaos transition in the hardness of random Boolean satisfiability problems
瞬态混沌是一种普遍存在的现象，其特征在于相空间轨迹的动力学朝着流体、化学反应和凝聚态系统等不同物理系统中的稳态吸引子演化。在这里，我们表明，瞬态混沌也出现在某些有效的算法的动态搜索解决方案的约束满足问题，包括调度，电路设计，布线，数据库问题，甚至数独。特别是，我们提出了一个研究的硬度出现在布尔可满足性（$k$ -SAT），一类典型的约束满足问题，通过使用一个模拟确定性算法的基础上的常微分方程组。通过逃逸率$κ$定义了问题的困难度，$κ$是动力系统瞬态混沌的一个不变测度，它表示了轨迹接近解的速率，我们证明了对于给定的约束密度和固定数目的布尔变量$N$，随机$k$ -SAT系综中公式的困难度有很大的变化，可近似为对数正态分布。我们还表明，当增加密度的约束$α$，硬度出现通过二阶相变在$α_χ$在随机3-SAT系综的动力学轨迹成为瞬态混沌。在4-SAT中也发现了类似的行为，然而，对于2-SAT不发生这种转变。这种行为也意味着一种新型的瞬态混沌，其中逃逸率与临界参数$κ\sim N^{B|α- α_χ|^{1-γ}}$和$0< γ< 1$具有指数-代数关系。我们表明，过渡所产生的亚稳态盆地的外观在解空间中的约束$α$的密度增加。
2016-04-20 cond-mat.stat-mech cs.CC
Special Coverings of Sets and Boolean Functions
本文引入集合的特殊分解与特殊覆盖概念，证明布尔可满足性问题与集合特殊覆盖存在性多项式等价，后者为NP完全问题，并研究可满足函数的生成关系与等价类划分。
2025-03-29 cs.CC
Efficient Solution of Boolean Satisfiability Problems with Digital MemComputing
布尔可满足性是多个领域感兴趣的命题逻辑问题，例如，物理学、数学和计算机科学。在研究领域之外，SAT问题的实例，如已知的，在各种应用中需要有效的解决方法。它是决定布尔公式是否具有令人满意的赋值的决策问题，被认为需要指数增长的时间来求解最坏情况的算法。然而，许多类布尔公式的有效解决方案甚至回避了最成功的算法，不仅对于最坏的情况下，而且对于典型的情况下的实例。在这里，我们介绍了一个内存辅助的物理系统（一个数字memcomputing机），当它的非线性常微分方程的数值积分，证明多项式有界的可扩展性，同时解决“硬”种植解决方案的SAT，已知需要指数时间来解决在典型情况下的完整和不完整的算法。此外，我们分析表明，物理系统可以有效地解决SAT问题在连续的时间，而不需要引入混沌或指数增长的能量。模拟的效率与原始物理系统的集体动力学性质有关，这些性质在数值积分中持续存在，即使在存在数值误差的情况下也能鲁棒地引导解搜索。我们预计我们的研究结果，以拓宽物理启发的计算范式的研究方向，从理论到应用，从模拟到硬件实现。
2020-11-12 cond-mat.stat-mech cs.CC cs.ET
Generalized Satisfiability for the Description Logic ALC
基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。我们分类的复杂性标准可满足性问题的所有可能的布尔和量词片段的ALC中存在的一般公理。
2011-03-04 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
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
Faster Random $k$-CNF Satisfiability
我们描述了一个算法，以解决问题的布尔CNF-可满足性时，输入公式是随机选择。我们建立在Sch{<$}ning 1999和Dantsin等人的算法之上。2002年Sch{ö}ning算法的工作原理是尝试许多可能的随机分配，并针对每个分配在该分配的附近系统地搜索满意的解决方案。这个问题的以前的算法在时间上运行$O(2^{n (1- Ω(1)/k)})$。我们的改进很简单：我们计算每个随机抽样的分配满足了多少子句，并且仅在具有异常多的满足子句的分配的邻域中搜索。我们发现，像这样的任务更有可能接近一个令人满意的任务。这一改进节省了$2^{n Ω(\lg^2 k)/k}$因子，导致随机$k$ -SAT的总运行时间为$O(2^{n (1- Ω(\lg^2 k)/k)})$。
2019-03-25 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
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
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
Compression with wildcards: All models of a Boolean 2-CNF
提出 A-I-I 算法，以使用无关符号的压缩格式枚举偏序集的图独立序理想，可并行化并适应多项式总时间算法枚举布尔 2-CNF 模型集，在多项实例中优于 Mathematica 内置命令。
2025-04-06 cs.CC
The Complexity of Monotone Hybrid Logics over Linear Frames and the Natural Numbers
带绑定器的混合逻辑是一种表达性很强的规约语言。它的可满足性问题一般是不可判定的。如果框架被限制为N阶或一般的线性阶，则可满足性是可判定的，但具有非初等的复杂性。在本文中，我们考虑单调混合逻辑（即，布尔连接词仅为合取和析取）在N和一般线性阶上。我们证明了可满足性问题在线性阶上仍然是非初等的，但其复杂性下降到N上的PSPACE完备性。我们分类严格的片段所产生的不同组合的模式和混合操作到NP-完全和易处理的（即完整的NC 1或LOGSPACE）。有趣的是，NP完全性只依赖于片段而不依赖于框架。对于NP以上的情况，线性阶上的可满足性比N上的可满足性更难，而在NP以下，它最多是一样难。此外，我们研究模型理论的有关片段的属性。
2012-06-12 cs.CC
Detection of Planted Solutions for Flat Satisfiability Problems
University of Cambridge（剑桥大学）；University of Wisconsin, Madison（威斯康星大学麦迪逊分校）
我们研究了在随机情况下的平面可满足性问题，布尔可满足性公式的推广寻找种植解决方案的检测问题。我们描述的属性的随机情况下，平坦的可满足性，以及相关的假设检验问题的最佳检测率。我们还研究了算法有效的测试过程的性能。我们介绍了我们的模型的修改，光种植的解决方案，并表明，这是很难的学习奇偶噪声的问题。这强烈暗示了检测种植平坦可满足性对于广泛的测试类的困难。
2019-03-06 cs.CC cs.LG math.ST
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
Enhanced Fast Boolean Matching based on Sensitivity Signatures Pruning
Peking University（北京大学）；Peng Cheng Laboratory（鹏城实验室）
布尔匹配在数字集成电路设计中具有重要意义。用于布尔匹配的穷举方法即使对于仅具有几个变量的函数在计算上也是昂贵的，因为用于n变量布尔函数的这种算法的时间复杂度是$O(2^{n+1}n!)$。灵敏度是布尔函数的一个重要特性，也是布尔函数复杂性的一个度量。它已被用于分析算法的复杂性在不同的领域。该测度可以看作是布尔函数的一种签名，在缩小布尔匹配的搜索空间方面具有很大的潜力。在本文中，我们将布尔敏感性引入到布尔匹配中，并设计了几个敏感性相关的签名，以提高快速布尔匹配。首先，我们提出了一些新的签名，涉及敏感性布尔等价。然后，我们证明了这些签名是布尔匹配的先决条件，我们可以使用它来减少匹配问题的搜索空间。此外，我们发展了一个快速的灵敏度计算方法来计算和比较两个布尔函数的这些签名。与传统的余因子和对称检测方法相比，灵敏度是一系列特征的另一个维度。我们还表明，灵敏度可以很容易地集成到传统的方法和区分不匹配的布尔函数更快。据我们所知，这是第一个工作，介绍了布尔匹配的敏感性。实验结果表明，本文提出的敏感度相关签名可以在很大程度上减少搜索空间，并执行高达3倍的加速比最先进的布尔匹配方法。
2021-11-11 cs.AI cs.CC
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
Geometrical organization of solutions to random linear Boolean equations
随机XORSAT问题处理布尔变量的大型随机线性系统。这类问题的难度由方程数与变量数的比值控制。已知在该参数的某些值范围内，解的空间分裂成许多不连通的簇。在这里，我们研究正是相应的几何组织。特别是，这些集群之间的距离分布计算的空腔方法。这允许研究“x-可满足性”阈值，即在给定距离处存在两个解的方程的临界密度。
2006-09-05 cond-mat.dis-nn cs.CC
Computational Complexity of Quantum Satisfiability
量子逻辑是由加勒特·伯克霍夫和约翰·冯·诺依曼在1936年提出的，作为捕捉量子可观测量的逻辑特性的框架。它推广了布尔命题逻辑，并且在一维希尔伯特空间上与布尔命题逻辑相吻合。介绍了量子逻辑项的弱可满足性和强可满足性问题。在二维空间中，两者都是NP完全的。另一方面，对于d>2固定的高维空间R^d和C^d，我们证明了这两个问题对于实计算的非确定性Blum-Shub-Smale模型是完备的。这提供了一个统一的观点图灵和真正的BSS复杂性理论，并扩展了仍然相对稀缺的家庭NP_R-完全的问题，其中一个可能最接近的精神，以经典的库克-莱文定理。我们对弱/强可满足项的维数的研究导致了不定维、有限维和无穷维的可满足性问题。这里，强可满足性证明为多项式时间等价于非交换整数多项式方程的可行性
2012-11-12 cs.CC math.LO
Model Counting for Dependency Quantified Boolean Formulas
National Taiwan University（台湾大学）；University of Liverpool（利物浦大学）
本文研究依赖量化布尔公式（DQBF）的模型计数问题，证明#2-DQBF是#EXP完全的，并开发专用2-DQBF模型计数器，实验显示其在大依赖集场景下扩展性优于基线方法。
2025-11-15 cs.CC cs.LO
A Critique of a Polynomial-time SAT Solver Devised by Sergey Gubin
本文反驳了Sergey Gubin提出的求解可满足性的多项式时间算法的有效性。Gubin介绍了使用3-SAT的算法，并最终将其扩展到接受各种形式的布尔可满足性问题。因为3-SAT是NP-完全的，所以如果算法是正确的，它将意味着P = NP。此外，本文还反驳了他的多项式时间约化SAT为2-SAT的正确性。
2008-04-16 cs.CC cs.DS
Symmetric Promise Constraint Satisfaction Problems: Beyond the Boolean Case
承诺约束满足问题（Promise Constraint Satisfaction Problem，PCSP）是约束满足问题（Constraint Satisfaction Problem，CSP）的一个推广。我们调查的计算复杂性的一类PCSP超出了大多数研究的情况下，可满足性和图着色问题的近似变量。我们给出了一类PCSP的几乎完全分类的形式：给定一个3-一致超图，有一个容许的2-染色，找到一个容许的3-染色，其中容许性是由三元对称关系。这类PCSP中唯一一个复杂性在本书中没有讨论的是一个自然超图着色问题，其中的容许性由以下关系给出：“如果两种颜色相等，则剩下的一种颜色更高。"
2020-10-09 cs.CC math.LO
Deciding One to One property of Boolean maps: Condition and algorithm in terms of implicants
本文针对布尔映射可逆性判定问题，提出基于蕴含项的条件，并推广至一般映射，为二元域上的可逆性判定提供新途径。
2025-09-09 cs.CC cs.SC
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
Probabilistic and Causal Satisfiability: Constraining the Model
Saarland University（萨尔大学）；University of Lübeck（吕贝克大学）
本文研究概率与因果推理中的可满足性问题，通过固定结构因果模型的图结构并引入小模型约束这两个新维度扩展已有工作，刻画了不同算术、因果层级及紧凑边缘化设置下的复杂度。
2025-04-28 cs.AI cs.CC cs.LO
