A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
Computing Laboratory（计算实验室）；Oxford University（牛津大学）；School of Computer Science（计算机科学学院）；University of Manchester（曼彻斯特大学）
本文研究了分级模态逻辑在自反性、序列性、对称性、传递性和欧几里得性等不同组合框架类上的可满足性问题，并为其获得了紧致的复杂性界限。
2009-05-19 cs.AI cs.CC cs.LO
On the satisfiability problem for a 3-level quantified syllogistic
我们证明了一个集合的三个排序集理论公式，表示TLQSR，并承认一个限制形式的量化个人和集合变量，有一个可解的可满足性问题，证明它享有一个小的模型属性，即，任何可满足的TLQSR公式psi都有一个有限模型，其大小仅取决于psi本身的大小。我们还引入了TLQSR的子语言（TLQSR）^h，其公式的特征是具有长度以h \geq 2为界的量词前缀和其他一些句法约束，并证明了它们都具有NP-完全的可满足性问题.然后，我们证明了模态逻辑S5可以在（TLQSR）^[3]中形式化。
2013-04-08 cs.LO
Satisfiability Modulo ODEs
Carnegie Mellon University（卡内基梅隆大学）
研究包含常微分方程的实数SMT问题，开发了delta完整算法以处理纯存在性量化和受限时间变量全称量化的公式，通过dReal求解器在大规模非线性ODE和变量基准上展示算法可扩展性。
2013-10-30 cs.LO cs.SY eess.SY
Satisfiability and Synthesis Modulo Oracles
University of Edinburgh（爱丁堡大学）；UC Berkeley（加州大学伯克利分校）；University of Iowa（爱荷华大学）
在经典的程序合成算法中，例如反例引导归纳合成（CEGIS），算法在合成阶段和预言（验证）阶段之间交替。许多合成算法使用基于可满足性模理论（SMT）求解器的白盒预言机来提供反例。但是，如果白盒Oracle不可用或不容易使用，该怎么办？我们提出了一个框架来解决一般类的预言指导的合成问题，我们长期合成模预言。在这种情况下，预言机可以是黑盒子，具有由合成问题定义的查询-响应接口。作为该框架的一个必要组成部分，我们还形式化了可满足性模理论和预言机问题，并提出了一个算法来解决这个问题。我们实现了一个原型求解器的可满足性和合成模神谕，并证明，通过使用神谕执行功能不容易建模SMT约束，如递归函数或神谕，将编译和执行的代码，SMTO和SyMO能够解决超出标准SMT和合成求解器的能力的问题。
2021-07-28 cs.LG cs.LO cs.PL
Sampling Techniques for Boolean Satisfiability
布尔可满足性（{ \SAT }）在跨越测试、形式化验证、规划、优化、推理等的不同领域中发挥了关键作用。除了检查布尔可满足性的经典问题外，随机一致生成满足的问题和计算满足赋值的总数的问题也吸引了大量的理论和实践兴趣。以前的工作提供了启发式的方法，非常弱或没有保证的性能，和理论的方法与证明的保证，但在实践中表现不佳。我们提出了一种基于有限独立散列的新方法，使我们能够为这两个问题设计算法，具有强大的理论保证和扩展到数千个变量的可扩展性。基于这种方法，我们提出了两个实用的算法，{ \UniformWitness }：一个近似均匀的生成器和{ \approxMC }：第一个可扩展的近似模型计数器，以及参考实现。我们的算法通过向{ \SAT }求解器发出多项式调用来工作。我们证明了我们的算法的可扩展性，从不同的应用领域所产生的一个大的基准集。
2014-04-26 cs.LO
Model-Checking Problems as a Basis for Parameterized Intractability
大多数参数化复杂性类都是根据布尔可满足性问题（所谓的加权可满足性问题）的参数化版本来定义的。例如，Downey和Fellow的W-层次结构就是这种形式。但是也有一些类，例如A-层次，它们更自然地以一阶逻辑的某些片段的模型检验问题来表征。唐尼、费罗斯和里根是第一个在两种形式主义之间建立联系的人，他们用一阶模型检验问题来描述W-层次。我们改进了他们的结果，然后证明了A-层次和W^*-层次的加权可满足性和模型检验问题之间类似的对应关系。因此，我们获得了非常统一的许多最重要的参数化复杂性类的特征，在这两种形式主义。我们的结果可以用来给一些结构参数化复杂性理论的核心结果的新的，简单的证明。
2005-06-22 cs.CC cs.LO
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
在过去的二十年中，模态和描述逻辑已被应用于计算机科学的许多领域，包括知识表示，形式化验证，数据库理论，分布式计算，以及最近的语义Web和本体。基于这个原因，模态逻辑和描述逻辑中的自动推理问题得到了深入的研究。特别地，已经提出了许多方法来有效地处理核心正规模态逻辑K（m）及其记法变体描述逻辑ALC的可满足性。虽然K（m）/ALC结构简单，但在计算上很难推理，它的可满足性是PSPACE完全的。在本文中，我们开始探索的想法，执行自动推理任务的模态和描述逻辑编码成SAT，以便处理的国家的最先进的SAT工具，与大多数以前的方法，我们开始我们的调查从满足性K（m）。我们提出了一个有效的编码，我们测试了一组广泛的基准，比较的方法与主要的国家的最先进的工具。虽然编码必然是最坏情况下的指数，从我们的实验中，我们注意到，在实践中，这种方法可以处理大多数或所有的问题，这是在其他方法的范围内，与性能相当，甚至更好，那些目前的国家的最先进的工具。
2014-01-15 cs.AI cs.LO
ExpTime Tableaux for Type PDL
PDL型系统（$τ$ PDL）是命题动态逻辑（PDL）的扩展，其主要目标是为推理动作类型（由其前提和效果建模）和主体能力提供形式化的基础。该系统有两个等价的解释，即标准关系语义和类型语义，其中过程术语被解释为类型，即二元关系集。它的可满足性问题是可判定的，因为基于过滤参数提供了NExpTime判定过程，并且建议$τ$ PDL的可满足性问题应该在确定性的单指数时间内可解。在本文中，我们解决的问题的复杂性问题的可满足性问题的$τ$ PDL。我们提出了一个确定性的基于表的可满足性算法，并证明它是健全的和完整的，它运行在ExpTime。此外，该算法通过尽可能限制或分支，尽可能早地检测可满足性。
2019-09-01 cs.LO
On the Satisfiability of Local First-Order Logics with Data
本文研究带数据一阶逻辑的可满足性问题，提出局部片段限制量化范围，证明半径-1片段可判定而更大半径不可判定，并给出存在片段完整的可判定性与复杂性图景。
2024-07-01 cs.LO
Reasoning about Strategies: on the Satisfiability Problem
策略逻辑（Strategy Logic，简称SL）是由Mogavero、Murano和Vardi提出的一种有用的形式主义，用于在多智能体并发游戏中明确地推理策略（作为一阶对象）。这种逻辑被证明是非常强大的，包含了所有主要的先前研究的模态逻辑的战略推理，包括ATL，ATL* 等。不幸的是，由于其高表达性，SL具有非基本可判定的模型检查问题，并且可满足性问题是不可判定的，特别是Sigma_1^1。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，每次有一个单一的时间目标，对于每个策略量化的代理。我们证明了SL[1G]与SL不同，SL[1G]具有有界树模型性质，并且它的可满足性问题在2ExpTime中是可判定的，因此并不比ATL* 的可满足性问题难.
2017-03-16 cs.LO
Satisfiability Games for Branching-Time Logics
分支时间时态逻辑如CTL*、CTL和CTL+的可满足性问题在程序规范和验证中有重要的应用。它们的计算复杂性是已知的：CTL* 和CTL+对于双指数时间是完全的，CTL对于单指数时间是完全的.这些逻辑的一些决策程序是已知的;它们使用树自动机，tableaux或公理系统。在本文中，我们提出了一个统一的博弈论框架，这些分支时间时序逻辑的可满足性问题。我们定义可满足性游戏的完整的分支时间时序逻辑CTL* 使用高层次的定义获胜的条件，抓住了最少不动点展开的本质的良好基础。这些获胜条件构成了ω-词的形式语言。我们分析了在何种情况下需要哪种确定性ω-自动机来识别这些语言。然后，我们得到一个减少的问题，解决奇偶校验或Büchi游戏。所获得的算法的最坏情况下的复杂性匹配这些逻辑的已知下界。这种方法提供了一个统一的，但复杂性理论上的最佳处理分支时间时序逻辑的可满足性。它将时序逻辑机器的使用与自动机的使用分开，从而保留了输入公式和表示可满足性的对象之间的语法关系，即奇偶或Büchi游戏中的获胜策略。这里介绍的游戏只在输入公式的Fischer-Ladner闭包上工作。最后但并非最不重要的是，这里提出的游戏来尝试提供工具支持复杂的分支时间逻辑，如CTL* 和CTL+的可满足性问题。
2013-10-15 cs.LO
Delta-Complete Decision Procedures for Satisfiability over the Reals
我们引入了“δ-完备决策过程”的概念来解决实数上的SMT问题，目的是处理包括超越函数和Lipschitz连续常微分方程的解在内的广泛的非线性函数.给定一个SMT问题φ和一个正有理数δ，一个δ-完全决策过程要么确定φ是不可满足的，要么确定φ的“δ-弱化”是可满足的。这里，φ的δ-弱化是φ的一个变体，它允许φ上的δ-有界数值扰动。我们证明了具有上述函数的实数上有界SMT的δ-完全判定过程的存在性。对于类型2复杂性类C的函数，在温和的假设下，有界δ-SMT问题是NP^C。δ-完备决策过程可以利用可扩展的数值方法来处理非线性，我们建议使用这个概念作为数值驱动决策过程的理想要求。作为一个具体的例子，我们对<ICP>DPLL（T）中集成了区间约束传播（ICP）的DPLL框架进行了形式化分析，建立了其δ-完备性的充分必要条件。我们讨论了δ-完备决策过程在正确性关键应用中的实际应用，包括形式化验证和定理证明。
2012-09-17 cs.LO cs.SC
Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras
本文研究了Kochen-Specker偏布尔代数中命题可满足性问题的复杂性，证明了不同类别的可满足性问题在计算复杂性上的不同结果。
2026-02-27 cs.LO quant-ph
Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving
Florida International University（佛罗里达国际大学）；SRI International（SRI国际（斯坦福国际研究院））；United States Military Academy（美国军事学院（西点军校））；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Central Florida（中佛罗里达大学）；Vanderbilt University（范德堡大学）
本文提出 LLM 与 SMT 求解器迭代交互的神经符号框架，通过反例反馈修正规划综合结果，并在积木规划任务中验证其可生成可证明正确的解。
2023-09-28 cs.AI 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
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
在SAT和SMT中计算Craig插值的问题最近受到了很大的关注，主要是因为它在形式化验证中的应用。插值生成的有效算法已经提出了一些理论的利益-包括平等和未解释的功能，线性算术的有理数，以及它们的组合-他们成功地使用在模型检验工具。然而，对于整数上的线性算术理论（LA（Z）），找到插值的问题更具挑战性，并且为完整理论LA（Z）开发有效的插值生成器的任务仍然是正在进行的研究的目标。在本文中，我们试图缩小这一差距。我们建立在以前的工作，并提出了一种新的插值算法的SMT（LA（Z）），它利用了当前最先进的SMT（LA（Z））求解器的全部功能。我们证明了我们的方法的潜力与我们的实施所提出的算法在MathSAT SMT求解器的广泛的实验评估。
2012-08-09 cs.LO
Neuro-Symbolic Constrained Optimization for Cloud Application Deployment via Graph Neural Networks and Satisfiability Modulo Theory
本文提出基于图神经网络和可满足性模理论的神经符号框架，用于优化云应用部署，通过结合约束推理与机器学习提升求解器的可扩展性和成本最优性。
2025-11-28 cs.LO
Computational Complexity of Standpoint LTL
本文分析立场线性时态逻辑SLTL的计算复杂度，证明其可满足性问题为EXPSPACE完全，还提出约束方法得到PSPACE完全的SLTL片段，实现立场逻辑与LTL的低复杂度结合。
2024-08-16 cs.LO
One-dimensional guarded fragments
我们称一个一阶公式是一维的，如果它的每个存在（全称）量词的最大块最多留下一个变量。我们认为一维的限制的守护片段，GF，和三守护片段，TGF，后者是一个最近的扩展GF中的量化子公式，最多有两个自由变量不需要守护，因此可以被看作是一个统一的GF和两个变量的片段，FO 2。我们分别表示由此产生的形式主义，GF 1和TGF 1。我们表明，GF 1具有指数模型的属性和NExpTime完全可满足性问题（即，它比完整的GF更容易）。对于TGF 1，我们证明了它是可判定的，具有有限模型属性，并且它的可满足性问题是TwoExpTime-完全的（在没有等式的情况下是NExpTime-完全的）。所有上述结果都是针对没有常数的签名获得的。最后，我们讨论了它们的影响，观察到常数不破坏可判定性，但增加了可满足性问题的复杂性。
2019-06-28 cs.LO
Schur Number Five
我们提出了一个世纪的老问题的解决方案称为舒尔数五：什么是最大的（自然）数$n$，使存在一个五着色的正数高达$n$没有单色解决方案的方程$a + b = c$？我们得到的解决方案，$n = 160$，通过编码的问题到命题逻辑和应用大规模并行可满足性求解技术的结果公式。我们构建并验证了解决方案的证明，以增加对多CPU年计算正确性的信任。证明大小为2 PB，并使用正式验证的证明检查器进行了认证，表明可满足性求解器的任何结果-无论多大-现在都可以使用高度可信的系统进行验证。
2017-11-21 cs.DC cs.DM cs.LO
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality
均匀一维片段UF 1 ^=是从一阶逻辑中获得的一种形式，通过将量化限制在存在（全称）量词块的应用中，使得在量化公式中最多有一个变量保持自由。片段在布尔运算下是闭合的，但附加的限制（称为一致性条件）适用于具有两个或多个变量的原子公式的组合。这个片段可以被看作是二元逻辑的规范化推广，定义它是为了能够处理任意的关系。最近引入了分片的概念，并证明了UF 1 ^=的无等式分片的可满足性问题是可判定的.本文证明了UF 1 ^=的可满足性和有限可满足性问题是NEXPTIME-完全的。我们还证明了具有计数量词的扩展UF ^=的相应问题是不可判定的。除了可判定性问题，我们还比较了UF ^=和二元逻辑与计数量词FOC^2的表达性。我们表明，虽然逻辑一般来说是不可比较的，但当注意力仅限于元数界为二的词汇时，UF 1 ^=严格包含在FOC^2中。
2014-09-02 cs.LO math.LO
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
本文提出概率交替时间μ演算PAMC用于随机多智能体系统策略能力推理，证明其复杂度性质并给出模型检测与可满足性检测算法，实现为开源工具且验证了有效性。
2024-12-12 cs.FL cs.GT cs.LO
(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。
2013-06-25 cs.LO
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
UCLID 5是一个多模态形式化建模、验证和系统综合的工具。它使人们能够解决异构系统的验证问题，如硬件和软件的组合，或那些有多个，不同的规格，或系统，需要混合模式的建模。\uclid的一个新方面是强调使用语法引导和归纳综合来自动化建模和验证步骤。本文介绍了\uclid工具的新发展，包括新的语言功能，集成与新技术的语法指导合成和可满足性解决，支持hyperproperties和组合的公理和操作建模，演示新的问题类，和一个强大的实现。
2022-08-07 cs.LO
Complexity and expressivity of propositional dynamic logics with finitely many variables
研究了命题动态逻辑有限变量片段可满足性的复杂性。我们认为三种形式主义属于三个代表性的复杂性类，广泛理解，-经常PDL，这是EXPTIME-完整的，PDL的交集，这是2 EXPTIME-完整的，PDL与并行组合，这是不可判定的。我们表明，对于这些逻辑中的每一个，即使我们只允许仅由命题常量（即没有命题变量）构建的公式作为输入，可满足性的复杂性也保持不变。此外，我们表明，这是一个后果的丰富的表达能力的变量免费片段：对于所有的逻辑，我们认为，这样的片段是整个逻辑的语义表达。我们推测，这是PDL风格的代表，以及密切相关的逻辑。
2019-01-18 cs.LO math.LO
Formal Languages via Theories over Strings
我们调查的形式语言的性质表示的公式在量词的自由理论的字方程，算术长度的限制，语言成员谓词的类定期，明显下推，和确定性上下文无关的语言。总的来说，我们考虑了20个不同的理论和可判定性问题，例如形式语言的空性和普遍性。首先，我们讨论了它们的相对表达能力，并观察到一个粗略的划分为两个层次的基础上是否存在字方程。其次，我们考虑了几个重要的决策问题，如空性和普遍性的可判定性状态。注意空性问题等价于相应理论上的可满足性问题。第三，我们考虑的问题，是否在一个理论的语言是在另一个表达，并显示几个负面的结果，这个问题是不可判定的。这些结果是特别相关的背景下，范式在实践和理论方面的字符串解决。
2022-05-01 cs.FL cs.LO
A Decidable Fragment of Strategy Logic
策略逻辑（Strategy Logic，简称SL）是Mogavero、Murano和Vardi最近提出的一种有用的形式主义，用于在多智能体并发博弈中明确地推理作为一阶对象的策略。这种逻辑变得非常强大，包含了所有以前研究过的用于战略推理的模态逻辑，包括ATL，ATL* 等。不幸的是，由于它的表达能力，SL有一个非基本可判定的模型检查问题和一个高度不可判定的可满足性问题，特别是$Σ_{1}^{1}$ -Hard。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这个逻辑是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，对于代理的每个策略量化，每次都有一个单一的时间目标。SL[1G]是一个基本可判定的模型检验问题。在这里，我们证明，与SL不同，它具有有界树模型属性，并且它的可满足性问题在2 ExpTime中是可判定的，因此不比ATL* 难。
2012-06-12 cs.LO math.LO
Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)
本研究提出C2的单子立场扩展的多项式时间翻译方法，证明其可满足性仍为NExpTime完全，可在不提升复杂度的情况下为OWL相关描述逻辑增加多视角推理能力，并明确了复杂度下界与不可判定边界。
2025-08-01 cs.LO
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
Case Western Reserve University（凯斯西储大学）；Microsoft Corporation（微软公司）；Microsoft Research（微软研究院）
本文针对LLM生成形式化规范时的概率性与验证确定性之间的冲突，提出PCFG框架建模输出不确定性，并通过信号融合实现选择性验证，大幅降低错误率，推动可靠自动化推理。
2025-05-26 cs.AI cs.CL cs.LO
Tighter Bounds on the Expressivity of Transformer Encoders
University of Notre Dame（圣母大学）
本研究通过识别一种带计数量词的一阶逻辑变体，同时作为固定精度 Transformer 编码器的上界和 Transformer 编码器的下界，从而更精确地刻画了 Transformer 编码器可识别的语言类别。
2023-11-13 cs.FL cs.LG cs.LO
Word equations in linear space
词方程的可满足性是形式语言和代数交叉中的一个重要问题：给定两个由字母和变量组成的序列，我们要决定是否存在变量的替换，使这个方程变成真正的字符串相等。这个问题的确切计算复杂性仍然是未知的，最好的下限和上限分别是NP和PSPACE。最近，一种新的再压缩技术被应用到这个问题上，简化了已知的证明，并将空间复杂度降低到（不确定性）O（nlog n）。本文证明了词方程的可满足性是在非确定线性空间中的，因此可满足的词方程的语言是上下文敏感的，并通过著名的Immerman-Szelepcsenyi定理证明了不可满足的词方程的语言也是上下文敏感的.我们使用已知的基于再压缩的算法，并另外采用霍夫曼编码的信件。然而，证明使用了对方程的片段如何相互依赖的分析，以及算法的非确定性选择的新策略，该策略使用了几个新的想法来限制字母所占用的空间。
2020-10-16 cs.FL cs.LO
Model checking and model synthesisfrom partial models: a logic-based perspective
我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。
2020-12-22 cs.LO
