How to solve a McNuggets problem using z3py

user_15071113 0
Viewed 77

I am new to z3py and wondering if this problem can be easily solved using "from z3 import *".

The McNuggets version of the coin problem was introduced by Henri Picciotto, who included it in his algebra textbook co-authored with Anita Wah. Picciotto thought of the application in the 1980s while dining with his son at McDonald's, working the problem out on a napkin. A McNugget number is the total number of McDonald's Chicken McNuggets in any number of boxes. In the United Kingdom, the original boxes (prior to the introduction of the Happy Meal-sized nugget boxes) were of 6, 9, and 20 nuggets. [Wikipedia]

Task

McDonald is selling McNuggets in these boxes A=6, B= 9, C=20, D=27. Your friends and you are hungry and want to eat X chicken pieces.

first question: is possible to buy S boxes of size A, T boxes of size B, U boxes of size C and V boxes of size D such that you get exactly X chicken pieces (without left over)? (for example x=36)

second question: determine the minimal number X which gives a satisfiable solution, while for Y=X-1 it is not satisfiable and thus this Y is the solution of the Chicken McNuggets problem for the fixed A, B, C, D values above. This means that it is the largest number Y which can NOT be represented this way, or in terms of chicken pieces, no matter how many (S,T,U,V) boxes of the given sizes (A,B,C,D) you buy and your friends do eat exactly Y pieces, then there has to be some left over pieces.

z3py
1 Answers

Stack-overflow works the best if you show what you tried, and what sort of problems you ran into. I'm guessing you're not quite familiar with the idioms with z3py: Start by reading through https://ericpony.github.io/z3py-tutorial/guide-examples.htm which will get you on the right track.

Having said that, the first question is trivial to code in z3py:

from z3 import *

A = 6
B = 9
C = 20
D = 27

S, T, U, V = Ints('S T U V')

X = 36

s = Solver()
s.add(S >= 0)
s.add(T >= 0)
s.add(U >= 0)
s.add(V >= 0)
s.add(S*A + T*B + U*C + V*D == X)

while s.check() == sat:
    m = s.model()
    print(m)

    block = []
    for var in [S, T, U, V]:
        v = m.eval(var, model_completion=True)
        block.append(var != v)

    s.add(Or(block))

This prints:

[S = 6, T = 0, U = 0, V = 0]
[S = 0, T = 1, U = 0, V = 1]
[S = 3, T = 2, U = 0, V = 0]
[S = 0, T = 4, U = 0, V = 0]

giving you all the solutions.

The second question is a bit confusing to read, but you might want to use the Optimize object instead of Solver. Start by reading through https://rise4fun.com/Z3/tutorial/optimization and see if you can make progress. If not, feel free to ask a new question; detailing what problem you ran into. (The tutorial there is in SMTLib, but you can do the same in Python using the Optimize class.)

user_9363100
Related