Z3中非线性整数算术NIA是不可判定还是半可判定？

1. NIA的可判定性问题 #

首先明确定义：通常说的「不可判定」指不存在算法能对任意输入的该理论公式，在有限时间内返回「可满足/不可满足」的确定结果；「半可判定」指存在算法，当公式可满足时一定能在有限时间内返回肯定结果，公式不可满足时算法可能永不终止。

• NIA（整数非线性算术）的全量词一阶理论确实是不可判定的，这一结论来自哥德尔不完备定理：不存在完备的递归公理系统能覆盖所有一阶皮亚诺算术命题，因此不可能有算法判定任意NIA公式的有效性。
• 但NIA的纯存在量词片段（前缀仅含存在量词的闭公式）是半可判定的：你看到的Leonardo的回复就是针对这一片段，我们可以枚举所有整数组合代入验证，只要公式有解就一定能在有限步内找到，和停机问题的半可判定逻辑一致；但如果公式不可满足，枚举会无限进行，无法得到否定结果。

你的测试用例恰好属于NIA的半可判定片段，且存在非常直观的解（比如y1=0, y2=1即可满足对任意整数x的约束），因此Z3可以快速返回sat结果。

2. LIA是否存在不可判定片段 #

纯LIA（线性整数算术，又称普雷斯伯格算术）是完全可判定的，不存在不可判定的一阶片段。该理论已被证明支持量词消去，任意复杂度的LIA公式都可以在有限时间内得到确定的判定结果，仅求解复杂度随量词嵌套层数升高呈超指数增长。
注意：如果LIA扩展了乘法谓词、未解释函数或其他理论符号，就不再属于纯LIA范畴，可能出现不可判定性。

3. Z3对NRA的支持说明 #

NRA（实数非线性算术）的多项式片段是完全可判定的，这一结论来自塔尔斯基对实闭域理论的证明：所有仅含多项式运算、量词、布尔连接符的NRA公式都可以通过量词消去（如圆柱代数分解算法）得到确定判定结果，Z3对这类问题的求解是完备且可靠的。
如果NRA公式中包含超越函数（如sin、log、指数等），则属于不可判定问题，Z3仅能通过启发式策略尝试求解，无法保证对任意输入都能返回结果。你看到的资料中「Z3仅对非线性多项式可判定」的描述正是对应这一情况。

内容的提问来源于stack exchange，提问作者Theo Deep