Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
证明了对于任何固定的$i>0$，Presburger算术的$Σ_{i+1}$ -片段，即，它对以存在量词开始的$i+1$量词交替的限制对于$\mathsfΣ^{\mathsf{EXP}}_{i}$是完全的，$\mathsfΣ^{\mathsf{EXP}}_{i}$是弱EXP层次的第$i$层，是驻留在$\mathsf{NEXP}$和$\mathsf{EXPSPACE}$之间的多项式时间层次的类似物。这一结果完成了Presburger算法的计算复杂性景观，这一研究可以追溯到Fischer & Rabin在1974年的开创性工作。此外，我们应用的一些技术开发的证明的下限，以建立界限上的自然定义的$Σ_1$ -片段Presburger算法：给定一个$Σ_1$ -公式$Φ(x)$，它表明，一组非负的解决方案是一个最终的周期集，其周期是最多双指数，这个界是紧的。
2014-05-12 cs.LO
On two-variable guarded fragment logic with expressive local Presburger constraints
本文研究二变量守卫片段逻辑扩展局部Presburger量词后的可满足性问题，证明其为EXP完全，并提出一种新的简单确定性图算法给出上界。
2024-08-26 cs.LO
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic
本文提出了一种近似方法来验证计数器系统相对于线性时态逻辑的表达计数扩展中制定的属性。它可以表达，例如，通过对运行中的特定位置进行计数并施加算术约束，确保应答的数量永远不会超过对服务的请求的数量。所解决的问题是不可判定的，因此解决了平坦的下近似的系统。这提供了一个灵活的可调整的穷举和计算工作量之间的权衡，类似于有界模型检验。最近的技术和结果的平坦Kripke结构的模型检查频率特性的解除和构造一个参数化编码的（近似）问题的量化器免费Presburger算法。基于z3 SMT求解器的原型实现证明了基于RERS挑战赛问题的方法的有效性。
2019-01-17 cs.LO cs.SE
One-Parametric Presburger Arithmetic has Quantifier Elimination
本文提出了单参数Presburger算术的量词消去算法，解决了相关开放问题，并证明其存在片段的可满足性问题属于NP且最小解具多项式位大小。
2025-06-30 cs.LO cs.SC
An efficient quantifier elimination procedure for Presburger arithmetic
本文提出一种可在单指数时间内消去存在量词变量块的Presburger算术量词消去过程，纠正了双重指数时间上界为紧的旧有论断，并据此确定了单元可分解性、良拟序判定及Ramsey量词公式等问题的精确复杂度。
2024-05-02 cs.FL cs.LO math.LO
Arithmetic, First-Order Logic, and Counting Quantifiers
本文给出了一个全面的概述，什么是已知的一阶逻辑计数量词和算术谓词。作为一个主要定理，我们证明了Presburger算术在一元计数量词下是封闭的。确切地说，这意味着对于每个一阶公式phi（y，z_1，.，z_k）上存在一阶公式Psi（x，z_1，...，z_k），其在结构<Nat，<，+>上（分别在该结构的初始段上）表示变量x被变量y的可能解释的数量精确地解释，对于该变量y，公式phi（y，z_1，...，z_k）满足。应用这一定理，我们得到一个简单的证明鲁尔的结果，可达性（同样，连接）在有限的图形是不可表达的一阶逻辑与一元计数量词和加法。此外，关于Presburger算法的上述结果有助于表明Crane Beach猜想的一个特定版本的失败。
2002-11-19 cs.LO
Short Presburger arithmetic is hard
研究了Presburger算法（Short-PA）中短句的计算复杂性。这里的“短”是指具有有限数量的变量、量词、不等式和布尔运算的句子;输入仅由线性不等式中涉及的整数系数组成。证明了当第一个量词为$\exists$或$\forall$时，含有$m+2$交替量词的短PA句的可满足性分别是$Σ_{P}^m$ -完全或$Π_{P}^m$ -完全的.对计数版本和受限系统也进行了分析。进一步应用于随机优化中两个自然问题的困难性。
2017-10-20 cs.CC cs.LO math.CO
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
自然数上的加法的一阶理论，被称为Presburger算术，在双指数时间内是可判定的。在语言中添加一个不可解释的一元谓词会导致一个不可判定的理论。我们锐化已知的边界之间的判定和不可判定的，我们表明，纯粹的普遍的片段扩展理论已经是不可判定的。我们的证明是基于减少停机问题的两个计数器的机器的不满足的句子在扩展语言的Presburger算法，不使用存在量化。另一方面，我们认为，一个单一的$\forall\exists$量词交替把扩展语言的可满足的句子集变成一个$Σ^1_1$-完全集。其中的一些结果可以推广到有序实数上的线性算术领域。这涉及到纯通用片段的不可判定性和至少有一个量词交替的句子的$Σ^1_1$-硬度。最后，我们讨论了我们的结果验证的相关性。特别是，我们得出不可判定性的结果量化的片段的分离逻辑，理论的数组，并结合理论的平等的未解释的功能与限制形式的整数算术。在某些情况下，我们的结果甚至意味着缺乏健全和完整的演绎演算。
2017-03-03 cs.LO
VC-dimension of short Presburger formulas
研究了Presburger算术中短公式的VC-维数，定义为变量、量词和原子的个数有界。我们给出了下限和上界，这是紧到一个多项式因子的位长度的公式。
2017-10-11 cs.LO math.CO math.LO
On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
在过去的几十年里，大量的努力投入到确定一阶逻辑的可判定片段。这种努力产生了，除其他外，两个变量的片段和守卫片段，这取决于对语言公式施加的限制类型。尽管上述逻辑在形式化验证和知识表示等领域取得了成功，但这种一阶片段太弱，无法表达影响网络建模或统计推理所需的最简单的统计约束。在这项工作中，我们研究了这些经典的可判定逻辑与百分比量词的扩展，指定如何频繁的一个公式是满足缩进模型。令人惊讶的是，我们发现，所有提到的可判定的片段成为不可判定下这样的扩展，锐化文献中现有的结果。我们的负面结果补充的决定性的两个变量的守卫片段，甚至更有表现力的计数，即Presburger约束。我们的研究结果可以应用于推断各种模态和描述逻辑，如Presburger模态逻辑与逆向或ALCI，表达基数约束的可判定性。
2021-10-03 cs.LO
Integer Linear-Exponential Programming in NP by Quantifier Elimination
本文提出基于量词消去的NP过程判定整数线性指数约束系统可解性，证明对应存在性理论的可满足性为NP完全，改进了EXPSPACE上界，并得到整数线性规划的非确定性多项式时间高斯消去变体。
2024-07-09 cs.LO
Compiling Petri Net Mutual Reachability in Presburger
Petri网是一种经典的并发模型，在形式化验证中被广泛应用和研究，在硬件和软件、数据库和反应式系统的建模和分析中有许多应用。可达性问题是中心，因为许多其他问题减少到可达性问题。已知可达性问题是可判定的，但其复杂性非常高（非原始递归）。在2011年，可达性问题的一个变体，称为相互可达性问题，包括决定两个配置是否相互可达，被证明是指数空间完备的。最近，这个问题发现了几个意想不到的应用，特别是在人口协议理论中。虽然相互可达性问题在Preburger算法中是可定义的，但最近证明了这样一个公式的最著名的上限是非初等的（塔）。在本文中，我们提供了一种方法来编译的相互可达关系的Petri网与$d$计数器到一个无量词Presburger公式给出的双指数析取的$O(d)$线性约束的指数大小。我们还提供了一些初步的结果Presburger公式编码底部配置。
2022-10-18 cs.LO
Decidability bounds for Presburger arithmetic extended by sine
我们考虑Presburger算法的正弦函数扩展，称之为正弦Presburger算法（$\sin$ -PA），并系统地研究了决策问题的$\sin$ -PA的句子集。特别地，在Schanuel猜想的假设下，给出了一个存在$\sin$ -PA语句的判定算法.这个过程减少决策的理论有序添加剂群的实数扩展正弦，这是决定下Schanuel猜想。另一方面，我们证明了四个交替的量词块足以满足$\sin$ -PA句子的不可判定性。要做到这一点，我们明确解释弱一元二阶理论的网格，这是不可判定的，在$\sin$ -PA。
2022-05-02 cs.LO math.LO
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
向量加法系统的可达性问题是网理论的一个中心问题。一般的问题是已知的，是可判定的算法完全基于经典的Komaju-Lambert-Mayr-Sacerdote-Tenney分解。本文使用这种分解来证明VAS识别的语言的Parikh图像是半伪线性的;一类扩展半线性集的类，a.k.a.在Presburger算术中可定义的集合。我们提供了一个应用程序，这个结果，我们证明了最终配置是不可到达的初始一个当且仅当存在一个半线性归纳不变，包含初始配置，但不是最终的。由于我们可以决定是否Presburger公式表示归纳不变量，我们推断存在不可达性的可检查证书。特别是，存在一个简单的算法来决定一般的VAS可达性问题的基础上两个半算法。第一个试图证明的可达性列举有限序列的行动和第二个试图证明的不可达列举Presburger公式。
2010-09-09 cs.LO
Complexity of short Presburger arithmetic
研究了Presburger算法中短句的复杂性。这里的“短”是指包含有限数量的变量、量词、不等式和布尔运算的句子;输入仅由不等式中涉及的整数组成。我们证明了，假设Kannan的划分可以在多项式时间内找到，短PA句子的可满足性可以在多项式时间内决定。此外，在同样的假设下，我们证明了短Presburger句子的满意分配的数量也可以在多项式时间内计算。
2017-04-28 cs.CC cs.DM cs.LO
Succinct Population Protocols for Presburger Arithmetic
Angluin等人证明了种群协议可以精确地计算Presburger算法（PA）中定义的谓词，Presburger算法是加法的一阶理论。作为这一结果的一部分，他们提出了一个程序，将带有余数谓词的无量词PA的任何公式$φ$（其具有与完整PA相同的表达能力）转换为具有计算$φ$的$2^{O(\text{poly}(|φ|))}$状态的群体协议。更准确地说，协议的状态数与公式中最大系数的位长和语法树的节点数都是指数关系。本文证明了带有剩余谓词的无量词PA的每个公式$φ$都可由具有$O(\text{poly}(|φ|))$状态的无领导种群协议计算。我们的证明是基于几个新的建设，这可能是独立的利益。给定一个带有余数谓词的无量词PA的公式$φ$，第一个构造产生一个计算$φ$的简洁协议（带有$O(|φ|^3)$前导）;这完成了在[STACS'18]中开始的工作，在那里我们为PA的一个片段构造了这样的协议。对于足够大的输入，我们可以摆脱这些领导者。如果输入不够大，那么它就很小，我们设计另一个构造，产生一个简洁的协议，其中一个领导者计算$φ$。我们的最后一个建筑摆脱了这个领导者的小投入。
2020-01-13 cs.CC cs.DC cs.LO
Presburger Arithmetic with algebraic scalar multiplications
该研究将Presburger算术扩展为带代数无理数标量乘法的α-PA，证明其判定复杂度远超PA：二次α时需塔式空间且特定量词结构为PSPACE-hard，非二次α时四块量词即不可判定。
2021-07-19 cs.CC cs.LO math.CO
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
本文引入了一个新的一阶逻辑等式可判定片段，它严格地推广了两个已知的一阶逻辑等式可判定片段--Bernays-Schönfinkel-Ramsey（BSR）片段和Monadic片段.定义原则是在原子水平上将普遍量化的变量与存在量化的变量句法分离。因此，我们的分类既不依赖于对量词前缀的限制（如在BSR的情况下），也不依赖于对谓词符号的arity的限制（如在一元的情况下）。我们证明了新的片段表现出有限模型的属性，并推导出一个非小学的计算时间上界所需的决定在新的片段满足。对于量词前缀为$\exists^* \forall^* \exists^*$的前趋句的子片段，可满足性问题被证明是NEXPTIME完备的。最后，我们讨论了如何自动推理程序可以利用我们的结果。
2016-06-20 cs.LO
The complexity of Presburger arithmetic with power or powers
University of Oxford（牛津大学）；University of Warwick（华威大学）；IMDEA Software Institute（IMDEA软件研究所）
研究带指数运算的Presburger算术的复杂性，证明PresPower理论可在三指数时间内判定，PresExp存在片段有NExpTime上界。
2026-05-22 cs.LO
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.LO
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
一元可分解性是变量独立性的概念，它询问一阶理论中的给定公式是否可以表示为理论中一元谓词的布尔组合。最近，Veanes等人在SMT的上下文中展示了一元可分解性的有用性（即输入公式是无量词的），并发现了各种有趣的应用，包括字符串分析。然而，检查一元可分解性通常是不可判定的。某些理论的可判定性是已知的（例如，Presburger算术，Tarski的实闭域），但关于它们的计算复杂性的结果很少。本文研究了整数线性算术在SMT下的一元可分解性。我们表明，这个决策问题是CONP-完全的，当monadically可分解，一个公式承认在最坏的情况下分解的指数大小。我们提供了一个新的应用程序，我们的结果字符串约束求解长度约束。然后，我们扩展我们的结果变元分解，谓词可以承认多个自由变量（相对于一元分解）。最后，我们给出了整数线性算术中的量词消去的一个应用，其中量词块中的变量，如果是独立的，可以用指数（而不是标准的双指数）爆破消除。
2020-04-26 cs.LO
Deciding Hyperproperties
超性质，如观测决定论或对称性，不能表示为单个计算轨迹的性质，因为它们描述了多个计算轨迹之间的关系。HyperLTL是一种时态逻辑，它通过跟踪变量来捕获这种关系，跟踪变量是通过存在和泛跟踪量词引入的，可以用于同时引用多个计算。本文研究了HyperLTL的可满足性问题。我们发现，这个问题是PSPACE-完全的替代自由的公式（因此，没有比LTL可满足性更昂贵），EXPSPACE-完全的存在，为所有的公式，和undecidable为所有存在的公式。许多实际的超性质可以表示为无择一公式。我们的结果表明，这类性质的可满足性和蕴涵都是可判定的。
2016-06-22 cs.LO
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
2006-09-29 cs.CC cs.LO
Expansion-Based QBF Solving Without Recursion
近年来，基于展开的方法在求解量化布尔公式（QBF）方面的理论和实践都显示出了强大的功能，QBF是布尔变量上带有存在量词和泛量词的命题公式的扩展。这种方法部分地扩展了一种类型的变量（存在的或通用的），并将所获得的公式传递给SAT求解器以决定QBF。现有的基于展开的QBF求解器对给定的公式进行分块处理，并递归地进行展开，直到找到一个解为止.本文提出了一种基于展开的QBF求解算法，该算法一次处理整个量词前缀.因此，避免了展开原理的递归应用。实验表明，我们的简单的方法的性能是与QBF解决的艺术状态，特别是在与其他解决技术相结合。
2018-10-05 cs.LO
Decidable Horn Systems with Difference Constraints Arithmetic
研究了Horn子句递归系统解的存在性问题，其中二阶变量被解释为整数关系，并利用无量词差界算法.我们从证明问题的可判定性开始“系统有解吗？“对于一类具有一个二阶变量和一个非线性递归规则的简单Horn系统，证明依赖于一个树自动机的建设，承认在加权图对应的每一个展开树的霍恩系统的所有周期。我们约束树识别只有负权重的周期，通过添加一个Presburger公式，利用每个规则被解雇的次数，并减少我们的问题的普适性Presburger约束树自动机。我们研究了这个问题的复杂性，发现它是在\textsc{NEXPtime}与\textsc{EXPtime} -硬下界。其次，我们放弃了单变量的限制，并考虑多变量二阶Horn系统的结构限制，称为\emph{flatness}。这类更一般的霍恩系统被发现是可判定的，在相同的复杂性范围内。最后，我们使用Horn系统对交替分支向量加法系统（ABVASS）的可达性问题进行了编码，并证明了对于平坦ABVASS，该问题是在co- \textsc{NEXPtime}中的。
2016-02-14 cs.FL cs.LO
Completeness Theorems for k-SUM and Geometric Friends: Deciding Fragments of Integer Linear Arithmetic
在过去的三十年里，$k$ -SUM假说已经成为各种算法问题长期存在的时间障碍的令人满意的解释。然而，直到今天，文献只知道很少的证明结果的反驳这一假设。以描述性的复杂性的观点，我们问：什么是最大的逻辑定义类的问题\emph{captured}的$k$ -SUM问题？为此，我们介绍了一类$\mathsf{FOP}_{\mathbb{Z}}$的问题，相应的决定在Presburger算术/线性整数算术有限整数子集的句子。我们建立了两个大片段的$k$ -SUM问题是细粒度减少下完成：1。$k$ -SUM问题是判定含有$k$存在量词的句子的完全问题。2. $3$ -SUM问题对于$\mathsf{FOP}_{\mathbb{Z}}$的所有$3$ -量词语句都是完备的，最多可以用$3$线性不等式表示.具体地，用于$k$-SUM的快于$n^{\lceil k/2 \rceil \pm o(1)}$算法（或分别用于$3$-SUM的快于$n^{2 \pm o(1)}$算法）直接转换为用于相应片段中的\emph{all}语句的通用算法的多项式加速比。观察一个障碍，证明完整性$3$ -SUM为整个类$\mathsf{FOP}_{\mathbb{Z}}$，我们转向的问题，其他-似乎更一般-问题是完整的$\mathsf{FOP}_{\mathbb{Z}}$。在这个方向上，我们建立了$\mathbb{Z}^d$…
2025-02-07 cs.CC cs.CG cs.LO
Lower Bounds for QBFs of Bounded Treewidth
TU Dresden（德累斯顿工业大学）；TU Wien（维也纳工业大学）；University of Potsdam（波茨坦大学）
量化布尔公式的有效性判定问题是一个理论和实践上都很活跃的研究领域。在参数化算法领域，研究得很好的图测度树宽被证明是一个成功的参数。Chen在参数化复杂性中的一个著名结果是，当输入公式的原始图的树宽与公式的量词深度一起参数化时，QSAT是固定参数易处理的。更准确地说，这种算法的运行时间在公式大小上是多项式的，在树宽上是指数的，其中树宽上的指数函数是一个塔，其高度是量词深度。一个自然的问题是，在假设指数时间假设（ETH）的情况下，是否可以显着改善这些结果并减少塔。在过去的几年里，人们对在ETH下建立下界的兴趣越来越大，大多数情况下都是特定于问题的下界，直到多项式层次的第三层。尽管如此，一个重要的问题是尽可能地解决这个问题，并覆盖整个多项式层次。在这项工作中，我们展示了基于ETH的由树宽（和量词深度）参数化的任意QBF的下限。更正式地说，我们建立了QSAT和树宽的下限，即在ETH下，不可能有一个算法在运行时解决量化器深度i的QSAT明显优于树宽的i倍指数和输入大小的多项式。在这样做时，我们提供了一个通用的减少技术来压缩树宽编码的本质上的任意树分解的动态规划。此外，我们描述了一个更细粒度的分析问题的一般方法，树宽参数化的多项式层次结构的更高级别。
2020-07-02 cs.AI cs.CC cs.DM
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
本文提出了一种新的方法来解决可满足性模理论问题，该方法是在无量词非线性代数算法SMT（QF-NIA）理论的基础上，对整数多项式约束下的基公式的可满足性进行判定.根据以前的工作，我们建议解决SMT（QF-NIA）的情况下，通过减少他们的线性算术：非线性单项式线性化，通过抽象他们与新鲜的变量和执行情况分裂的整数变量与有限域。对于没有有限域的变量，我们可以人为地通过施加一个下限和一个上限来引入一个，并迭代地扩大它，直到找到一个解（或过程超时）。该方法成功的关键是在每次迭代中确定哪些域必须扩展。以前，不可满足的核心被用来识别要改变的域，但没有得到关于新域应该有多大的线索。在这里，我们解释了两种新的方法来指导这个过程，通过分析优化问题的解决方案：（i）最大限度地减少违反人工域边界的数量，通过Max-SMT求解器解决，以及（ii）最小化相对于人工域的距离，通过优化模理论（OMT）求解器解决。使用这种基于SMT的优化技术允许平滑地扩展该方法，也可以通过非线性整数运算来解决Max-SMT问题。最后，我们利用得到的最大SMT（QF-NIA）技术来解决$\exists \forall$公式的量化的非线性算术的一个片段，通常出现在验证和合成应用。
2020-08-31 cs.LO
Polynomial definability in constraint languages with few subpowers
Charles University（查理大学）
本文研究了约束语言中少数子幂的多项式可定义性，证明了短定义与少数子幂的等价性，并讨论了其对复杂度的影响。
2026-01-27 cs.LO math.LO math.RA
Termination of Triangular Polynomial Loops
研究环 $\mathcal{S}$ 上三角弱非线性循环（twn-loops）的终止性问题，通过将其归约到一阶理论的存在性片段证明可判定性与半可判定性，并提出循环转换、线性化技术及多项式时间的复杂度界限。
2024-02-13 cs.LO
Variable Independence in Linear Real Arithmetic
该研究针对线性实数算术（LRA）中变量独立性与可分解性的复杂度开放问题，提出新的公式刻画方法，证明相关复杂度结论，设计出理论最优、速度指数级提升的算法，还可计算分解的最优近似以优化数据库查询。
2023-07-18 cs.DB cs.LO
Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
超图对偶问题DUAL定义如下：给定两个简单超图$\mathcal{G}$和$\mathcal{H}$，判定$\mathcal{H}$是否精确地由$\mathcal{G}$的所有极小断面组成（在这种情况下我们称$\mathcal{G}$是$\mathcal{H}$的对偶）.这个问题等价于决定两个给定的非冗余单调DNF是否是对偶的。已知非DUAL（DUAL的补充问题）在$\mathrm{GC}(\log^2 n,\mathrm{PTIME})$中，其中$\mathrm{GC}(f(n),\mathcal{C})$表示在$O(f(n))$的非确定性猜测之后可以在复杂性类$\mathcal{C}$内判定（检查）的所有问题的复杂性类。证实了$\mathrm{GC}(\log^2 n,\mathrm{LOGSPACE})$中存在非DUAL。在本文中，我们证明了这个猜想，并实际上把非对偶问题的复杂性类$\mathrm{GC}(\log^2 n,\mathrm{TC}^0)$，这是一个子类的$\mathrm{GC}(\log^2 n,\mathrm{LOGSPACE})$。我们这里指的是$\mathrm{TC}^0$的对数时间统一版本，其对应于$\mathrm{FO(COUNT)}$，即，一阶逻辑通过计数量词来扩充。我们分两步实现后一个界限。首先，基于现有的问题分解方法，我们开发了一个新的非DUA…
2017-11-20 cs.CC cs.DS cs.LO
