返回未知的简单 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
.05
• Mixed fruit .15
• French Fries .75
• Side Salad .35
• Hot Wings .55
• Mozzarella Sticks :20
• Sampler Plate :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 没有出现在公式中。希望这足以提示您解决这些问题:-)

至于为什么第一个公式returns不详，注意这两个公式都是非线性混合整数实数查询。所陈述的公式确实很容易满足，但 QF_NIRA 的 SMT 求解器并不可靠。您可能想阅读 Hilbert's 10th problem 以了解更多历史背景。

返回未知的简单 Z3 练习

Simple Z3 exercise returning unknown

solver

smt

z3

z3py