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 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
Implicant based parallel all solution solver for Boolean satisfiability
本文发展了一种并行计算求解器，用于计算由多元布尔函数定义的布尔方程组的所有满意赋值。虽然有我们已知的CNF形式的布尔公式的可满足性的求解器，但这些主要是为了确定公式的可满足性而设计的，并且没有解决找到所有满意解的问题。而可满足性问题的并行求解器的开发仍然是计算机科学尚未完成的课题。本文提出的求解器旨在用并行算法表示布尔公式的所有解，即使没有CNF形式。将所提出的算法应用于布尔函数的代数范式（ANF）。该算法的基本思想是用布尔函数的一组完整的蕴涵式来表示满足的赋值，这些蕴涵式作为布尔公式的因子。该算法主要在公式的因子稀疏（即具有变量总数的一小部分）的情况下有效。这允许一次一个地计算单个因子的一组完整的蕴涵式，并在每一步减少公式。本文还提出了一个求ANF中函数正交蕴涵的完备集的算法。该算法的一个优点是所有的解都可以用蕴涵式来表示。最后，由于在每一步的小和分布式计算，以及在独立的线程计算，本文提出的求解器预计将是有用的开发一个良好的可扩展性的并行求解器的大规模问题的布尔可满足性在大量的处理器。
2017-02-06 cs.DS cs.LO
Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability
本文描述了多常数乘法（MCM）问题到伪布尔可满足性（PBS）的三种编码，并介绍了一种最优求解MCM问题的算法。据我们所知，所提出的编码和优化算法是第一次正式的MCM问题在PBS的方式。该报告评估了问题大小的复杂性和几个PBS求解器在三种编码上的性能。
2011-05-17 cs.LO math.LO math.OC
Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras
本文研究了Kochen-Specker偏布尔代数中命题可满足性问题的复杂性，证明了不同类别的可满足性问题在计算复杂性上的不同结果。
2026-02-27 cs.LO quant-ph
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
Fast LTL Satisfiability Checking by SAT Solvers
线性时态逻辑（LTL）的可满足性检查是检查LTL断言中可能错误的基本步骤。现存的LTL可满足性检查器使用各种不同的搜索过程。唯一的例外是基于有界模型检验的LTL可满足性检验，它没有提供一个完整的决策过程，LTL可满足性检验器没有利用过去20年在布尔可满足性求解方面取得的显著进展。在本文中，我们提出了一个新的LTL可满足性检查框架，加速使用布尔SAT求解器。我们的方法是基于变体的\emph{obligation-set method}，我们提出了在早期的工作。我们在这里描述了允许使用布尔SAT求解器来分析给定LTL公式的义务的算法。实验评估表明，新的方法提供了一个显着的性能优势。
2014-04-29 cs.DS 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
A Probabilistic Approach to Satisfiability of Propositional Logic Formulae
University of New Hampshire（新罕布什尔大学）
我们提出了一个版本的WalkSAT算法，命名为BetaWalkSAT。该方法使用概率推理来偏置局部搜索算法的起始状态。Beta分布用于对文字的布尔值的置信度建模。我们的研究结果表明，提出的BetaWalkSAT算法可以优于其他的不知情的局部搜索方法复杂的布尔可满足性问题。
2019-12-04 cs.AI 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
The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.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
Generalized Satisfiability Problems via Operator Assignments
Schaefer介绍了布尔域上的广义可满足性问题的框架，并描述了这类问题的计算复杂性。我们研究了Schaefer框架的代数化，其中傅立叶变换被用来以独特的方式表示多线性多项式的约束。约束的多项式表示引起了可满足性概念的放松，其中变量的值是某些希尔伯特空间上的线性算子。对于由二元场上的线性方程组给出的约束的情况，这种松弛在量子力学的基础中受到了相当大的关注，其中诸如Mermin-Peres幻方的构造表明，存在在布尔域中没有解的系统，但通过在某些有限维希尔伯特空间上的算子赋值有解。我们得到了一个完整的性质的布尔关系类，其中有一个在布尔域的可满足性和可满足性通过操作符分配松弛之间的差距。为了建立我们的主要结果，我们适应的概念连续积极的可定义性（PP-可定义性），我们的设置，一个概念，已被广泛用于约束满足问题的研究。在这里，我们表明，PP-可定义性引起的小工具减少，保持可满足性差距。我们还提出了这种方法的几个额外的应用。特别是，也许令人惊讶的是，我们表明，宽松的概念PP-可定义性，其中量化的变量被允许范围超过运营商的分配，没有额外的表达能力，在定义布尔关系。
2017-04-06 cs.LO quant-ph
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
Hardware Acceleration for Boolean Satisfiability Solver by Applying Belief Propagation Algorithm
University of Michigan（密歇根大学）
布尔可满足性（SAT）在计算机科学中有着广泛的应用领域，特别是在电子设计自动化中的应用。电路综合，优化和验证问题可以通过将原始问题转化为SAT问题来解决。然而，可满足性问题是NP完全问题，目前还没有有效的求解方法，因此需要一种有效的可满足性问题求解器来提高其性能。我们提出了一种硬件加速方法的SAT问题。通过对SAT问题和一类特殊的纠错码--低密度奇偶校验码（LDPC）的译码问题的研究，发现它们都是约束满足问题。置信传播算法已成功地应用于LDPC码的译码，并对相应的译码器硬件设计进行了广泛的研究。因此，我们提出了一种基于置信传播的算法来解决SAT问题。利用该算法，可满足性问题求解器可以通过硬件加速。通过软件仿真验证了算法的有效性，并对算法的性能改进进行了评估.我们的实验结果表明，时间复杂度不增加SAT问题的大小，所提出的方法可以实现至少30倍的速度比MiniSat。
2016-03-16 cs.AI cs.LO
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
Balanced incomplete block designs and exact satisfiability
本文通过用布尔公式的子句和布尔变量区组识别区组设计的点，探讨了平衡不完全区组设计（BIBD）与某些线性CNF公式之间的对应关系。BIBD中的并行类对应于相应公式中的XSAT解决方案。这种对应关系允许将结果从一个字段转移到另一个字段。作为一个新的结果，我们从已知的可满足性定理推导出，在部分平衡的不完全区组设计中寻找平行类的问题是NP完全的。
2020-10-05 cs.CC cs.LO math.CO
Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms
United Technologies Research Center（联合技术研究中心）；SRI International（SRI国际）
给定合取范式（CNF）中的布尔公式$ϕ(x)$，对于$e$的所有值，状态密度计算恰好违反$e$子句的变量赋值的数量。因此，状态密度是所有可能分配上未满足子句数量的直方图。该计算概括了最大可满足性（MAX-SAT）和模型计数问题，不仅提供了对整个解空间的洞察，而且还产生了对问题实例的\emph{hardness}的测量。因此，在现实世界的场景中，即使使用最先进的算法，这个问题通常也是不可行的。虽然找到一个确切的答案，这个问题是一个计算密集型的任务，我们提出了一种新的方法来估计密度的状态的基础上的浓度测量不等式。该方法导致二次无约束二进制优化（QUBO），这是特别适合量子退火为基础的解决方案。我们提出了整体的方法和比较结果从D波量子退火对最著名的经典算法，如Hamze-de Freitas-Selby（HFS）算法和可满足性模理论（SMT）求解器。
2019-10-29 cs.AI cs.DM cs.LO
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
Extending rational choice behavior: The decision problem for Boolean set theory with a choice correspondence
给定备选项集合$U$的所有非空子集的族$P$，对$U$的选择是函数$c \colon Ω\to P$，使得对于所有菜单$B \in Ω$为$Ω\subseteq P$和$c(B) \subseteq B$。如果选择$Ω= P$，则选择全部，否则选择部分。在经济学中，当一个代理人的选择行为满足适当的一致性公理时，她就被认为是理性的，一致性公理是在菜单上量化的属性。在这里，我们解决以下提升问题：给定一个部分选择满足一个或多个公理的一致性，是否有可能将其扩展到一个总的选择满足相同的公理？在刻画了经济学文献中一些著名的选择性质的提升之后，我们研究了集合论的一个基本片段的未量化公式的连通可满足性问题的可判定性，其中涉及到选择函数符号、布尔集合算子、单例、等式和包含谓词以及命题连接词.在两种情况下，我们证明了可满足性问题是NP-完全的，而在其余的情况下，我们得到NP-完全的额外的假设下，选择条款的数量是常数。
2022-12-02 cs.LO
Generalized Satisfiability for the Description Logic ALC
基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。我们分类的复杂性标准可满足性问题的所有可能的布尔和量词片段的ALC中存在的一般公理。
2011-03-04 cs.CC cs.LO
parSAT: Parallel Solving of Floating-Point Satisfiability
本文提出parSAT方法，通过将浮点可满足性问题重新形式化并结合全局优化与多核并行执行，构建面向浮点算术的组合式半决策过程，以补充传统SMT求解器在非线性浮点约束求解中的不足。
2025-09-16 cs.LO
Satisfiability of commutative vs. non-commutative CSPs
本研究将布尔CSP的经典与算子可满足性间隙分类推广到任意有限域，证明NP难CSP存在间隙，有界宽度易解CSP无间隙，无界宽度易解CSP可模拟素数阶阿贝尔群线性方程并产生间隙。
2025-09-11 cs.CC cs.LO quant-ph
Symmetry Breaking for Maximum Satisfiability
University of Southampton（南安普顿大学）；Technical University of Lisbon（里斯本理工大学）；INESC-ID（葡萄牙国家系统与计算机工程研究所）
对称性是许多组合问题所固有的，包括布尔可满足性（SAT）和约束规划（CP）。在SAT中，对称破缺谓词（SBP）的识别是一种众所周知的，通常有效的解决难题的技术。SAT中SBPs的识别近年来一直是显著改进的主题，从而产生了更紧凑的SBPs和更有效的算法。SBPs的识别也被应用到伪布尔（PB）约束，表明对称破缺也可以是PB约束的有效技术。本文进一步扩展了SBPs的应用，并表明SBPs可以识别和使用在最大可满足性（MaxSAT），以及在其最知名的变体，包括部分MaxSAT，加权MaxSAT和加权部分MaxSAT。与SAT和PB一样，MaxSAT和变体的对称性破缺谓词对于代表性数量的问题域是有效的，允许解决当前最先进的MaxSAT求解器无法解决的问题实例。
2008-04-03 cs.AI cs.LO
EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability
Vanderbilt University（范德堡大学）；University of Southern California（南加州大学）
针对 SAT/SMT 教学交互工具不足的问题，本文提出 EduSAT，集成 DPLL、ROBDD 及五类 NP 完全问题抽象，经评估全部求解器达到 100% 正确率。
2023-08-15 cs.AI cs.FL cs.LO
TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System
NVIDIA
针对SAT求解并行度受限问题，提出TurboSAT混合求解器，将SAT表述为可微分二值矩阵乘法层，结合GPU并行可微分优化与CPU冲突驱动搜索，在基准测试上较CPU求解器实现超200倍加速。
2025-11-11 cs.AI cs.LG cs.LO
QBF-Based Boolean Function Bi-Decomposition
布尔函数双分解在逻辑综合中是普遍存在的。它需要使用两个输入的简单逻辑门的布尔函数的分解。现有的双分解解决方案通常基于BDD，最近，基于布尔可满足性。此外，分区的输入变量集的假设，或启发式的解决方案被认为是寻找良好的分区。与以前的工作相比，本文提出了使用量化布尔公式（QBF）计算双分解。这些双分解是最佳的输入变量集的不相交性和平衡性。在代表性基准上获得的实验结果表明，计算分解的质量有了明显的改善，而且基于QBF的双分解的实际可行性。
2011-12-14 cs.LO
diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
National University of Ireland, Galway（爱尔兰国立高威大学）
本文介绍了diff-SAT，一个答案集和SAT求解器，它结合了经常使用概率条款，事实和规则的能力，解决和采样的最佳世界观（满足布尔变量分配或答案集的多集）受用户提供的概率约束。采样过程使用称为可微可满足性求解（$\partial\mathrm{SAT}$）或可微答案集编程（$\partial\mathrm{ASP}$）的基于梯度下降的优化方法来最小化用户定义的可微目标函数。用例是i.a.概率逻辑编程（以概率答案集编程的形式），概率布尔可满足性求解（PSAT）和模型多集（答案集或布尔解释）的分布感知采样。
2021-01-03 cs.AI cs.LO
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
(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。
2013-06-25 cs.LO
Complexity assessments for decidable fragments of Set Theory. IV: A quadratic reduction of constraints over nested sets to Boolean formulae
University of Catania（卡塔尼亚大学）；Scuola Superiore di Catania（卡塔尼亚高等研究院）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Trieste（的里雅斯特大学）
作为定量集合论推理的一个贡献，提出了一个翻译的形式$x=y\setminus z$，$x \neq y\setminus z$，和$z =\{x\}$，其中$x,y,z$代表的变量范围在冯诺依曼宇宙的集合，到一个相当简单的合取范式的未量化的布尔公式的文字的合取。目标语言中的公式涉及布尔集合环上的变量，以及表示相等、不相交和包含的差分运算符和关系符。此外，每个翻译的结果是形式为$x=y\setminus z$、$x\neq y\setminus z$的文字的合取，以及其前因是孤立文字且其后因是变量之间的包含（严格或非严格）或变量之间的等式的蕴涵的合取。除了反映了一个简单和自然的语义，这确保可满足性保存，建议的翻译具有二次算法的时间复杂度，和桥梁两种语言都是已知的NP完全可满足性问题。
2022-11-12 cs.AI cs.LO
Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits
Universidad de Concepción（康塞普西翁大学）；University of California, Berkeley（加州大学伯克利分校）；Universidad Técnica Federico Santa María（费德里科圣玛丽亚理工大学）
本研究针对伪布尔优化问题，设计了一种考虑用户指定计算时间限制的随时元求解器，通过广泛的实证证明其性能大幅优于组合中最佳单求解器Gurobi。
2023-09-07 cs.AI cs.LO
SDPs and Robust Satisfiability of Promise CSP
本研究首次探索Promise CSP的鲁棒满足算法，提出基于多数/交替阈值多态性的鲁棒SDP舍入算法，证明缺少该多态性的对称布尔谓词对PCSP困难，并给出相关PCSP的代数刻画猜想。
2025-09-08 cs.DM cs.DS cs.LO
Generalized Modal Satisfiability
众所周知，模态可满足性是PSPACE完备的（Ladner 1977）。然而，如果我们限制所使用的命题运算符的集合，复杂度可能会降低。请注意，存在无限数量的命题运算符，因为命题运算符只是一个布尔函数。我们对命题算子的每一个有限集合的模态可满足性的复杂性进行了完全分类，即，与以前工作相比，我们对无限数量的问题进行了分类。我们表明，根据命题算子的集合，模态可满足性是PSPACE-完全的，CONP-完全的，或在P.我们得到这个分割不仅为模态公式，但也为他们更简洁的表示使用模态电路。我们考虑了单模态和多模态的情况，并研究了有效性的对偶问题。
2008-04-17 cs.CC cs.LO
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
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
2006年，Biere、Jussila和Sinz提出了一个关键的观察，即构造简化有序二元决策图（BDD）的算法背后的逻辑可以被编码为扩展归结逻辑框架中的证明步骤。通过这一点，基于BDD的布尔可满足性（SAT）求解器可以为一组子句生成不可满足性的可检查证明。这样的证明表明，该公式是真正不可满足的，而不需要用户信任的BDD包或SAT求解器建立在it.We扩展他们的工作，使任意存在量化的公式变量，BDD为基础的SAT求解器的关键能力。我们证明了这种方法的实用性，通过应用BDD为基础的求解器，通过修改现有的BDD包，几个具有挑战性的布尔可满足性问题。我们的研究结果表明，缩放奇偶公式，以及厄克特，残缺的棋盘，鸽子洞问题远远超出了其他证明生成SAT求解器。
2023-03-27 cs.LO
Canonical Models and the Complexity of Modal Team Logic
该研究通过引入典范模型将模态团队逻辑MTL的可满足性简化为模型检验，并证明其复杂性为TOWER(poly)完全问题，同时刻画了有界模态深度片段的初等层级复杂性。
2019-04-10 cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
FBK-IRST（布鲁诺·凯斯勒基金会-材料与微系统研究所）
寻找SAT公式的小不可满足核的问题最近受到了广泛的关注，主要是因为它在形式化验证中的应用。然而，命题逻辑往往是不够的表达，表示许多有趣的验证问题，这可以更自然地解决的框架可满足性模理论，SMT。令人惊讶的是，在SMT中找到不可满足的核心的问题在文献中很少受到关注。在本文中，我们提出了一种新的方法来解决这个问题，称为引理提升方法。其主要思想是将SMT求解器与外部命题核心提取器相结合。SMT求解器产生在搜索期间发现的理论引理，动态地将适量的理论信息提升到布尔级别。核心提取器，然后调用原始SMT问题和理论引理的布尔抽象。这将导致一个不可满足的核心，为原来的SMT问题，一旦剩余的理论引理被删除。这种方法在概念上很有趣，在实践中有几个优点。事实上，它的实现和更新非常简单，并且它可以以即插即用的方式与每个命题核心提取器接口，以便免费受益于已经或将要提供的所有未饱和核心还原技术。我们已经评估了我们的算法与一个非常广泛的实证测试SMT-LIB基准，这证实了这种方法的有效性和潜力。
2014-01-16 cs.AI cs.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
On Solving Boolean Multilevel Optimization Problems
INESC-ID Lisboa（里斯本高等工程学院信息与决策系统研究所）；IST（里斯本高等技术学院）；University College Dublin（都柏林大学学院）
许多组合优化问题都涉及到多个层次相关的优化问题。经常使用的解决方案是将适当大的成本与每个单独的优化问题相关联，使得所得到的聚合优化问题的解决方案解决了原始的一组分层依赖优化问题。本文首先研究软件发行版中的软件包可移植性问题。基于最大可满足性（MaxSAT）和伪布尔（PB）优化的简单解决方案被证明是无效的，并且不太可能扩展到大型问题实例。之后，封装可扩展性问题涉及到多级优化。然后，本文开发了新的算法布尔多级优化（BMO），并强调了大量的潜在应用。实验结果表明，所提出的算法BMO允许解决优化问题，现有的MaxSAT和PB求解器，否则无法解决。
2009-03-31 cs.AI cs.LO
LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
Vrije Universiteit Brussel（布鲁塞尔自由大学）
回答集编程（ASP）是一种成熟的知识表示形式。大多数ASP求解器都是基于布尔可满足性求解技术的（扩展）。虽然这些求解器在许多实际应用中非常成功，但它们的强度受到其底层证明系统分辨率的限制。在本文中，我们提出了一个新的工具LP2PB，ASP程序转换为伪布尔理论，求解器的基础上（更强）切割平面证明系统存在。我们评估我们的工具，和潜在的切割平面为基础的解决ASP对传统的ASP基准以及基准从伪布尔求解。我们的结果好坏参半：总的来说，传统的ASP求解器仍然优于我们的翻译方法，但几个基准家庭被确定的平衡转移的其他方式，从而表明，进一步调查到一个更强大的证明系统的ASP是有价值的。
2020-09-22 cs.AI cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Probabilistic and Causal Satisfiability: Constraining the Model
Saarland University（萨尔大学）；University of Lübeck（吕贝克大学）
本文研究概率与因果推理中的可满足性问题，通过固定结构因果模型的图结构并引入小模型约束这两个新维度扩展已有工作，刻画了不同算术、因果层级及紧凑边缘化设置下的复杂度。
2025-04-28 cs.AI cs.CC cs.LO
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Department of Computer Science, Purdue University, IN, USA（计算机科学系，普渡大学）
本文提出KOCO-SMC，一种集成的精确模计数可满足性求解器，通过跟踪上下界和部分变量赋值实现早期估计，显著提升求解效率。
2025-06-17 cs.AI cs.LO
A Study of Parallel Continuous Local Search
School of Computing, Australian National University（澳大利亚国立大学计算机学院）
研究并行连续局部搜索（CLS）在对称伪布尔约束可满足性问题中的应用，发现冗余约束会抑制收敛，CLS在混合求解中能快速完成部分赋值，且局部搜索因鞍点密集目标而快速收敛到稳定解质量分布。
2026-06-08 cs.AI cs.LO
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Hypergraph Neural Networks Accelerate MUS Enumeration
Hitachi, Ltd.（日立制作所）
本文提出基于超图神经网络的领域无关方法，通过强化学习训练代理加速MUS枚举，减少可满足性检查次数。
2026-04-10 cs.AI cs.LG cs.LO
Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints
Rice University（莱斯大学）
针对量子计算中边着色图的受约束完美匹配问题，提出基于Tutte定理与优化技术的新型混合布尔约束编码，实验证明其扩展性显著优于竞争方法，凸显了设计特定问题编码的必要性。
2023-05-18 cs.AI cs.LO math.CO
