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 

因此，它似乎一旦你有一個聲明的變量，那麼與之互動常數自動強制該變量的類型。但我完全不會相信這一點：當你在無類型的環境中工作時，最好始終保持清晰。