Z3和浮点系数

Question

我是用一个小的多目标整数规划问题，玩的解释：

在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] 

正如我真正的问题浮点系数为工作目标，我除以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)表示。

我的问题是：

1. 这是截断 “作为设计的”？
2. 我的解决方法是解决此问题的正确方法吗？或者我应该完全避免浮点系数？
3. 打印的理性数字(/ 1.0 2.0)似乎暗示仍然存在浮点数。这真的是(/ 1 2)？ （我认为这些实际上是bigint）。

Answer 1

我觉得你基本上回答了你自己的问题。最重要的是，Python是一种无类型的语言，所以当你将不同类型的操作数与算术运算符混合搭配时，你会受到库的支配，因为它会为你“匹配”这些类型，并不奇怪它在这里做错了事。在SMT-Lib2或其他任何更强类型的绑定中，你会得到一个类型错误。

从不混合算术中的类型，并且一律是明确的。或者，更好的是，使用一个在其类型系统中执行此操作的接口，而不是隐式强制常量。所以，简单的回答是，是的。这是通过设计，但不是因为任何深层原因，而是因为Python绑定的行为。

这里有一个简单的演示：

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

因此，它似乎一旦你有一个声明的变量，那么与之互动常数自动强制该变量的类型。但我完全不会相信这一点：当你在无类型的环境中工作时，最好始终保持清晰。