如何用z3py解决麦乐鸡的问题

Question

我是z3py的新手，想知道这个问题是否可以使用"from z3 import *"。

麦乐鸡块版本的硬币问题是由Henri Picciotto提出的，他将其纳入了与华艳芳合著的代数教科书中。皮乔托上世纪80年代，他和儿子在纽约一家餐馆吃饭时想到了这个申请麦当劳，在餐巾纸上解决问题。麦乐鸡的号码是麦当劳麦乐鸡块的总数量。在英国，原来的盒子(之前的介绍(开心乐园餐大小的金块盒)有6块、9块和20块。(维基百科)

A=6, B= 9, C=20, D=27。你和你的朋友饿了，想吃X块鸡肉。 第一个问题是:<<p>/strong>是否有可能买S盒A码，T盒B码，U盒C码，V盒D码，这样你正好得到X块鸡肉(没有剩余)?(例如x=36)

第二个问题:确定给出可满足解的最小数X，而对于Y=X-1它是不可满足的，因此这个Y是上述固定值a, B, C, D的麦乐鸡块问题的解。这意味着它是不能用这种方式表示的最大数字Y，或者用鸡肉块来表示，无论你买了多少(S,T,U,V)盒给定尺寸(A,B,C,D)，你的朋友确实吃了Y块，那么必须有一些剩余的块。

Answer 1

如果您显示您尝试了什么，以及您遇到了什么类型的问题，则堆栈溢出效果最好。我猜你不太熟悉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, T, U, 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, U = 0, V = 1]
[S = 3, T = 2, U = 0, V = 0]
[S = 0, T = 4, U = 0, V = 0]

给出所有的解。

第二个问题读起来有点混乱，但您可能想使用Optimize对象而不是Solver。从浏览https://rise4fun.com/Z3/tutorial/optimization开始，看看你是否能取得进展。如果没有，请随便问一个新问题;详细说明你遇到的问题。(那里的教程是在SMTLib中，但您可以使用Optimize类在Python中做同样的事情。)