z3 和浮点系数的解释

Question

我在玩一个小的多objective整数规划问题：

在 Z3 中（使用 Python 绑定）我们可以非常优雅地说明这一点：

from z3 import *

x1,x2 = Ints('x1 x2')
z1,z2 = Reals('z1 z2')
opt = Optimize()
opt.set(priority='pareto')
opt.add(x1 >= 0, x2 >=0, x1 <= 2, x2 <= 2)
opt.add(x1 <= 2*x2)
# this version is ok: 
#    opt.add(z1 == x1 - 2*x2, z2 == -x1 + 3*x2)
# this truncates coefficients (round down to integer): 
#    opt.add(z1 == 0.5*x1 - 1.0*x2, z2 == -0.5*x1 + 1.5*x2)
# this one seems to work: 
#    opt.add(z1 == 0.5*ToReal(x1) - 1.0*ToReal(x2), z2 == -0.5*ToReal(x1) + 1.5*ToReal(x2))
opt.add(z1 == x1 - 2*x2, z2 == -x1 + 3*x2)
f1 = opt.maximize(z1)
f2 = opt.maximize(z2)
while opt.check() == sat:
    print(opt.model())

这正确解决并给出：

[x1 = 2, x2 = 1, z2 = 1, z1 = 0]
[x1 = 0, x2 = 2, z2 = 6, z1 = -4]
[x1 = 2, x2 = 2, z2 = 4, z1 = -2]
[x1 = 1, x2 = 1, z2 = 2, z1 = -1]
[x1 = 1, x2 = 2, z2 = 5, z1 = -3]

因为我的实际问题有 objectives 的浮点系数，所以我将 objectives 除以 2:

opt.add(z1 == 0.5*x1 - 1.0*x2, z2 == -0.5*x1 + 1.5*x2)

此模型应该为 x 变量给出相同的五个解。然而，当我们运行它时，我们看到一些错误的结果：

[x1 = 0, x2 = 0, z2 = 0, z1 = 0]
[x1 = 0, x2 = 2, z2 = 2, z1 = -2]
[x1 = 0, x2 = 1, z2 = 1, z1 = -1]

当我打印 opt 时，我可以看到哪里出了问题：

(assert (= z1 (to_real (- (* 0 x1) (* 1 x2)))))
(assert (= z2 (to_real (+ (* 0 x1) (* 1 x2)))))

系数被静默处理运行并转换为整数：0.5 到达 0，1.5 变为 1。

解决方法似乎是：

opt.add(z1 == 0.5*ToReal(x1) - 1.0*ToReal(x2), z2 == -0.5*ToReal(x1) + 1.5*ToReal(x2))

这会将浮点系数转换为其有理数：

(assert (= z1 (- (* (/ 1.0 2.0) (to_real x1)) (* 1.0 (to_real x2)))))
(assert (= z2 (+ (* (- (/ 1.0 2.0)) (to_real x1)) (* (/ 3.0 2.0) (to_real x2)))))

现在 0.5 变成 (/ 1.0 2.0) 而 1.5 表示为 (/ 3.0 2.0)。

我的问题是：

这是运行阳离子"as designed"吗？
我的变通办法是解决这个问题的正确方法吗？或者我应该完全避免浮点系数吗？
打印的有理数 (/ 1.0 2.0) 似乎暗示仍然涉及浮点数。这真的是(/ 1 2)吗？（我假设这些实际上是 bigints）。

Answer 1

我认为你基本上回答了你自己的问题。底线是 Python 是一种无类型语言，因此当您将不同类型的操作数与算术运算符混合搭配时，您将受到库的支配，因为它会为您 "match" 这些类型，它在这里做错事也就不足为奇了。在 SMT-Lib2 或任何其他更强类型的绑定中，您会收到类型错误。

切勿在算术中混用类型，并且始终是显式的。或者，更好的是，使用在其类型系统中强制执行此操作的接口，而不是隐式强制常量。所以，简短的回答是，是的；这是设计使然，但不是因为任何深层原因，而是 Python 绑定的行为方式。

这是一个更简单的演示：

>>> from z3 import *
>>> x = Int('x')
>>> y = Real('y')
>>> x*2.5
x*2
>>> y*2.5
y*5/2

因此，看起来一旦您声明了变量，与它们交互的常量就会自动强制转换为该变量的类型。但我根本不会指望这一点：当你在非类型设置中工作时，最好始终明确。

z3 和浮点系数的解释

z3 and interpretation of floating point coefficients

z3

z3py