发表机构
University of Wrocław（弗罗茨瓦夫大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究带任意多个后继关系的二变量逻辑的可满足性，证明其属于2NEXPTIME，并给出有限模型与无限模型间的双指数阈值，同时证明有限情形下受邻接丢失约束的可满足性为NEXPTIME完全。
AI 中文摘要
我们研究了带有有限个、依赖于输入的不同后继关系以及任意附加一元和二元谓词的二变量一阶逻辑。每个被区分的后继关系必须是公共域上某个线性序的精确直接后继关系；这些序本身在语言中不可用，并且可能具有任意的序类型。我们证明了可满足性属于2NEXPTIME，且与后继数量无关。该证明为可能无限的模型提供了有限证书。一种闭包操作将局部邻域描述（称为星型类型）区分为有界多重性的类型和可以被无限次实现的类型。有界部分被显式表示。在其之外，整数高度向量允许重叠的后继需求被匹配，而不会产生循环或意外的等同。随后对所得路径分量进行稠密排序，从而恢复精确的后继关系。附加二元谓词的一致赋值处理涉及有界部分的见证。相同的证书在2NEXPTIME中判定无限可满足性，并给出一个双指数阈值，超过该阈值，有限模型保证存在无限模型。仅使用两个后继和一元谓词就可以强制产生一个双指数大的有限核心。对于有限模型，我们证明了在受其他序丢失的参考邻接总数约束的情况下，可满足性是NEXPTIME完全的，即使预算以二进制编码且后继数量是输入的一部分。
英文摘要
We study two-variable first-order logic with a finite, input-dependent number of distinguished successor relations and arbitrary additional unary and binary predicates. Each distinguished relation must be the exact immediate-successor relation of some linear order on the common domain; the orders themselves are not available in the language and may have arbitrary order types. We prove that satisfiability belongs to 2NEXPTIME, uniformly in the number of successors. The proof gives finite certificates for possibly infinite models. A closure operation separates local neighbourhood descriptions, called star types, into those of bounded multiplicity and those that can be realized infinitely often. The bounded part is represented explicitly. Outside it, integer height vectors allow overlapping successor requirements to be matched without creating cycles or unintended identifications. Ordering the resulting path components densely then recovers exact successor relations. Consistent assignments of the additional binary predicates handle witnesses involving the bounded part. The same certificates decide infinite satisfiability in 2NEXPTIME and give a doubly exponential threshold above which a finite model guarantees an infinite model. A doubly exponentially large finite core can be forced with only two successors and unary predicates. For finite models, we prove that satisfiability subject to a bound on the total number of reference adjacencies lost by the other orders is NEXPTIME-complete, even when the budget is encoded in binary and the number of successors is part of the input.
