1.Knowledge - 让电脑理解逻辑 ¶
关于逻辑，命题、真值表、范式、蕴含、等价、归结等等概念在离散数学中都有所提及。本次尝试通过代码让电脑完成简单的推理。
在 logic.py 中利用 python 的类实现了一些逻辑运算以及知识库（Knowledge Base）的功能。下面给出一些运用的例子。
Knights and Knaves¶
问题描述 ¶
有几个人，其中有骑士（Knight）与小偷（Knave）。骑士总是说真话，小偷总是说谎话。现在有他们说的一些话，请你判断他们分别是什么身份。
Puzzle 0¶
A says “I am both a knight and a knave.”
因为 A 说“我既是骑士又是小偷”，这是不可能的。因此 A 说的是假话，即 A 是小偷。
Puzzle 1¶
A says “We are both knaves.” B says nothing.
A 说“我们都是小偷”，这是不可能的（假设法）。因此 A 说的是假话，即 A 是小偷。B 什么都没说，因此 B 是骑士。
Puzzle 2¶
A says “We are the same kind.” B says “We are of different kinds.”
A 说“我们是同一种人”，这是错的（假设法）。因此 A 说的是假话，即 A 是小偷。B 说“我们是不同种类的人”，这是正确的，因此 B 是骑士。
Puzzle 3¶
A says either “I am a knight.” or “I am a knave.”, but you don’t know which. B says “A said ‘I am a knave.’” B then says “C is a knave.” C says “A is a knight.”
A 说“我是骑士”或“我是小偷”，但你不知道哪个是真的。事实上 A 无论如何也不会说自己是小偷。B 说“A 说‘我是小偷’”，所以这是假话，因此 B 是小偷。B 说“C 是小偷”，这是假的，因此 C 是骑士。C 说“A 是骑士”，这是正确的，因此 A 是骑士。
那么电脑该如何理解并推理出上述的结果呢？下面尝试使用代码来实现。
from logic import *
# Symbols
Aknight = Symbol("A is a Knight")
Aknave = Symbol("A is a Knave")
Bknight = Symbol("B is a Knight")
Bknave = Symbol("B is a Knave")
Cknight = Symbol("C is a Knight")
Cknave = Symbol("C is a Knave")
# Knowledge 0
knowledge0 = And(
# A is either a knight or a knave, but not both
Or(Aknight, Aknave),
Not(And(Aknight, Aknave))
)
# Puzzle 0
# A says “I am both a knight and a knave.”
knowledge0.add(
Biconditional(Aknight, And(Aknight, Aknave))
)
print("Puzzle 0")
for symbol in [Aknight, Aknave]:
if model_check(knowledge0, symbol):
print(symbol)
print()
# Knowledge 1
knowledge1 = And(
# A is either a knight or a knave, but not both
Or(Aknight, Aknave),
Not(And(Aknight, Aknave)),
# B is either a knight or a knave, but not both
Or(Bknight, Bknave),
Not(And(Bknight, Bknave))
)
# Puzzle 1
# A says “We are both knaves.”
# B says nothing
knowledge1.add(
Biconditional(Aknight, And(Aknave, Bknave))
)
print("Puzzle 1")
for symbol in [Aknight, Aknave, Bknight, Bknave]:
if model_check(knowledge1, symbol):
print(symbol)
print()
# Knowledge 2
knowledge2 = And(
# A is either a knight or a knave, but not both
Or(Aknight, Aknave),
Not(And(Aknight, Aknave)),
# B is either a knight or a knave, but not both
Or(Bknight, Bknave),
Not(And(Bknight, Bknave))
)
# Puzzle 2
# A says “We are the same kind.”
# B says “We are of different kinds.”
knowledge2.add(
Biconditional(Aknight, Or(And(Aknight, Bknight), And(Aknave, Bknave)))
)
knowledge2.add(
Biconditional(Bknight, Or(And(Aknight, Bknave), And(Aknave, Bknight)))
)
print("Puzzle 2")
for symbol in [Aknight, Aknave, Bknight, Bknave]:
if model_check(knowledge2, symbol):
print(symbol)
print()
# Knowledge 3
knowledge3 = And(
# A is either a knight or a knave, but not both
Or(Aknight, Aknave),
Not(And(Aknight, Aknave)),
# B is either a knight or a knave, but not both
Or(Bknight, Bknave),
Not(And(Bknight, Bknave)),
# C is either a knight or a knave, but not both
Or(Cknight, Cknave),
Not(And(Cknight, Cknave))
)
# Puzzle 3
# A says either “I am a knight.” or “I am a knave.”, but you don’t know which.
# B says “A said ‘I am a knave.’”
# B then says “C is a knave.”
# C says “A is a knight.”
knowledge3.add(
Biconditional(Aknight, Or(Aknight, Aknave))
)
knowledge3.add(
Biconditional(Bknight, Biconditional(Aknight, Aknave))
)
knowledge3.add(
Biconditional(Bknight, Cknave)
)
knowledge3.add(
Biconditional(Cknight, Aknight)
)
print("Puzzle 3")
for symbol in [Aknight, Aknave, Bknight, Bknave, Cknight, Cknave]:
if model_check(knowledge3, symbol):
print(symbol)
print()
上面的代码在运行后即可得出结果如下：
Puzzle 0
A is a Knave
Puzzle 1
A is a Knave
B is a Knight
Puzzle 2
A is a Knave
B is a Knight
Puzzle 3
A is a Knight
B is a Knave
C is a Knight
Minesweeper¶
" 扫雷游戏是一款经典的益智游戏，游戏的目标是在不触雷的情况下，揭开所有的方块。每个方块上都有一个数字，代表周围 8 个方块中有多少个雷。如果一个方块上没有数字，那么它周围的 8 个方块都不是雷。如果一个方块上的数字为 0，那么它周围的 8 个方块都不是雷。如果一个方块上的数字为 1，那么它周围的 8 个方块中有 1 个雷。如果一个方块上的数字为 2，那么它周围的 8 个方块中有 2 个雷。以此类推。"
要让电脑通过逻辑推理完成扫雷游戏，需要完成以下几个步骤：
- 读取扫雷游戏的初始状态
- 根据初始状态，推理出每个方块周围的雷的数量
- 根据推理出的结果，判断哪些方块是雷，哪些方块不是雷
- 根据判断出的结果，标记出雷的位置
其中关键在于，在得到某个块周围的雷的数量后，如何判断哪些方块是雷，哪些方块不是雷。这里可以使用以下的逻辑：
- 如果某个方块周围的雷的数量为 0，那么它周围的方块都不是雷
- 如果某个方块周围的雷的数量与未知方块的数量相同，那么这些未知的方块都是雷
而扫雷的逻辑推理如果使用真值表来建立知识库的话，那么知识库的规模将会非常大，因此这里使用逻辑语句来建立知识库，这样可以大大减少知识库的规模。
我定义一个列表 knowledge 表示知识库，其中每个元素都是一个 Sentence 对象，表示一个逻辑语句。其中 Sentence 对象的 cells 属性表示该逻辑语句中的所有方块，count 属性表示该逻辑语句中的雷的数量。例如一个 Sentence 对象 Sentence({(1, 1), (1, 2), (2, 1)}, 1) 表示，这三个方块中有一个雷。
此外，处理以上的两种推理方法，我们还可以通过“做差”的方式推理得到更多信息。例如有两个 Sentence 对象 Sentence({(1, 1), (1, 2), (2, 1)}, 1) 和 Sentence({(1, 1), (1, 2), (2, 1), (2, 2)}, 2)，那么这两个 Sentence 对象的差集 Sentence({(2, 2)}, 1) 表示，这个方块中有一个雷。这种方法可以推理出更多的信息，因此在推理的过程中，我们需要不断地使用这种方法来推理出更多的信息。于是我们根据上述内容写出以下关键部分代码：
def add_knowledge(self, cell, count):
# 1) mark the cell as a move that has been made
self.moves_made.add(cell)
# 2) mark the cell as safe
self.mark_safe(cell)
# 3) add a new sentence to the AI's knowledge base
# based on the value of `cell` and `count`
# (i.e. the sentence should represent the fact that
# `count` of `cell`'s neighbors are mines)
neighbors = set()
for i in range(cell[0] - 1, cell[0] + 2):
for j in range(cell[1] - 1, cell[1] + 2):
if (i, j) == cell:
continue
if 0 <= i < self.height and 0 <= j < self.width:
if (i, j) in self.mines:
count -= 1
elif (i, j) not in self.safes:
neighbors.add((i, j))
self.knowledge.append(Sentence(neighbors, count))
while True:
pre_knowlodges = self.knowledge.copy()
# 4) mark any additional cells as safe or as mines
# if it can be concluded based on the AI's knowledge base
for sentence in self.knowledge:
mines = set(sentence.known_mines())
safes = set(sentence.known_safes())
for cell in mines:
self.mark_mine(cell)
for cell in safes:
self.mark_safe(cell)
# 5) add any new sentences to the AI's knowledge base
# if they can be inferred from existing knowledge
for sentence1 in self.knowledge:
for sentence2 in self.knowledge:
if sentence1 == sentence2:
continue
if sentence1.cells.issubset(sentence2.cells):
new_cells = sentence2.cells - sentence1.cells
new_count = sentence2.count - sentence1.count
new_sentence = Sentence(new_cells, new_count)
if new_sentence and new_sentence not in self.knowledge:
self.knowledge.append(new_sentence)
# Remove empty sentences
self.knowledge = [sentence for sentence in self.knowledge if sentence.cells]
if pre_knowlodges == self.knowledge: break
附上完整的 minesweeper.py 与 runner.py。
（建议前往官网下载相关内容以获得更佳体验）
Thanks
本笔记中代码大部分注释由 Copilot 倾情提供 ~（