z3 und Interpretation von Punkt-Koeffizienten Floating

Question

I wurde mit einem kleinen Multi Ziel Integer Programming Problem spielen:

In Z3 (die Python-Bindings verwenden) können wir diesen Zustand sehr elegant:

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

Dies löst richtig und gibt:

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

Als mein eigentliches Problem ist für die Ziele Punkt Koeffizienten schwebend, aufgeteilt ich die Ziele von 2:

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

Dieses Modell sollte die gleichen fünf Lösungen für die x-Variablen geben. Aber wenn wir es laufen, sehen wir einige falsche Ergebnisse:

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

Wenn ich opt drucke ich kann sehen, wo die Dinge schief gehen:

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

Die Koeffizienten geräuschlos abgeschnitten werden und umgewandelt ganze Zahlen: 0,5 kam als 0 und 1,5 wurde 1.

Eine Abhilfe zu sein scheint:

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

Dieser wandelt die Gleitkomma-Koeffizienten zu ihrer rationalen Äquivalente:

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

Nun wird 0.5 und 1.5 durch (/ 1.0 2.0)(/ 3.0 2.0) dargestellt ist.

Meine Fragen sind:

1. Ist das Abschneiden "wie er entworfen"?
2. Ist meine Workaround der richtige Weg, um darüber zu gehen? Oder sollte ich Gleitkomma-Koeffizienten insgesamt vermeiden?
3. Die gedruckte rationale Zahl (/ 1.0 2.0) scheint darauf hinzuweisen, dass es immer noch Gleitkommazahlen gibt. Ist das wirklich (/ 1 2)? (Ich nehme an, das sind eigentlich Bigints).

Answer 1

Ich denke, dass Sie im Wesentlichen Ihre eigene Frage beantwortet haben. Unterm Strich ist Python eine untypisierte Sprache. Wenn Sie also verschiedene typisierte Operanden mit arithmetischen Operatoren mischen, sind Sie der Bibliothek ausgeliefert, da sie diese Typen für Sie "abgleicht", und das ist nicht überraschend Es macht das Falsche hier. In SMT-Lib2 oder einer anderen stärker typisierten Bindung erhalten Sie stattdessen einen Typfehler.

Niemals Typen in Arithmetik mischen und immer explizit sein. Oder, noch besser, verwenden Sie eine Schnittstelle, die dies in ihrem Typsystem erzwingt, anstatt Konstanten implizit zu erzwingen. Also, kurze Antwort ist, ja; Das ist Absicht, aber nicht aus irgendeinem Grund, sondern wie sich die Python-Bindungen verhalten.

Hier ist eine einfache Demo:

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

So scheint es, dass, sobald Sie eine deklarierte Variable haben, dann ist die Konstanten, die mit ihnen automatisch auf die Art dieser Variablen coerce interagieren. Aber darauf würde ich nicht zählen: Es ist am besten, immer explizit zu sein, wenn Sie in einer nicht typisierten Einstellung arbeiten.