如何用z3py优雅地解决爱因斯坦之谜？

如何解决如何用z3py优雅地解决爱因斯坦之谜？

z3py伙计们提供了一个基于https://github.com/0vercl0k/z3-playground/blob/master/einstein_riddle_z3.py的代码。但是，与该https://artificialcognition.github.io/who-owns-the-zebra相比，该解决方案相当复杂，冗长且难看。我真的不希望切换库，因为z3py似乎更高级和更易于维护。因此，我开始使用我的版本，但是我未能声明某些部分（缺乏知识或无法实现？）。这是我所拥有的以及卡住的地方（2条评论）：

from z3 import *

color = Int('color')
nationality = Int('nationality')
beverage = Int('beverage')
cigar = Int('cigar')
pet = Int('pet')
house = Int('house')

color_variations = Or(color==1,color==2,color==3,color==4,color==5)
nationality_variations = Or(nationality==1,nationality==2,nationality==3,nationality==4,nationality==5)
beverage_variations = Or(beverage==1,beverage==2,beverage==3,beverage==4,beverage==5)
cigar_variations = Or(cigar==1,cigar==2,cigar==3,cigar==4,cigar==5)
pet_variations = Or(pet==1,pet==2,pet==3,pet==4,pet==5)
house_variations = Or(house==1,house==2,house==3,house==4,house==5)

s = Solver()

s.add(color_variations)
s.add(nationality_variations)
s.add(beverage_variations)
s.add(cigar_variations)
s.add(pet_variations)
s.add(house_variations)

# This is not right
#s.add(Distinct([color,nationality,beverage,cigar,pet]))

s.add(And(Implies(nationality==1,color==1),Implies(color==1,nationality==1))) #the Brit (nationality==1) lives in the red (color==1) house
s.add(And(Implies(nationality==2,pet==1),Implies(pet==1,nationality==2))) #the Swede (nationality==2) keeps dogs (pet==1) as pets
s.add(And(Implies(nationality==3,beverage==1),Implies(beverage==1,nationality==3))) #the Dane (nationality==3) drinks tea (beverage=1)
s.add(And(Implies(color==2,beverage==2),Implies(beverage==2,color==2))) #the green (color==2) house's owner drinks coffee (beverage==2)
s.add(And(Implies(cigar==1,pet==2),Implies(pet==2,cigar==1))) #the person who smokes Pall Mall (cigar==1) rears birds ([pet==2])
s.add(And(Implies(color==4,cigar==2),Implies(cigar==2,color==4))) #the owner of the yellow (color==4) house smokes Dunhill (cigar==2)
s.add(And(Implies(house==3,beverage==3),Implies(beverage==3,house==3))) #the man living in the center (hause==3) house drinks milk (beverage==3)
s.add(And(Implies(nationality==4,house==1),Implies(house==1,nationality==4))) #the Norwegian (nationality==4) lives in the first house (house==1)
s.add(And(Implies(cigar==3,beverage==4),Implies(beverage==4,cigar==3))) #the owner who smokes BlueMaster (cigar==3) drinks beer (beverage==4)
s.add(And(Implies(nationality==5,cigar==4),Implies(cigar==4,nationality==5))) #the German (nationality==5) smokes Prince (cigar==4)

# I can't figure our this part,so I can keep it short and efficient
# the green (color==2) house is on the left of the white (color==3) house

当前正在研究ForAll和Function s的方向

解决方法

您应该在此处对各种事物使用枚举。同样，您不能只拥有一个颜色变量：毕竟，每所房子都有不同的颜色，并且您希望对其进行单独跟踪。一个更好的主意是使color，nationality等都是未解释的函数；将数字分别映射到颜色，国家等。

这是针对此问题的Haskell解决方案，它使用SBV库，该库通过我描述的策略通过SMTLib接口使用z3：https://hackage.haskell.org/package/sbv-8.8/docs/src/Documentation.SBV.Examples.Puzzles.Fish.html

将此策略转换为Python，我们有：

from z3 import *

# Sorts of things we have
Color,(Red,Green,White,Yellow,Blue)   = EnumSort('Color',('Red','Green','White','Yellow','Blue'))
Nationality,(Briton,Dane,Swede,Norwegian,German) = EnumSort('Nationality',('Briton','Dane','Swede','Norwegian','German'))
Beverage,(Tea,Coffee,Milk,Beer,Water)  = EnumSort('Beverage',('Tea','Coffee','Milk','Beer','Water'))
Pet,(Dog,Horse,Cat,Bird,Fish)   = EnumSort('Pet',('Dog','Horse','Cat','Bird','Fish'))
Sport,(Football,Baseball,Volleyball,Hockey,Tennis) = EnumSort('Sport',('Football','Baseball','Volleyball','Hockey','Tennis'))

# Uninterpreted functions to match "houses" to these sorts. We represent houses by regular symbolic integers.
c = Function('color',IntSort(),Color)
n = Function('nationality',Nationality)
b = Function('beverage',Beverage)
p = Function('pet',Pet)
s = Function('sport',Sport)

S = Solver()

# Create a new fresh variable. We don't care about its name
v = 0
def newVar():
    global v
    i = Int("v" + str(v))
    v = v + 1
    S.add(1 <= i,i <= 5)
    return i

# Assert a new fact. This is just a synonym for add,but keeps everything uniform
def fact0(f):
    S.add(f)

# Assert a fact about a new fresh variable
def fact1(f):
    i = newVar()
    S.add(f(i))

# Assert a fact about two fresh variables
def fact2(f):
    i = newVar()
    j = newVar()
    S.add(i != j)
    S.add(f(i,j))

# Assert two houses are next to each other
def neighbor(i,j):
    return (Or(i == j+1,j == i+1))

fact1 (lambda i   : And(n(i) == Briton,c(i) == Red))                       # The Briton lives in the red house.
fact1 (lambda i   : And(n(i) == Swede,p(i) == Dog))                       # The Swede keeps dogs as pets.
fact1 (lambda i   : And(n(i) == Dane,b(i) == Tea))                       # The Dane drinks tea.
fact2 (lambda i,j: And(c(i) == Green,c(j) == White,i == j-1))           # The green house is left to the white house.
fact1 (lambda i   : And(c(i) == Green,b(i) == Coffee))                    # The owner of the green house drinks coffee.
fact1 (lambda i   : And(s(i) == Football,p(i) == Bird))                      # The person who plays football rears birds.
fact1 (lambda i   : And(c(i) == Yellow,s(i) == Baseball))                  # The owner of the yellow house plays baseball.
fact0 (                 b(3) == Milk)                                           # The man living in the center house drinks milk.
fact0 (                 n(1) == Norwegian)                                      # The Norwegian lives in the first house.
fact2 (lambda i,j: And(s(i) == Volleyball,p(j) == Cat,neighbor(i,j)))  # The man who plays volleyball lives next to the one who keeps cats.
fact2 (lambda i,j: And(p(i) == Horse,s(j) == Baseball,j)))  # The man who keeps the horse lives next to the one who plays baseball.
fact1 (lambda i   : And(s(i) == Tennis,b(i) == Beer))                      # The owner who plays tennis drinks beer.
fact1 (lambda i   : And(n(i) == German,s(i) == Hockey))                    # The German plays hockey.
fact2 (lambda i,j: And(n(i) == Norwegian,c(j) == Blue,j)))  # The Norwegian lives next to the blue house.
fact2 (lambda i,b(j) == Water,j)))  # The man who plays volleyball has a neighbor who drinks water.

# Determine who owns the fish
fishOwner = Const("fishOwner",Nationality)
fact1 (lambda i: And(n(i) == fishOwner,p(i) == Fish))

r = S.check()
if r == sat:
    m = S.model()
    print(m[fishOwner])
else:
    print("Solver said: %s" % r)

运行此命令时，我得到：

$ python a.py
German

表明鱼的主人是德国人。我认为您的原始问题有不同但相似的约束条件，您可以轻松地使用相同的策略来解决原始问题。

查看以下内容的输出也具有指导意义：

print(m)

在sat中为

。打印：

[v5 = 4,v9 = 1,v16 = 2,v12 = 5,v14 = 1,v2 = 2,v0 = 3,v10 = 2,v18 = 4,v15 = 2,v6 = 3,v7 = 1,v4 = 5,v8 = 2,v17 = 1,v11 = 1,v1 = 5,v13 = 4,fishOwner = German,v3 = 4,nationality = [5 -> Swede,2 -> Dane,1 -> Norwegian,4 -> German,else -> Briton],color = [5 -> White,4 -> Green,1 -> Yellow,2 -> Blue,else -> Red],pet = [3 -> Bird,1 -> Cat,2 -> Horse,4 -> Fish,else -> Dog],beverage = [4 -> Coffee,3 -> Milk,5 -> Beer,1 -> Water,else -> Tea],sport = [1 -> Baseball,2 -> Volleyball,5 -> Tennis,4 -> Hockey,else -> Football]]

忽略对vN变量的所有分配，这些分配是我们内部用于建模目的的分配。但是您可以看到z3如何将每个未解释的函数映射到相应的值。对于所有这些，映射的值是房屋数量到满足拼图约束的相应值。您可以根据需要使用此模型中包含的信息，以编程方式提取该难题的完整解决方案。