optimization - z3py 中的 Optimize() 未找到最佳解决方案
问题描述
我正在尝试使用 z3py 作为优化求解器,以最大化从一张纸上剪下的长方体的体积。python API 提供了 Optimize() 对象,但使用它似乎不可靠,给我的解决方案显然不准确。
我尝试使用h = opt.maximise
后跟opt.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())
输出:
unknown
[w = 1, b = 1, l = 47, v = 47]
这绝对不是最大值。将所有值设置为 10 可以提供更好的解决方案来满足约束条件。
解决方案
Z3 的优化器不处理非线性问题。事实上,这正是它打印的原因unknown
。当你看到调用check
returnunknown
时,恰恰意味着:Z3不知道问题是否可以解决,更不用说它是否找到了最优解。
如果添加:
print(opt.reason_unknown())
调用 后check
,您将看到:
(incomplete (theory arithmetic))
在这些情况下,调用model
将返回在处理问题时获得的一些中间结果z3
,但绝不保证它是最优的。
您的问题是非线性的,因为您正在乘以变量。( w
, b
, and l
.) Z3可以解决实数上的非线性可满足性问题,但不能解决优化问题。例如,请参见此处:z3Opt 使用 qfnra-nlsat 优化非线性函数
(请注意,与纯可满足性相比,非线性优化对于实数来说是一个非常困难的问题。因此,这不仅仅是“尚未实现它”的问题。)
推荐阅读
- c# - 如何使用 C# 生成具有特定结构的 XML 文件?
- c# - 如何使用 C# 从结构定义中创建类
- javascript - D3.js - 来自 JSON 的堆积条形图?
- javascript - 如何在通过循环获得的元素的点击事件上绑定一个类?
- iis - 访问 Web 应用程序共享文件夹的最佳方式
- mysql - 在 mysql 中使用 count(*) .. Over(*)
- scala - 我们可以在 Apache Kafka 中将 KStream 转换为 Global KTable 吗?
- angular-material - 如何在导航栏中将按钮向左对齐
- java - 从在 docker 容器中运行的 Java 客户端访问公司代理后面的 Web 服务
- javascript - 函数不会将括号转换为减号