一句话：证明 Büchi 算术与线性 p-adic 域存在片段的可满足性问题均为 NP 完全。
本文研究 Büchi 算术的存在片段以及 p-adic 域上线性算术存在片段的可满足性问题的复杂度。主要结果是二者均为 NP 完全。其中，p-adic 域上线性算术存在片段的 NP 上界回答了 Weispfenning（1988）提出的公开问题；该上界的重要之处在于，即使两个理论中满足赋值的比特长度可能超多项式于公式描述长度。关键技术贡献是证明：对于语言编码某线性丢番图方程系统解集的有限状态自动机，其两个状态之间存在路径这一事实可在 NP 内给出见证。
We consider the complexity of the satisfiability problems for the existential fragment of Büchi arithmetic and for the existential fragment of linear arithmetic over p-adic fields. Our main results are that both problems are NP-complete. The NP upper bound for existential linear arithmetic over p-adic fields resolves an open question posed by Weispfenning [J. Symb. Comput., 5(1/2) (1988)] and holds despite the fact that satisfying assignments in both theories may have bit-size super-polynomial in the description of the formula. A key technical contribution is to show that the existence of a path between two states of a finite-state automaton whose language encodes the set of solutions of a given system of linear Diophantine equations can be witnessed in NP.