CODEWITHSUNDEEP
z3solversmtz3py
user1618465
user1618465

Reputation: 1941

Simple Z3 exercise returning unknown

I'm starting using SMT solvers and I was practicing with this simple problem:

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?

My solution for a) is:

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

But it is returning unknown. Why??

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

Same result! :(

Solution for c): I need to get the solutions first :'(

This is a very simple problem. What am I doing wrong?

NOTE: Exercise gotten from: http://www.loria.fr/~mery/malg/Z3.pdf Thanks

SOLUTION: 

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

Upvotes: 1

Views: 286

Answers (1)

Tim
Tim

Reputation: 1098

Make sure that you use the prices for each item. Notice that the price of fruit $2.15 does not appear in the formulas. Hope that is enough of a hint for you to fix these :-)

As to why the formula first formula returns unknown, notice that both formulas are non-linear mixed integer real queries. The formulas as stated are really easy to satisfy, but SMT solvers for QF_NIRA are not robust. You might want to read up on Hilbert's 10th problem for more historical context.

Upvotes: 2

Related Questions