SMT求解器处理简单整数表达式返回Unknown的原因及解决方法咨询

问题根源 #

你的SMT-LIB代码中，第7行的(^ 2 z)是整数变量的指数运算，这属于非线性整数算术约束。当前主流SMT求解器（如Z3）对这类非线性约束的支持能力有限——非线性整数算术是半可判定问题，求解器无法保证在有限时间内得出可满足性结论，因此返回Unknown。

当你取消第6行注释断言x=1时，z被固定为1，指数运算退化为具体数值计算（2^1=2），所有约束变为线性整数算术范畴，求解器可以直接处理，因此返回sat。

解决方法 #

由于z的取值已被约束为0或1，你可以通过枚举z的可能值消除非线性运算，将约束转换为求解器可处理的线性形式，有两种常见方式：

方式1：使用条件表达式（ITE）替换指数运算

将第7行替换为：

(assert (= k (ite (= z 0) 0 1))) ; 等价于k=2^z-1，z∈{0,1}

方式2：展开为析取约束

将第7行替换为：

(assert (or (and (= z 0) (= k 0)) (and (= z 1) (= k 1))))

两种方式都等价于原约束的语义，修改后所有约束均为线性整数算术，求解器会返回sat。

内容的提问来源于stack exchange，提问作者VV. K. ben