z3 和浮点系数的解释 [英] z3 and interpretation of floating point coefficients

问题描述

我在玩一个小的多目标整数规划问题:

在 Z3(使用 Python 绑定)中，我们可以非常优雅地说明这一点:

from z3 import *x1,x2 = Ints('x1 x2')z1,z2 = Reals('z1 z2')选择 = 优化()opt.set(priority='pareto')opt.add(x1 >= 0, x2 >=0, x1 <= 2, x2 <= 2)opt.add(x1 <= 2*x2)# 这个版本没问题:# opt.add(z1 == x1 - 2*x2, z2 == -x1 + 3*x2)# 这会截断系数(向下舍入为整数):# opt.add(z1 == 0.5*x1 - 1.0*x2, z2 == -0.5*x1 + 1.5*x2)# 这个似乎有效:# 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)而 opt.check() == sat:打印(选项.模型())

这正确解决并给出:

[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)))))(断言 (= 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)))))(断言 (= 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).

解决方案

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

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

这是一个更简单的演示:

<预><代码>>>>从 z3 导入 *>>>x = Int('x')>>>y = Real('y')>>>x*2.5×*2>>>y*2.5y*5/2

因此，似乎一旦您声明了变量，与它们交互的常量就会自动强制转换为该变量的类型.但我根本不会指望这一点:当您在无类型设置中工作时，最好始终保持明确.

I was playing with a small multi-objective integer programming problem:

In Z3 (using the Python bindings) we can state this very elegantly:

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())

This solves correctly and gives:

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

As my real problem has floating point coefficients for the objectives, I divided the objectives by 2:

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

This model should give the same five solutions for the x variables. However, when we run it, we see some wrong results:

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

When I print opt I can see where things go wrong:

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

The coefficients are silently truncated and converted to integers: 0.5 arrived as 0 and 1.5 became 1.

A workaround seems to be:

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

This converts the floating point coefficient to their rational equivalents:

(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)))))

Now 0.5 becomes (/ 1.0 2.0) and 1.5 is represented by (/ 3.0 2.0).

My questions are:

1. Is this truncation "as designed"?
2. Is my workaround the correct way to go about this? Or should I avoid floating point coefficients altogether?
3. The printed rational number (/ 1.0 2.0) seems to hint there are still floating point numbers involved. Is this really (/ 1 2)? (I assume these are actually bigints).

解决方案

I think you essentially answered your own question. Bottom line is that Python is an untyped language, so when you mix-and-match different typed operands to arithmetic operators, you are at the mercy of the library as it will "match" these types for you, and it is not surprising that it does the wrong thing here. In SMT-Lib2, or any other more strongly-typed binding, you'd instead get a type error.

Never mix types in arithmetic, and always be explicit. Or, better yet, use an interface that enforces this in its type system, instead of implicitly coercing constants. So, short answer is, yes; this is by design, but not because of any deep reason, but rather how the Python bindings behave.

Here's a simpler demo:

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

So, it appears that once you have a declared variable, then the constants that interact with them automatically coerce to the type of that variable. But I wouldn't count on that at all: It's best to be always explicit when you are working in an untyped setting.

这篇关于z3 和浮点系数的解释的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！