基于Z3定理证明器的冰湖寻路代码问题排查与修复

问题描述 #

需要在冰湖矩阵中找出从初始位置到目标位置的可行路径，矩阵中1代表安全单元格，0代表危险单元格，使用Z3定理证明器编写Python代码实现该需求。

示例说明 #

给定矩阵中，起点为D1（对应坐标(3,0)），终点为C3（对应坐标(2,2)）。安全单元格包括A1、A2、A3、B1、B3、C1、C3、D1，危险单元格为其余单元格，唯一有效路径为D1→C1→B1→A1→A2→A3→B3→C3。

原代码 #

from z3 import *

def find_path(matrix, start, end):
    # Define the dimensions of the matrix
    rows = len(matrix)
    cols = len(matrix[0])

    # Create Z3 variables for each cell in the matrix
    cells = [[Bool(f'cell_{i}_{j}') for j in range(cols)] for i in range(rows)]

    # Create a Z3 solver
    s = Solver()

    # Add constraints for the starting and destination positions
    s.add(cells[start[0]][start[1]])  # Starting position
    s.add(cells[end[0]][end[1]])  # Destination position

    # Add constraints for safe and unsafe cells
    for i in range(rows):
        for j in range(cols):
            if matrix[i][j] == 0:
                s.add(Not(cells[i][j]))  # Unsafe cell
            else:
                s.add(cells[i][j])  # Safe cell

    # Add constraints for adjacent cells
    for i in range(rows):
        for j in range(cols):
            adjacent_cells = []
            if i > 0:
                adjacent_cells.append(cells[i-1][j])  # Cell above
            if i < rows - 1:
                adjacent_cells.append(cells[i+1][j])  # Cell below
            if j > 0:
                adjacent_cells.append(cells[i][j-1])  # Cell to the left
            if j < cols - 1:
                adjacent_cells.append(cells[i][j+1])  # Cell to the right
            s.add(Implies(cells[i][j], Or(adjacent_cells)))  # Only connect to adjacent safe cells
    
    print(s)
    # Check if there is a valid path from the starting position to the destination
    if s.check() == sat:
        model = s.model()
        path = []
        for i in range(rows):
            for j in range(cols):
                if model[cells[i][j]]:
                    path.append((i, j))
        s.reset()
        return path
    else:
        return None

# Example usage
matrix = [[1, 1, 1, 0],
          [1, 0, 1, 0],
          [1, 0, 1, 0],
          [1, 0, 0, 0]]
start = (3, 0)
end = (2, 2)

path = find_path(matrix, start, end)
if path:
    print("Valid path found:")
    for cell in path:
        print(f"({chr(ord('A') + cell[0])}{cell[1] + 1})")
else:
    print("No valid path found.")

代码问题分析 #

1. 安全单元格约束错误：原代码强制所有值为1的安全单元格必须被选中（s.add(cells[i][j])），但路径只需要经过部分安全单元格，而非全部。这会导致模型返回所有安全单元格，而非仅路径上的节点。
2. 连通性约束缺失：原代码仅保证选中的单元格有至少一个相邻选中单元格，但未确保这些选中单元格形成从起点到终点的连通路径。比如起点和终点的安全单元格可能被孤立选中，中间没有连通的节点链。
3. 路径无顺序性：原代码收集所有选中的单元格，但未按路径顺序输出，无法直接得到如D1→C1→B1...这样的有序路径。

修复方案 #

核心修改点 #

• 移除强制所有安全单元格必须选中的约束，仅限制危险单元格不可选中。
• 添加可达性变量，定义每个单元格是否能从起点到达，确保终点可达，且所有可达单元格形成连通链。
• 增加路径顺序生成逻辑，将无序的路径节点整理为有序路径。

修复后的代码 #

from z3 import *

def find_path(matrix, start, end):
    rows = len(matrix)
    cols = len(matrix[0])

    # 定义两个变量矩阵：
    # cell_in_path：单元格是否在路径中
    # reachable：单元格是否从起点可达
    cell_in_path = [[Bool(f'path_{i}_{j}') for j in range(cols)] for i in range(rows)]
    reachable = [[Bool(f'reachable_{i}_{j}') for j in range(cols)] for i in range(rows)]

    s = Solver()

    # 起点必须在路径中且可达
    s.add(cell_in_path[start[0]][start[1]])
    s.add(reachable[start[0]][start[1]])

    # 终点必须在路径中且可达
    s.add(cell_in_path[end[0]][end[1]])
    s.add(reachable[end[0]][end[1]])

    # 危险单元格不能在路径中，也不可达
    for i in range(rows):
        for j in range(cols):
            if matrix[i][j] == 0:
                s.add(Not(cell_in_path[i][j]))
                s.add(Not(reachable[i][j]))

    # 可达性与路径连通约束
    for i in range(rows):
        for j in range(cols):
            if matrix[i][j] == 1:
                # 非起点的可达单元格，必须至少有一个相邻单元格可达（保证连通性）
                if (i, j) != start:
                    adjacent_reachable = []
                    if i > 0:
                        adjacent_reachable.append(reachable[i-1][j])
                    if i < rows - 1:
                        adjacent_reachable.append(reachable[i+1][j])
                    if j > 0:
                        adjacent_reachable.append(reachable[i][j-1])
                    if j < cols - 1:
                        adjacent_reachable.append(reachable[i][j+1])
                    s.add(Implies(reachable[i][j], Or(adjacent_reachable)))
                
                # 在路径中的单元格必须是可达的
                s.add(Implies(cell_in_path[i][j], reachable[i][j]))

                # 路径节点的相邻约束：区分起点、终点和中间节点
                adjacent_path = []
                if i > 0:
                    adjacent_path.append(cell_in_path[i-1][j])
                if i < rows - 1:
                    adjacent_path.append(cell_in_path[i+1][j])
                if j > 0:
                    adjacent_path.append(cell_in_path[i][j-1])
                if j < cols - 1:
                    adjacent_path.append(cell_in_path[i][j+1])
                
                if (i, j) == start or (i, j) == end:
                    # 起点和终点至少有一个相邻路径节点
                    s.add(Implies(cell_in_path[i][j], AtLeast(*adjacent_path, 1)))
                else:
                    # 中间节点必须至少有两个相邻路径节点，保证是路径的连续部分
                    s.add(Implies(cell_in_path[i][j], AtLeast(*adjacent_path, 2)))

    if s.check() == sat:
        model = s.model()
        # 收集所有在路径中的单元格
        path_nodes = [(i, j) for i in range(rows) for j in range(cols) if model[cell_in_path[i][j]]]
        
        # 生成有序路径：从起点开始，依次寻找相邻的路径节点
        ordered_path = [start]
        current = start
        while current != end:
            for node in path_nodes:
                if node == current or node in ordered_path:
                    continue
                # 判断是否为相邻单元格（曼哈顿距离为1）
                if abs(node[0] - current[0]) + abs(node[1] - current[1]) == 1:
                    ordered_path.append(node)
                    current = node
                    break
        return ordered_path
    else:
        return None

# 示例调用
matrix = [[1, 1, 1, 0],
          [1, 0, 1, 0],
          [1, 0, 1, 0],
          [1, 0, 0, 0]]
start = (3, 0)
end = (2, 2)

path = find_path(matrix, start, end)
if path:
    print("Valid path found:")
    path_str = "→".join([f"({chr(ord('A') + cell[0])}{cell[1] + 1})" for cell in path])
    print(path_str)
else:
    print("No valid path found.")

修复说明 #

1. 变量拆分：新增reachable变量跟踪单元格的可达性，cell_in_path变量标记路径成员，分离两个逻辑，便于精准约束。
2. 约束细化：
   • 仅限制危险单元格的不可达性，安全单元格由路径需求动态决定是否被选中。
   • 为起点、终点、中间节点设置不同的相邻约束，确保路径是连续的单链，而非孤立节点集合。
3. 路径排序：通过从起点遍历相邻路径节点的方式，将无序的路径节点整理为符合行走逻辑的有序路径，匹配示例输出格式。

内容的提问来源于stack exchange，提问作者atiwari