Z3求解4/n=1/x+1/y+1/z约束返回意外结果，问题出在哪？

你代码的核心问题是使用Z3的Int整数类型进行运算时，Z3默认对整数除法执行截断向零取整的规则，和你预期的实数除法规则完全不同。

代入你拿到的模型按整数除法规则验证：

• 左边：4 / 2 整数除法结果为 2
• 右边：1/1 + 1/1 + 1/3 整数除法拆分后为 1 + 1 + 0 = 2
  两边相等，因此Z3判定这个解是合法的，和你用实数运算验证的结果存在差异。

你可以根据需求选择以下两种方案之一：

• 方案一：将变量声明为实数类型Real，让除法按实数规则执行，修改后代码如下：

import z3
n,x,y,z = z3.Reals('n x y z')
s = z3.Solver()
s.add(4/n == 1/x + 1/y + 1/z)
s.add(x > 0)
s.add(n > 0)
s.add(y > 0)
s.add(z > 0)
print(s.check())
print(s.model())

运行后会得到符合实数运算规则的解，例如[n = 4, x = 3, y = 3, z = 3]这类符合数学常识的结果。

• 方案二：如果你的问题约束要求x、y、z、n必须为正整数，可以将除法等式转换为等价的整数乘法表达式，避免整数除法的截断歧义：
  将原代码中的等式约束s.add(4/n==1/x+1/y+1/z)替换为：

s.add(4 * x * y * z == n * y * z + n * x * z + n * x * y)

该式为原式两边同乘n*x*y*z得到的等价表达式，所有运算均为整数乘法，得到的解会完全符合你预期的埃及分数拆分规则。

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