小编isa*_*gym的帖子

我正在尝试使用 z3py 作为优化求解器来最大化从一张纸上切下的长方体的体积。python API 提供了 Optimize() 对象，但使用它似乎不可靠，给我的解决方案显然不准确。

我尝试使用h = opt.maximisefollow byopt.upper(h)以及简单地检查模型，以及在将长方体添加到模型之前v = w*b*l和之后定义长方体的体积，以及将目标设置为w*b*l而不是v。他们都没有给我任何类似好的解决方案。

from z3 import *
l = Real("l")
w = Real("w")
b = Real("b")
v = Real("v")
opt = Optimize()
width = 63.6
height = 51

opt.add(b+l <= width)
opt.add(w+b+w+l+w <= height)
opt.add(w > 0)
opt.add(b > 0)
opt.add(l > 0)
opt.add(v == w*b*l)
opt.maximize(w * b * l)
# h = opt.maximize(v)


print(opt.check())
# print(opt.upper(h))
print(opt.model())

输出： …