Z3求解含平方根的整数约束问题失败，求问题原因及解决方法

你的代码存在两个关键问题：

• 整数类型与浮点数运算冲突：你将x、y声明为整数类型Int，但使用y ** 0.5进行浮点数平方根运算。Z3对整数与浮点数的混合运算支持有限，且浮点数精度问题会导致求解器无法处理约束。
• 平方根表达错误：Z3中不能通过** 0.5表示平方根，需使用内置的sqrt()函数；如果只需要整数解，直接用x * x == y表达平方关系更高效，完全规避浮点数问题。

修正后的代码 #

方案1：整数约束（推荐，针对整数解场景） #

from z3 import *

x = Int('x')
y = Int('y')

solve(x > 0, y > x, x * x == y)

执行后会输出符合条件的整数解，例如[x = 2, y = 4]

方案2：实数类型配合内置sqrt函数 #

from z3 import *

x = Real('x')
y = Real('y')

s = Solver()
s.add(x > 0)
s.add(y > x)
s.add(sqrt(y) == x)

print(s.check())
print(s.model())

执行后会得到实数解，若需要整数解，可额外添加IsInteger(x)和IsInteger(y)约束

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