简单的 Z3 练习返回未知

Question

我开始使用 SMT 求解器，我正在练习这个简单的问题：

Exercise 5. Using Z3 at the restaurant:
(a) Encode the following menu choices into Z3 and determine what a customer could buy using exactly
$15.05
• Mixed fruit $2.15
• French Fries $2.75
• Side Salad $3.35
• Hot Wings $3.55
• Mozzarella Sticks $4:20
• Sampler Plate $5:80
(b) Is it possible to order everything on the menu?
(c) Does this problem have only one solution? If it does
 not, what are the other solutions? 

我对 a) 的解决方案是：

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

Total= Real('total')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")

x = Real('x')
y = Real('y')
s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)


print(s.check())
print(s.model())

但它正在返回unknown。为什么？？

b) 的解决方案：

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

Total= Real('total')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")


s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)
s.add(multiplier1>0)
s.add(multiplier2>0)
s.add(multiplier3>0)
s.add(multiplier4>0)
s.add(multiplier5>0)
s.add(multiplier6>0)


print(s.check())
print(s.model())

同样的结果！ :(

c) 的解决方案：我需要先得到解决方案 :'(

这是一个非常简单的问题。我做错了什么？

注意：练习来自：http://www.loria.fr/~mery/malg/Z3.pdf 谢谢

解决方案：

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")

s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)
s.add(fruit==2.15)
s.add(fries==2.75)
s.add(salad==3.35)
s.add(wings==3.55)
s.add(mozzarella==4.20)
s.add(sampler==5.80)
s.add(multiplier1>=0)
s.add(multiplier2>=0)
s.add(multiplier3>=0)
s.add(multiplier4>=0)
s.add(multiplier5>=0)
s.add(multiplier6>=0)

while s.check() == sat:
  print s.model()
  s.add(Or(multiplier1 != s.model()[multiplier1], multiplier2 != s.model()[multiplier2] ,multiplier3 != s.model()[multiplier3] , multiplier4 != s.model()[multiplier4] ,multiplier5 != s.model()[multiplier5], multiplier6 != s.model()[multiplier6])) # prevent next model from using the same previous one

Answer 1

确保您使用每件商品的价格。请注意，2.15 美元的水果价格没有出现在公式中。希望这足以提示您解决这些问题:-)

至于为什么公式第一个公式返回未知，请注意两个公式都是非线性混合整数实数查询。上述公式很容易满足，但 QF_NIRA 的 SMT 求解器并不稳健。您可能想阅读Hilbert's 10th problem 了解更多历史背景。