如何使用 z3py 解决 McNuggets 问题

如何解决如何使用 z3py 解决 McNuggets 问题

我是 z3py 的新手，想知道这个问题是否可以使用“from z3 import *”轻松解决。

硬币问题的 McNuggets 版本是由 Henri Picciotto 引入的， 谁将它包含在他与 Anita Wah 合着的代数教科书中。皮乔托 想到 1980 年代与儿子在餐厅用餐时的应用程序 麦当劳，在餐巾纸上解决这个问题。一个 McNugget 数是 任意数量的盒子中的麦当劳 McNuggets 的总数。 在英国，原盒（在引入之前 Happy Meal 大小的金块盒）分别为 6、9 和 20 个金块。 [Wikipedia]

任务

麦当劳在 A=6、B=9、C=20、D=27 的盒子中出售 McNuggets。你和你的朋友饿了想吃 X 块鸡块。

第一个问题：是否可以购买 A 号的 S 盒、B 号的 T 盒、C 号的 U 盒和 D 号的 V 盒，这样你就可以得到 X 块鸡块（没有剩下的）？ （例如 x=36）

第二个问题： 确定给出可满足解的最小数 X，而对于 Y=X-1，它是不可满足的，因此该 Y 是针对固定解的 Chicken McNuggets 问题的解A、B、C、D 值以上。这意味着它是不能以这种方式表示的最大数 Y，或者不能以鸡块表示，无论给定尺寸（A、B、C、D）有多少（S、T、U、V）盒) 你买了，你的朋友确实吃了 Y 块，那么肯定还有一些剩余的块。

解决方法

如果您展示您尝试过的内容以及遇到的问题类型，则堆栈溢出效果最佳。我猜您不太熟悉 z3py 的习语：首先通读 https://ericpony.github.io/z3py-tutorial/guide-examples.htm，这将使您走上正轨。

话虽如此，第一个问题在 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,V]:
        v = m.eval(var,model_completion=True)
        block.append(var != v)

    s.add(Or(block))

打印：

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

为您提供所有解决方案。

第二个问题读起来有点混乱，但您可能希望使用 Optimize 对象而不是 Solver。首先通读https://rise4fun.com/Z3/tutorial/optimization，看看您是否可以取得进展。如果没有，请随时提出一个新问题；详细说明你遇到了什么问题。 （该教程在 SMTLib 中，但您可以使用 Optimize 类在 Python 中执行相同的操作。）