利用google or-tools 求解逻辑难题：斑马问题

今天我们利用google or-tools的cp_model建模语言来求解一个著名的逻辑问题：斑马问题。

斑马问题

1. 一条街上有五座不同颜色的房子，每座房子住着不同国籍的人，每个人抽不同的烟，喝不同的饮料，养不同的宠物。
2. 英国人住在红房子里。
3. 西班牙人养狗。
4. 住在绿房子里的人喝咖啡。
5. 乌克兰人喝茶。
6. 绿房子就在乳白色房子的右边。
7. 抽流金岁月（烟名）的人养蜗牛。
8. 抽薄荷烟的住在黄房子里。
9. 住在中间的房子里的人喝牛奶。
10. 挪威人住在第一座房子里。
11. 抽契斯特菲尔德（烟名）的人住在养狐狸的人旁边。
12. 抽薄荷烟的人住在养马的人旁边。
13. 抽好彩（烟名）的人喝橙汁。
14. 日本人抽百乐门（烟名）。
15. 挪威人住在蓝房子隔壁。

最后请问：谁喝水？谁养斑马？

解答

求解此类问题时,我们首先对问题中出现的名词进行分类,然后寻找各类名词之间的对应关系：

房屋颜色：红色、绿色、黄色、蓝色、乳白色。
国籍：英国人、西班牙人、日本人、乌克兰人、挪威人。
动物：狗、蜗牛、狐狸、斑马、马。
饮料：茶、咖啡、水、牛奶、橙汁
烟名：抽流金岁月、抽薄荷烟、契斯特菲尔德、好彩、百乐门。

创建变量

我们发现我们可以将问题中的所有名称分成5个分类，并且5个分类下有5个对应的名词。接下来我们为每一个名词创建一个整形变量：

from ortools.sat.python import cp_model
model = cp_model.CpModel()
#房屋颜色
red = model.NewIntVar(1, 5, 'red')
green = model.NewIntVar(1, 5, 'green')
yellow = model.NewIntVar(1, 5, 'yellow')
blue = model.NewIntVar(1, 5, 'blue')
ivory = model.NewIntVar(1, 5, 'ivory')
#国籍
englishman = model.NewIntVar(1, 5, 'englishman')
spaniard = model.NewIntVar(1, 5, 'spaniard')
japanese = model.NewIntVar(1, 5, 'japanese')
ukrainian = model.NewIntVar(1, 5, 'ukrainian')
norwegian = model.NewIntVar(1, 5, 'norwegian')
#动物
dog = model.NewIntVar(1, 5, 'dog')
snails = model.NewIntVar(1, 5, 'snails')
fox = model.NewIntVar(1, 5, 'fox')
zebra = model.NewIntVar(1, 5, 'zebra')
horse = model.NewIntVar(1, 5, 'horse')
#饮料
tea = model.NewIntVar(1, 5, 'tea')
coffee = model.NewIntVar(1, 5, 'coffee')
water = model.NewIntVar(1, 5, 'water')
milk = model.NewIntVar(1, 5, 'milk')
fruit_juice = model.NewIntVar(1, 5, 'fruit juice')
#烟名
old_gold = model.NewIntVar(1, 5, 'old gold')
kools = model.NewIntVar(1, 5, 'kools')
chesterfields = model.NewIntVar(1, 5, 'chesterfields')
lucky_strike = model.NewIntVar(1, 5, 'lucky strike')
parliaments = model.NewIntVar(1, 5, 'parliaments')

添加约束

因为每个分类下的名词都是唯一的，所以这里我们要对各个分类下的所有成员分别添加一个AddAllDifferent()约束：

model.AddAllDifferent([red, green, yellow, blue, ivory])
model.AddAllDifferent([englishman, spaniard, japanese, ukrainian, norwegian])
model.AddAllDifferent([dog, snails, fox, zebra, horse])
model.AddAllDifferent([tea, coffee, water, milk, fruit_juice])
model.AddAllDifferent([parliaments, kools, chesterfields, lucky_strike, old_gold])

接下来我们根据题目中所有已知条件来添加各类名词之间的对应关系约束：

#英国人住红房子
model.Add(englishman == red)
#西班牙人养狗
model.Add(spaniard == dog)
#绿房子里的人喝咖啡
model.Add(coffee == green)
#乌克兰人喝茶
model.Add(ukrainian == tea)
#绿房子就在乳白色房子的右边
model.Add(green == ivory + 1)
#抽流金岁月（烟名）的人养蜗牛
model.Add(old_gold == snails)
#抽薄荷烟的住在黄房子里
model.Add(kools == yellow)
#住在中间的房子里的人喝牛奶
model.Add(milk == 3)
#挪威人住在第一座房子里
model.Add(norwegian == 1)

以上我们对能够明确对应关系的名词对建立了关联关系，剩下我们还有3个关系不明确的条件：

1. 抽契斯特菲尔德（烟名）的人住在养狐狸的人旁边。
2. 抽薄荷烟的人住在养马的人旁边。
3. 挪威人住在蓝房子隔壁。

对于像旁边、隔壁这类地点状语，我们也可以推断出两个相关变量之间差的绝对值应该是1：

抽契斯特菲尔德（烟名）的人住在养狐狸的人旁边：
| chesterfields - fox | = 1  

抽薄荷烟的人住在养马的人旁边：
| horse - kools | = 1

挪威人住在蓝房子隔壁：
| norwegian - blue | = 1

为此我们还需要为这三个条件添加3个绝对值约束：

#抽契斯特菲尔德（烟名）的人住在养狐狸的人旁边：
diff_fox_chesterfields = model.NewIntVar(-4, 4, 'diff_fox_chesterfields')
model.Add(diff_fox_chesterfields == fox - chesterfields)
model.AddAbsEquality(1, diff_fox_chesterfields)

#抽薄荷烟的人住在养马的人旁边：
diff_horse_kools = model.NewIntVar(-4, 4, 'diff_horse_kools')
model.Add(diff_horse_kools == horse - kools)
model.AddAbsEquality(1, diff_horse_kools)

#挪威人住在蓝房子隔壁：
diff_norwegian_blue = model.NewIntVar(-4, 4, 'diff_norwegian_blue')
model.Add(diff_norwegian_blue == norwegian - blue)
model.AddAbsEquality(1, diff_norwegian_blue)

求解

solver = cp_model.CpSolver()
status = solver.Solve(model)

if status == cp_model.OPTIMAL:
    people = [englishman, spaniard, japanese, ukrainian, norwegian]

    #找出喝水的人
    water_drinker = [p for p in people if solver.Value(p) == solver.Value(water)][0]
    #找出养斑马的人
    zebra_owner = [p for p in people if solver.Value(p) == solver.Value(zebra)][0]
    
    print('The', water_drinker.Name(), 'drinks water.')
    print('The', zebra_owner.Name(), 'owns the zebra.')
else:
    print('No solutions to the zebra problem, this is unusual!')

参考资料

以上代码来自于: https://github.com/google/or-tools/blob/master/examples/python/zebra_sat.py