华容道之水，不下赤壁。—— 孔明(火凤燎原)
问题
慕慕妈妈给慕慕外卖凑单，多买了一个华容道游戏。
看到这种面板，脑子里自然而然的涌现几个问题：
- 所有可能的排列有多少种？分别是什么？
- 所有可能的关卡有多少种？分别是什么？（有答案的排列才能称之为关卡）
- 给定一个关卡，怎么写一个程序自动求解？
针对这些问题，一个一个的解决。所有代码和数据文件在 https://github.com/kainwen/misc/tree/main/dancing_links
短答案
- 所有可能的排列有75893760个，去重后有1581120个布局
- 所有可能的关卡有1294896个
- 程序见下面
用Dancing Link解决所有排列问题
思路和之前解决幽灵捕手的技术一样，可以参考：👻幽灵捕手——Dancing Links。
华容道盘面是一个4*5的面板，角色包含要逃跑的曹贼和蜀汉的五虎将+四卒，共计10个角色。每个角色是一块牌子，尺寸不同，曹贼是2*2，士卒都是1*1的，五虎将除了关二爷都是1*2，关二爷是2*156。最后剩下两个空位。先对面部建模，构建坐标系，给每个方格标上序号：
每个角色的牌子，可以用下面的关键元素建模：
- 左下角的坐标
- 长度和宽度
每个角色和空位对应的序号如下：
- (1) 曹操
- (2) 关羽
- (3) 张飞
- (4) 赵云
- (5) 马超
- (6) 黄忠
- (7) 士卒1
- (8) 士卒2
- (9) 士卒3
- (10) 士卒4
- (11) 空位1
- (12) 空位2
构造一个输入给Dancing Link的矩阵，每行有32列：前12列分别对应一个角色（按上面的序号），后20列对应面板上的格子（第13列对应第1格，第14列对应第2格，以此类推）。
如果把曹操放在占据1，2，5，6四个格子（即曹操左下角坐标{0,0}, 右上角坐标{2,2}），那么描述这种摆放的一行是：
1 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0
我们写一个程序打印所有上述的行，然后丢给Dancing Link求解全部答案。华容道问题，不需要考虑旋转，比幽灵捕手略简单一些。
#-*- coding: utf-8 -*-
from collections import namedtuple
from fractions import Fraction
Block = namedtuple('Block', ['id', 'name', 'width', 'height'])
CaoCao = Block(1, 'CaoCao', 2, 2)
GuanYu = Block(2, 'GuanYu', 2, 1)
ZhangFei = Block(3, 'ZhangFei', 1, 2)
ZhaoYun = Block(4, 'ZhaoYun', 1, 2)
MaChao = Block(5, 'MaChao', 1, 2)
HuangZhong = Block(6, 'HuangZhong', 1, 2)
Zu1 = Block(7, 'Zu1', 1, 1)
Zu2 = Block(8, 'Zu2', 1, 1)
Zu3 = Block(9, 'Zu3', 1, 1)
Zu4 = Block(10, 'Zu4', 1, 1)
Empty1 = Block(11, 'Empty1', 1, 1)
Empty2 = Block(12, 'Empty2', 1, 1)
half = Fraction(1, 2)
mid2pointid = dict()
for i in range(4):
for j in range(5):
x = i + half
y = j + half
mid2pointid[(x,y)] = j*4 + i + 1
def try_block(block):
r = []
for x in range(0, 5):
if x + block.width > 4: continue
for y in range(0, 6):
if y + block.height > 5: continue
row = [0] * 32
row[block.id-1] = 1
for i in range(block.width):
for j in range(block.height):
key = (x + i + half, y + j + half)
pointid = mid2pointid[key]
row[pointid+11] = 1
r.append(row)
return r
rows = []
for b in [CaoCao, GuanYu, ZhangFei, ZhaoYun, MaChao, HuangZhong,
Zu1, Zu2, Zu3, Zu4, Empty1, Empty2]:
rows.extend(try_block(b))
print(len(rows), 32)
for r in rows:
print(" ".join([str(i) for i in r]))
上面这个程序跑出来的结果，丢给Dancing Link，竟然跑出来几千万条配置：
➜ dancing_links git:(main) ✗ wc -l all
75893760 all
我们考虑一下优化，四个卒不要四个角色了，俩空格也只当一个角色。但这俩就需要单独处理。这样看看能减少到多少。这样总共的角色数目就成了8个，然后加上20个位置，新的矩阵的每一行就应该是28列。Python程序改成下面的：
#-*- coding: utf-8 -*-
from collections import namedtuple
from fractions import Fraction
import itertools
Block = namedtuple('Block', ['id', 'name', 'width', 'height'])
CaoCao = Block(1, 'CaoCao', 2, 2)
GuanYu = Block(2, 'GuanYu', 2, 1)
ZhangFei = Block(3, 'ZhangFei', 1, 2)
ZhaoYun = Block(4, 'ZhaoYun', 1, 2)
MaChao = Block(5, 'MaChao', 1, 2)
HuangZhong = Block(6, 'HuangZhong', 1, 2)
half = Fraction(1, 2)
mid2pointid = dict()
for i in range(4):
for j in range(5):
x = i + half
y = j + half
mid2pointid[(x,y)] = j*4 + i + 1
def try_block(block):
r = []
for x in range(0, 5):
if x + block.width > 4: continue
for y in range(0, 6):
if y + block.height > 5: continue
row = [0] * 28
row[block.id-1] = 1
for i in range(block.width):
for j in range(block.height):
key = (x + i + half, y + j + half)
pointid = mid2pointid[key]
row[pointid+7] = 1
r.append(row)
return r
rows = []
for b in [CaoCao, GuanYu, ZhangFei, ZhaoYun, MaChao, HuangZhong]:
rows.extend(try_block(b))
#Zu's ID = 7
#Empty's ID = 8
def handle_special(id_number, size):
r = []
for comb in itertools.combinations(range(1, 21), size):
row = [0] * 28
row[id_number-1] = 1
for k in comb:
row[k+7] = 1
r.append(row)
return r
rows.extend(handle_special(7, 4))
rows.extend(handle_special(8, 2))
print(len(rows), 28)
for r in rows:
print(" ".join([str(i) for i in r]))
再丢给Dancing Link程序，就少了很多，还剩下150多万种，程序也很快就跑完了：
➜ dancing_links git:(main) ✗ python3 huarongdao.py > gm2
➜ dancing_links git:(main) ✗ ./a.out < gm2 > all.2
➜ dancing_links git:(main) ✗ wc -l all.2
1581120 all.2
再用下面的程序，随机验证一些方案，跑了几次都是对的。
import sys
import random
gm_file = sys.argv[1]
solution_file = sys.argv[2]
with open(gm_file) as f:
f.readline()
mat = f.readlines()
with open(solution_file) as g:
ss = g.readlines()
for i in range(10):
s = random.choice(ss)
index = [int(k) for k in s.strip().split()]
n = sum([int("".join(mat[idx].strip().split()))
for idx in index])
st = set(str(n))
assert(len(st) == 1 and n%10 == 1)
跑的结果（没有AssertFail）：
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm2 all.2
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm2 all.2
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm2 all.2
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm2 all.2
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm2 all.2
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm all
➜ dancing_links git:(main) ✗ python3 huarongdao_verify.py gm all
用下面的程序可以随机画出版面，方便直观看看：
import matplotlib.pyplot as plt
import matplotlib
from fractions import Fraction
import random
import sys
fig = plt.figure()
ax = fig.add_subplot()
fig.subplots_adjust(top=0.85)
plt.gca().set_xlim([0, 4])
plt.gca().set_ylim([0, 5])
plt.gca().set_aspect('equal', adjustable='box')
half = Fraction(1, 2)
mid2pointid = dict()
pointid2mid = dict()
for i in range(4):
for j in range(5):
x = i + half
y = j + half
mid2pointid[(x,y)] = j*4 + i + 1
pointid2mid[j*4 + i + 1] = (x,y)
names = ['曹操', '关羽', '张飞', '赵云', '马超', '黄忠', '兵', '空']
colors = ['b', 'g', 'k', 'c', 'm', 'y', 'r', 'w']
def plot(line):
row = [int(i) for i in line.strip().split()]
id_number = row.index(1)
name = names[id_number]
color = colors[id_number]
for i, v in enumerate(row[8:]):
if v == 1:
p = i+1
x, y = pointid2mid[p]
ax.text(float(x), float(y), name, color=color,
family='WenQuanYi Zen Hei', ha='center', va='center')
gm_file = sys.argv[1]
solution_file = sys.argv[2]
with open(gm_file) as f:
f.readline()
mat = f.readlines()
with open(solution_file) as g:
ss = g.readlines()
s = random.choice(ss)
index = [int(k) for k in s.strip().split()]
for i in index:
plot(mat[i])
ax.text(2, -0.4, '出 口', color='k',
family='WenQuanYi Zen Hei', ha='center', va='center')
plt.grid()
plt.savefig("a.png", dpi=400)
随机画了一些图如下：
华容道自动求解程序
还剩下两个问题，都需要有程序自动求解华容道。上面罗列的所有可能的盘面里，有一类已经是结果局面，也就是“曹操”占据2，3，6，7四个格子。这个模式翻译成行是：
1 0 0 0 0 0 0 0 0 1 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0
上面对应gm2文件里的第4行（从第0行开始算），去all2里搜索包含第4行的解答，合计有16万多：
gpadmin@zlyu-rr:~/workspace/misc/dancing_links$ grep '^4 ' all2 | wc -l
163080
gpadmin@zlyu-rr:~/workspace/misc/dancing_links$ grep '^4 ' all2 | head -5
4 14 27 46 66 85 2863 5125
4 14 27 46 66 85 2866 5119
4 14 27 46 66 85 2867 5118
4 14 27 46 66 85 2888 5097
4 14 27 46 66 85 2889 5096
下面考虑构建状态编码和状态转移。一个盘面配置是一个状态，它对应且仅对应all2中某一行，所以我们可以用all2对应行的行号作为状态的编码。但这个不利于直观理解和端的输入输出，我们需要设计一个转换。人直观容易理解的输入输出是：8种角色，每个角色告知位置。考虑角色顺序固定是：曹操，关羽，张飞，赵云，马超，黄忠，士卒，空白，从0开始给每个角色编码。那么一个盘面的配置可以用下面的类型表示：
type role_pos() :: [integer()].
type board() :: [role_pos()].
上面的完成状态的示意图里的左侧的图，用这种办法表示，就是
[
[2,3,6,7], #曹操
[9,10], #关羽
[1,5], #张飞
[13,17], #赵云
[14,18], #马超
[11,15], #黄忠
[4,8,16,20], #士卒
[12,19] #空白
]
所有的角色牌（不考虑空格）的可以进行的基本操作只有4个：向上走一步，向下走一步，向左走一步，向右走一步。一步操作如果是可行的，那么其移动一步后，新的坐标位置里的格点要么之前是空格，要么之前就是自己占据。还是用上面的“完成状态的配置示意图”的左图为案例：黄忠可以上移但不能左移。移动对应原来位置变化：上移(+4)，下移(-4)，左移(-1), 右移(+1)。可以利用空格作为引子，罗列某个盘面潜在的可能的移动：找出空格所有的邻接点，潜在的移动必然是把邻接点的内容移动到空格中。
用程序跑出来200的下一个状态有4个：[207, 125, 215, 198]。我们都画出图来，验证:
罗列全部状态后，存储成二进制文件，也没多大，才28MB，符合预期，稀疏图。
➜ dancing_links git:(main) ✗ ls -alh fsm
-rw-r--r--@ 1 zlyu staff 28M Jan 6 15:24 fsm
给定任何一个初始化配置（游戏关卡），我们遍历所有终止位，然后用dijkstra算法找路径即可。这部分用了python的库networkx。下面的案例是网上找了一关：
➜ dancing_links git:(main) ✗ cat huarongdao_test
[(14,15,18,19),(10,11),(5,9),(8,12),(13,17),(16,20),(1,4,6,7),(2,3)]
python3 huarongdao_solver.py < huarongdao_test > labels
最后写了一个网页可以打印每一步过程和移动步骤，截图如下：
- 图片的名字是：
<序号>.<状态编码号>.png - 图片右下角是通向下一步的步骤
这块代码是：
# -*- coding: utf-8 -*-
import matplotlib.pyplot as plt
import matplotlib
from fractions import Fraction
from copy import deepcopy
import pickle, sys
import networkx as nx
class HuarongDao:
ADJ_INFO = [
None, #0, place holder
[2,5], #1
[1,3,6], #2
[2,4,7], #3
[3,8], #4
[1,6,9], #5
[2,5,7,10], #6
[3,6,8,11], #7
[4,7,12], #8
[5,10,13], #9
[6,9,11,14], #10
[7,10,12,15], #11
[8,11,16], #12
[9,14,17], #13
[10,13,15,18], #14
[11,14,16,19], #15
[12,15,20], #16
[13,18], #17
[14,17,19], #18
[15,18,20], #19
[16,19] #20
]
NAMES = ['曹操', '关羽', '张飞', '赵云', '马超', '黄忠', '兵', '空']
def __init__(self, gm_file, all_file):
self.gm_file = gm_file
self.all_file = all_file
self.state_built = False
def build_states(self):
# each state is
if self.state_built:
return
with open(self.gm_file) as f:
f.readline()
mat = [list(map(int, line.strip().split()))
for line in f]
self.state_keys = []
self.boards = []
self.boards_rev_index = []
self.keys_to_state = dict()
self.board_to_state = dict()
with open(self.all_file) as g:
for i, line in enumerate(g):
keys = tuple(sorted(list(map(int, line.strip().split()))))
self.state_keys.append(keys)
self.keys_to_state[keys] = i
board = []
board_rev_index = dict()
for k in keys:
pos = []
bits = mat[k]
assert(bits.index(1) == len(board))
for j, b in enumerate(bits[8:]):
if b == 1:
pos.append(j+1)
board_rev_index[j+1] = len(board)
board.append(pos)
self.boards.append(board)
self.boards_rev_index.append(board_rev_index)
self.board_to_state[tuple([tuple(lst) for lst in board])] = i
self.state_built = True
def dump_objs(self):
assert(self.state_built)
with open("boards", "wb") as f:
pickle.dump(self.boards, f)
with open("boards_rev_index", "wb") as f:
pickle.dump(self.boards_rev_index, f)
with open("keys_to_state", "wb") as f:
pickle.dump(self.keys_to_state, f)
with open("board_to_state", "wb") as f:
pickle.dump(self.board_to_state, f)
def load_objs(self):
with open("boards", "rb") as f:
self.boards = pickle.load(f)
with open("boards_rev_index", "rb") as f:
self.boards_rev_index = pickle.load(f)
with open("keys_to_state", "rb") as f:
self.keys_to_state = pickle.load(f)
with open("board_to_state", "rb") as f:
self.board_to_state = pickle.load(f)
self.state_built = True
def draw(self, state_id, fn):
assert(self.state_built)
fig = plt.figure()
ax = fig.add_subplot()
fig.subplots_adjust(top=0.85)
plt.gca().set_xlim([0, 4])
plt.gca().set_ylim([0, 5])
plt.gca().set_aspect('equal', adjustable='box')
half = Fraction(1, 2)
one_over_ten = Fraction(1, 10)
mid2pointid = dict()
pointid2mid = dict()
for i in range(4):
for j in range(5):
x = i + half
y = j + half
mid2pointid[(x,y)] = j*4 + i + 1
pointid2mid[j*4 + i + 1] = (x,y)
ax.text(float(i+one_over_ten), float(j+one_over_ten),
str(j*4 + i + 1), color='k', ha='center', va='center')
colors = ['b', 'g', 'k', 'c', 'm', 'y', 'r', 'w']
board = self.boards[state_id]
for i, (name, pos) in enumerate(zip(self.NAMES, board)):
color = colors[i]
for p in pos:
x, y = pointid2mid[p]
ax.text(float(x), float(y), name, color=color,
family='Songti SC', ha='center', va='center')
plt.grid()
plt.savefig(fn, dpi=400, bbox_inches='tight')
plt.cla()
plt.clf()
plt.close()
def next_state(self, state_id):
board = self.boards[state_id]
board_rev_index = self.boards_rev_index[state_id]
empty_pos = board[-1]
new_state_ids = []
for ep in empty_pos:
adjs = self.ADJ_INFO[ep]
for p in adjs:
role_id = board_rev_index[p]
if role_id == len(board) - 1: #empty
continue
role_pos = board[role_id]
new_state_id = self.move(role_id, p, ep, board, board_rev_index)
if new_state_id:
if p - ep == 1:
action = "left"
elif p - ep == 4:
action = "down"
elif ep - p == 1:
action = "right"
else:
action = "up"
label = "move %s at %s %s one step" % (self.NAMES[role_id], p, action)
self.edge_labels[(state_id, new_state_id)] = label
new_state_ids.append(new_state_id)
return new_state_ids
def move(self, role_id, role_pos, empty_pos, board, board_rev_index):
if role_id == len(board) - 2:
#兵
return self.move_bing(role_pos, empty_pos, board)
else:
old_pos = board[role_id]
delta = empty_pos - role_pos
new_pos = [p+delta for p in old_pos]
for p in new_pos:
if ((p <= 0 or p > 20) or
(board_rev_index[p] != role_id and
board_rev_index[p] != len(board) - 1)):
return None
bd = deepcopy(board)
bd[role_id] = new_pos
bd[-1] = []
st = set()
for x in bd:
for p in x:
st.add(p)
es = list(set(range(1,21)) - st)
es.sort()
bd[-1] = es
return self.board_to_state[tuple([tuple(lst) for lst in bd])]
def move_bing(self, role_pos, empty_pos, board):
bd = deepcopy(board)
old_empty = bd[-1]
old_bing = bd[-2]
old_bing.remove(role_pos)
old_bing.append(empty_pos)
old_empty.remove(empty_pos)
old_empty.append(role_pos)
old_bing.sort()
old_empty.sort()
return self.board_to_state[tuple([tuple(lst) for lst in bd])]
def create_and_dump_fsm(self):
assert(self.state_built)
self.edge_labels = dict()
fsm = []
for i in range(len(self.boards)):
states = self.next_state(i)
fsm.append(tuple(states))
with open("fsm", "wb") as f:
pickle.dump(fsm, f)
with open("edge_labels", "wb") as f:
pickle.dump(self.edge_labels, f)
def load_fsm(self):
with open("fsm", "rb") as f:
self.fsm = pickle.load(f)
with open("edge_labels", "rb") as f:
self.edge_labels = pickle.load(f)
def load_game(self):
#print("please input a game:")
line = sys.stdin.readline()
bd = eval(line)
state_id = self.board_to_state[tuple([tuple(lst) for lst in bd])]
return state_id
def get_all_finish_state_ids(self):
return [i
for i, board in enumerate(self.boards)
if board[0] == [2,3,6,7]]
def build_graph(self):
assert(self.state_built)
self.load_fsm()
G = nx.DiGraph()
for i in range(len(self.boards)):
G.add_node(i)
for i,t in enumerate(self.fsm):
for j in t:
G.add_weighted_edges_from([(i, j, 1)])
return G
def solve(self):
start_state = self.load_game()
if self.boards[start_state][0] == [2,3,6,7]:
return [start_state]
G = self.build_graph()
for i, board in enumerate(self.boards):
if board[0] == [2,3,6,7]:
try:
nodes = nx.dijkstra_path(G, start_state, i)
return nodes
except nx.NetworkXNoPath:
continue
h = HuarongDao("gm2", "all2")
h.load_objs()
path = h.solve()
states = []
if path is not None:
for i, st in enumerate(path):
h.draw(st, "%s.%s.png" % (i, st))
states.append(st)
if h.boards[st][0] == [2,3,6,7]:
break
for i in range(len(states) - 1):
start = states[i]
end = states[i+1]
label = h.edge_labels[(start,end)]
print(label)
其实直接分析fsm就可以了，而且是无向图（动作可逆），写个回答问题的程序：
import networkx as nx
import pickle
with open("edges", "rb") as f:
edges = pickle.load(f)
with open("boards", "rb") as f:
boards = pickle.load(f)
finish_set = set(i for i,b in enumerate(boards) if b[0] == [2,3,6,7])
G = nx.Graph()
G.add_nodes_from(range(len(boards)))
G.add_edges_from(edges)
n = 0
for C in nx.connected_components(G):
if C & finish_set:
n += len(C)
print(n)
建模成矩形覆盖问题用z3求解
最开始的思路是这个。留个参考资料未完待续了。
Pingback: 慕慕的玩具(4)：疯狂对对碰背后的数学模型 Steiner System和Finite Projective Plane(上) | Thoughts on Computing