我必须用z3py得到一个函数的最大值(在它们的一个范围内)。
例如:我有一个函数(foo(x,y) = 2*x + 1 + y
),我想找到[x,y]
(使用约束lo <= foo(x,y) <= hi
)的值,这样foo(x,y)
是最大值。
换句话说,我必须在一定范围内解决一个最大值问题,这可能吗?在
我用python编写了这个简单的脚本:
s = Solver()
# hi is given by the user
# expr is foo(x)
s.add(expr <= hi)
s.add(expr >= lo)
s.add(X >= 0)
s.add(Y >= 0)
if s.check() == sat:
print('_upper_bound: got model %s' % s.model())
如果我只使用一个变量(例如,foo(x) = 2*x + 1
),那么给定的模型是正确的,foo(x)
的值是最高的。如果我使用多个变量(例如,foo(x,y) = 2*x+y
),则得到的结果是最小的。在
范围内的所有点都在函数的域中。在
编辑:显然,如果我去掉关于X和Y的两个约束,我就得到了最大值。在
使用
scipy
,可以minimize
(如果最小化f,则最大化-f)如您所见,您有一个
bounds
参数有关优化例程的更多详细信息to be found here.
相关问题 更多 >
编程相关推荐