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
On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic
University of Oxford（牛津大学）；Max Planck Institute for Software Systems, Saarland Informatics Campus（马克斯·普朗克软件系统研究所）
本文研究了Presburger算术在单变量情况下的可判定性，通过完美固定幂和三次多项式两类谓词建立了可判定性结果，并讨论了当限制被取消时的局限性和难度结果。
2026-05-16 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
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
词方程是弦上约束求解理论基础中的一个重要组成部分，近年来受到了广泛的关注。一个词等式将两个词与字符串变量和常量联系起来。它的解决方案相当于一个函数，将变量映射到常量字符串，使等式的左侧和右侧相等。虽然求解词方程的问题是可判定的，但是求解具有长度约束的词方程的问题的可判定性（即，与词等式中的词的长度相关的约束）仍然是一个长期存在的公开问题。在本文中，我们专注于二次字方程的子类，即，其中每个变量最多出现两次。我们首先表明，二次字方程的解决方案的长度抽象一般不Presburger定义。然后，我们描述了一类计数器系统的Presburger转换关系，捕获的长度抽象的二次词方程与定期约束。我们提供了存在性普雷斯伯格整除算术（PAD）理论中计数器系统简单循环效果的编码。由于PAD是可判定的，我们得到了具有长度约束的二次字方程的判定过程，其中相关的计数器系统是\emph{flat}（即，所有节点属于至多一个循环）。我们展示了一个可判定性的结果（事实上，也是一个NP算法与PAD甲骨文）最近提出的NP-完整片段的字方程称为定期面向字方程，连同长度限制。当约束被额外扩展为具有1-弱控制结构的常规约束时，判定性成立。
2018-05-17 cs.LO
Craig Interpolation for Quantifier-Free Presburger Arithmetic
克雷格插值已成为一个通用的算法工具，以提高软件验证。例如，插值可以加速无限状态系统的不动点计算的收敛。它们还有助于改进迭代计算的惰性抽象的细化。有效的插值程序已经提出了只有少数理论。本文给出了一种完全的无量词Presburger算术公式的插值方法。我们提出了一个新的凸变量投影整数不等式和技术，将它们与等式。插值的推导在反驳证明的规模上具有低次多项式的复杂性，并且在实践中通常是快速的。
2008-11-21 cs.LO cs.SC
Complexity of short Presburger arithmetic
研究了Presburger算法中短句的复杂性。这里的“短”是指包含有限数量的变量、量词、不等式和布尔运算的句子;输入仅由不等式中涉及的整数组成。我们证明了，假设Kannan的划分可以在多项式时间内找到，短PA句子的可满足性可以在多项式时间内决定。此外，在同样的假设下，我们证明了短Presburger句子的满意分配的数量也可以在多项式时间内计算。
2017-04-28 cs.CC cs.DM 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
On the Decidability of Presburger Arithmetic Expanded with Powers
本文证明了整数结构上带两个幂集谓词的Presburger算术存在片段可判定，并指出自然数结构上带两个指数函数的存在片段可判定性将蕴含超越数展开方面的重大数学突破。
2025-07-20 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
One-Parametric Presburger Arithmetic has Quantifier Elimination
本文提出了单参数Presburger算术的量词消去算法，解决了相关开放问题，并证明其存在片段的可满足性问题属于NP且最小解具多项式位大小。
2025-06-30 cs.LO cs.SC
Presburger arithmetic, rational generating functions, and quasi-polynomials
Presburger算术是自然数加（但不乘法）的一阶理论。我们刻画了可由Presburger公式定义的集合为其特征函数可由有理生成函数表示的集合，并给出了这类集合的几何刻画.此外，如果p=（p_1，...，p_n）是Presburger公式中自由变元的子集，我们可以定义一个计数函数g（p）为该公式的解的个数，对于给定的p，我们证明了这样得到的每一个计数函数都可以等价地表示为分段拟多项式或有理母函数.最后，我们将已知的计算复杂性结果转化为这种设置，并讨论开放的方向。
2015-01-06 cs.LO math.CO math.LO
Decidability of Extensions of Presburger Arithmetic by Hardy Field Functions
研究Presburger算术通过次多项式Hardy域函数的扩展，证明当函数f增长快于x或次线性但不慢于某多项式时，带最近整数算子的扩展理论Th(ℤ; <, +, ⌊f⌉)不可判定。
2025-08-26 cs.LO math.LO math.NT
On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
University of Oxford（牛津大学）；IMDEA Software Institute（IMDEA软件研究所）；CNRS, Université Paris Cité, IRIF（法国国家科学研究中心，巴黎西岱大学，IRIF）
本文提出了一种通用框架，证明了弱 Presburger 算术和弱线性实数算术的固定否定片段在多项式时间内可判定。
2026-03-09 cs.LO
Unary counting quantifiers do not increase the expressive power of Presburger aritmetic: an alternative shorter proof
本文是2017年弱算术日会议展示的未刊成果，给出一元计数量词不提升Presburger算术表达能力的更短替代证明，2024年ICALP论文进一步解决了该工作未涉及的复杂性问题。
2024-10-09 cs.LO
An efficient quantifier elimination procedure for Presburger arithmetic
本文提出一种可在单指数时间内消去存在量词变量块的Presburger算术量词消去过程，纠正了双重指数时间上界为紧的旧有论断，并据此确定了单元可分解性、良拟序判定及Ramsey量词公式等问题的精确复杂度。
2024-05-02 cs.FL cs.LO math.LO
VC-dimension of short Presburger formulas
研究了Presburger算术中短公式的VC-维数，定义为变量、量词和原子的个数有界。我们给出了下限和上界，这是紧到一个多项式因子的位长度的公式。
2017-10-11 cs.LO math.CO math.LO
NEXP-Completeness of Existential Presburger Arithmetic with Divisibility
University of Antwerp（安特卫普大学）；DePaul University（德保罗大学）
研究带可除性谓词的存在Presburger算术（EPAD）的可满足性问题，证明其为PP-hard，从而否定其属于NP的预期，并定义可多项式时间识别的片段MergeAbs。
2026-09-18 cs.CC cs.LO
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。
2023-11-23 cs.FL cs.LO
Presburger Arithmetic with algebraic scalar multiplications
该研究将Presburger算术扩展为带代数无理数标量乘法的α-PA，证明其判定复杂度远超PA：二次α时需塔式空间且特定量词结构为PSPACE-hard，非二次α时四块量词即不可判定。
2021-07-19 cs.CC cs.LO math.CO
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
本文研究带长度约束的二次词方程的可判定性，通过计数器系统与带可除性的普雷斯堡算术编码，证明了平坦情形下可判定，并扩展至正则定向词方程。
2021-10-28 cs.FL cs.LO
On Presburger arithmetic extended with non-unary counting quantifiers
研究扩展了非一元计数量词的Presburger算术，通过量词消去与归约技术证明其满足性在两重指数空间内可判定，并给出不同量词组合下的计算复杂度上界。
2023-07-11 cs.LO
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
给定一个无量词的Presburger算术公式，如果它有一个令人满意的解，则存在一个其大小（以比特为单位）在公式的大小上多项式有界的解。本文考虑一类特殊的无量词Presburger公式，其中大部分线性约束是差分（分离）约束，而非差分约束是稀疏的.据观察，此类事件通常发生在软件验证中。除了传统的公式大小的措施，我们推导出一个新的解决方案的范围内的参数表征的稀疏性的线性约束和非差约束的数量。特别是，我们表明，每个整数变量所需的位数是线性的非差约束的数量和对数的非零系数的数量和大小，但在其他方面是独立的线性约束的总数在公式中。导出的界限可以用于基于在有限域上实例化整数变量并将输入的无量词Presburger公式转换为等可满足的布尔公式的决策过程中，然后使用布尔可满足性求解器来检查。除了我们的主要理论结果，我们讨论了在实践中获得更严格的界限的几个优化。经验证据表明，我们的决策程序可以大大优于其他决策程序。
2008-10-07 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
Decision Procedure for Entailment of Symbolic Heaps with Arrays
本文给出了用Presburger算法和数组判定分离逻辑中符号堆蕴涵有效性的方法。在后继数组的大小不存在界的条件下，证明了判定过程的正确性。该条件与Brotherston等人在CADE-2017论文中提出的条件无关，即其中一个条件并不意味着另一个条件。为了提高决策过程的效率，还提出了一些技术。决策过程的主要思想是一个新的翻译的蕴涵符号堆到一个公式Presburger算法，并将其与外部SMT求解器。本文还给出了一个实现的实验结果，这表明决策过程的工作效率足够使用。
2017-08-28 cs.LO
Decidability for Entailments of Symbolic Heaps with Arrays
本文证明了分离逻辑中带数组的符号堆蕴含式的两个可判定性结果，分别针对带存在量词的系统（在特定条件下）和同时带数组与列表的系统，核心方法包括转换为Presburger算术和扩展展开-折叠技术。
2021-05-10 cs.LO
On existential Büchi arithmetic in two coprime bases
University of Oxford（牛津大学）
该研究解决了互素基下Presburger算术扩展Büchi谓词的存在片段的可判定性问题，通过量词消去论证证明其可判定。
2026-08-26 cs.FL cs.LO
Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report)
我们提出了一种方法，以参数化的可达性通信有限状态线程，制定了一个可满足性问题的分析。除了无限数量的线程之外，基于SAT/SMT的可达性方法的主要挑战是线程执行的程序中存在无限循环。在本文中，我们展示了如何简单的循环可以加速近似Presburger算术约束。这些约束是通过符号执行获得的，如果给定的程序状态是可达的，则这些约束是可满足的。我们总结循环嵌套在其他循环使用递归关系从内部循环的加速。该摘要抽象了循环迭代参数，因此可能过于近似。我们的符号方法的一个优点是，建立Presburger公式的过程可以在任何算术运算之前立即揭示它们的不可满足性。我们证明了这种技术的力量，证明和反驳的安全特性的无限线程程序和其他无限状态转换系统。
2015-05-11 cs.LO
Discrete Linear Ensemble Logic
Institute of Computer Science, Leipzig University（莱比锡大学计算机研究所）；The University of Texas Health Science Center at Houston（德克萨斯大学健康科学中心休斯顿分校）
针对生物医学知识统一符号层需求，研究自然数上离散集成逻辑$\text{EL}(\text{Nat})$，给出语法语义、嵌入结果、复杂度与表达力结论，并提出相对完备的$\text{HEL}$证明系统。
2026-08-13 cs.LO
Analysis of logics with arithmetic
University of Oxford（牛津大学）；University of Liverpool（利物浦大学）
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.LO
Counting Constraints in Flat Array Fragments
我们确定了一个片段的Presburger算法丰富的自由函数符号和基数约束的解释集，这是适合自动化分析。我们建立这样一个片段的可判定性和复杂性的结果，我们实现我们的算法。在履行来自不变式检查和有界模型检查基准测试的证明义务的实验表明，我们的决策过程的实际可行性。
2016-02-01 cs.LO
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
我们确定差异约束集约束（DBS），一个类比的差异约束算术约束集。DBS不仅可以表示集合约束，而且可以表示集合元素上的算术约束。我们将DBS集成到具有线性组合归纳谓词的分离逻辑中，获得其中可以指定线性数据结构的集合数据约束的逻辑。我们证明了这个逻辑的可满足性是可判定的。决策过程的一个关键步骤是计算DBS可定义的集合关系的传递闭包，为了捕获它，我们提出了一种扩展的量化集合约束与Presburger算术（RQSPA）。RQSPA的可满足性，然后证明是可判定的利用先进的自动机理论技术。
2018-11-02 cs.LO
Presburger Functional Synthesis: Complexity and Tractable Normal Forms
Indian Institute of Technology Bombay（印度理工学院班加罗尔分校）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
本文研究了 Presburger 算术理论下的函数综合问题（PFnS），证明了其 EXPTIME 完备性，并提出了一种保证多项式时间可解的特殊范式 PSyNF 及其编译方法。
2025-08-10 cs.AI cs.LO
Decidability for Sturmian words
该研究证明Presburger算术上Sturmian字的一阶理论可判定，借助通用加法器论证其一致ω-自动性，并用Pecan算法实现复现经典定理、得到特征Sturmian字中反平方与反回文的新结果。
2024-08-02 cs.LO math.CO math.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
Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics
我们建立了一个通用的上限ExpTime的推理与全球的假设（也称为TBoxes）在共代数模态逻辑。与以前的结果不同，这种情况下，我们的界限不需要一个易于处理的一组Tableau规则的实例逻辑，使结果适用于更广泛的类的逻辑。例子是Presburger模态逻辑，它扩展了等级模态逻辑与后继数的线性不等式，以及概率模态逻辑与概率的多项式不等式。我们使用类型消除算法建立理论上界。我们还提供了一个全局缓存算法，潜在地避免了建立整个指数大小的候选状态空间，从而为实际推理提供了基础。该算法仍然涉及频繁的不动点计算，我们展示了如何有效地处理这些问题，在一个具体的算法建模刘和Smolka的线性时间不动点算法。最后，我们证明了上复杂度界是保持下添加名的逻辑，即在共代数混合逻辑。
2021-11-27 cs.LO
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version)
我们研究了在分离逻辑中增加指针运算的复杂性后果。具体来说，我们研究扩展的点到片段的符号堆分离逻辑与各种形式的Presburger算术约束。最重要的是，我们发现，即使在最小的情况下，当我们只允许简单的“差异约束”的合取，（x ′ \leq x+k）其中k是整数，多项式时间可判定性已经是不可能的：可满足性成为NP完全，无量词蕴涵成为CoNP完全蕴涵，量化蕴涵成为P2完全蕴涵（P2是多项式时间层次中的第二类）事实上，我们证明了上界是相同的，P2，即使对于全指针算术，但具有固定的指针偏移量，其中我们允许初等公式的任何布尔组合（x '= x+ k 0），（x' \leq x+ k 0）和（x'<x+ k 0），并且，除了指向公式之外，我们允许长度由k 0限定的数组的空间公式和长度由k 0限定的列表等，其中k 0是固定整数。然而，如果我们允许一种更有表现力的指针算术形式-即任意指针和上的基本公式的任意布尔组合-那么对于可满足性和无量化器蕴涵来说，复杂度的增加相对温和：它们仍然分别是NP-完全和coNP-完全的，并且对于量化蕴涵来说，复杂度似乎急剧增加。
2018-03-08 cs.LO
Optimal Satisfiability Checking for Arithmetic $μ$-Calculi
共代数$μ$演算为不动点逻辑提供了一个通用的语义框架，其分支类型超出了标准的关系设置，例如概率，加权或基于博弈。以前的工作的coalgebraic $μ$ -演算包括指数时间上界的可满足性检查，但需要一个良好的表规则的下一步模态。这样的规则并不是在所有感兴趣的情况下都可用，特别是那些涉及整数权重的情况，如分级$μ$ -演算，或者实值权重与非线性算术的组合。在本文中，我们证明了相同的复杂性上限更一般的假设下，特别是关于（更简单）的可满足性问题的复杂性的基本所谓的一步逻辑，大致描述为嵌套的下一个步骤片段的逻辑。我们还提出了一个通用的全局缓存算法，是适合于实际使用，并支持对飞行可满足性检查。示例应用包括在具有Presburger算术的分级$μ$ -演算的扩展中用于可满足性检查的新指数时间上界，以及（二值）概率$μ$ -演算的扩展与多项式不等式。作为一个副结果，我们还得到了一个新的上限$\mathcal{O}(((nk)!)^2)$的最小模型大小的可满足的公式，所有的共代数$μ$ -演算，其中$n$是大小的公式和$k$的交替深度。
2019-01-15 cs.LO
Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
本文在更一般的假设下证明了余代数μ-演算可满足性检查的指数时间上界，通过通用全局缓存算法实现，并直接支持无保护公式，应用于带多项式不等式的分级μ-演算和概率μ-演算扩展。
2024-07-22 cs.LO
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding
本文研究了在二进制编码位宽和常数的固定位向量理论上判定一阶量化公式可满足性的精确计算复杂性。这个问题是在EXPSPACE中的，并且是NEXPTIME困难的。我们表明，这个问题是完整的复杂性类AEXP（聚）-类的问题可判定的交替图灵机使用指数时间，但只有多项式数量的存在和普遍的状态之间的交替。
2018-05-02 cs.LO
Descriptive Complexity of $\#\textrm{AC}^0$ Functions
我们介绍了一个新的框架，描述复杂性的方法算术计算。我们定义了一个层次结构的类的基础上的想法计数的分配给自由函数变量的一阶公式。我们完全确定了包含结构，并证明了#P和#AC^0作为这个层次结构的类出现。通过这种方式，我们无条件地将#AC^0正确地放置在#P中的算术类的严格层次结构中。我们将我们的类与Saluja等人以模型理论的方式定义的#P中的层次结构进行比较。我们认为，我们的方法更适合于研究算术电路类，例如#AC^0，它可以被描述为我们框架中的一类。
2016-04-22 cs.CC cs.LO
Learning Theory in the Arithmetic Hierarchy
University of Wisconsin - Madison（威斯康星大学麦迪逊分校）
我们考虑了在不同的学习准则下可学习的一致可计算可积族的指数集的算术复杂性。我们确定这些集合的有限学习，学习的限制，行为正确的学习和异常学习的限制的标准概念的确切复杂性。在证明行为正确学习的$Σ_5^0$ -完备性结果中，我们证明了一个独立的结果;如果一个均匀可计算可枚举的家族是不可学习的，那么对于任何可计算的学习者，都有一个$Δ_2^0$枚举见证失败。
2013-02-28 cs.LG cs.LO math.LO
Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4
University of Washington（华盛顿大学）
研究非奇异方阵的Kannan - Bachem史密斯标准型算法，在Lean 4中形式化，通过递归减小枢轴二进制大小实现稳定终止，生成算术叶跟踪，用自定界编解码器定义输入输出大小，给出跟踪成本和矩阵编码长度的多项式界。
2026-07-27 cs.DS cs.LO cs.SC
