z3给出了一个令人惊讶的答案
z3给出了一个令人惊讶的答案
提问于 2021-10-17 17:22:10
我试过这个：
import z3
n,x,y,z = z3.Ints('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)
s.check()
s.model()我得到了：
[x = 1, n = 2, z = 3, y = 1, div0 = [(1, 1) → 1, (4, 2) → 2, else → 0], mod0 = [(1, 3) → 1, else → 0]]但是4/2不等于1/1+1/1+1/3。
我做错了什么？
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-10-17 18:16:42
您已将n, x, y, z声明为整数。所以除法是作为一个整数来完成的，得到1/1 = 1和1/3 = 0；因此满足相等的2=2。
最明显的做法是使用Real值来解决这个问题。将声明更改为：
n,x,y,z = z3.Reals('n x y z')产生：
[z = 1, y = 1, n = 4/3, x = 1]这确实满足了你提出的方程。
如果您确实希望n, x, y, z是整数，那么您应该在除法之前将它们转换为实数，如下所示：
import z3
n,x,y,z = z3.Ints('n x y z')
s = z3.Solver()
s.add(4/z3.ToReal(n)==1/z3.ToReal(x)+1/z3.ToReal(y)+1/z3.ToReal(z))
s.add(x>0)
s.add(n>0)
s.add(y>0)
s.add(z>0)
print(s.check())
print(s.model())这将打印：
sat
[n = 4, x = 3, z = 3, y = 3]再次满足您的约束。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/69606849
复制相关文章
相似问题
腾讯云开发者
