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的发展方向
您应该在这里使用不同种类的枚举。此外，你不能只拥有一个颜色变量：毕竟，每栋房子都有不同的颜色，你想单独跟踪它。一个更好的想法是使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', IntSort(), Nationality)
b = Function('beverage', IntSort(), Beverage)
p = Function('pet', IntSort(), Pet)
s = Function('sport', IntSort(), 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, neighbor(i, 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, neighbor(i, j))) # The Norwegian lives next to the blue house.
fact2 (lambda i, j: And(s(i) == Volleyball, b(j) == Water, neighbor(i, 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)
在CCD_ 5的情况下。此打印：
[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是如何将每个未解释的函数映射到相应的值的。对于所有这些，映射的值是房子的数量到满足谜题约束的相应值。您可以根据需要使用此模型中包含的信息以编程方式提取谜题的完整解决方案。