引言：基于 Z3 的网格路径查找
在计算机科学和人工智能领域，路径查找是一个经典问题，广泛应用于游戏开发、机器人导航、物流规划等场景。当路径查找涉及到复杂规则或多重条件时，传统的图搜索算法（如 bfs、dfs、a*）可能难以直接表达所有约束。此时，约束编程和定理证明器（如 z3）便能发挥其独特优势。
本教程将以一个“冰湖寻路”问题为例，演示如何使用 Python Z3 库来寻找一个从起点到终点的安全路径。冰湖被表示为一个二维矩阵，其中某些单元格是安全的（可通行），而另一些则是不安全的（不可通行）。我们的目标是找到一条完全由安全单元格组成的路径。
问题描述与 Z3 建模思想
假设我们有一个 rows x cols 的网格，每个单元格的值为 1 表示安全，0 表示不安全。给定起始坐标 (start_row, start_col) 和目标坐标 (end_row, end_col)，我们需要找到一条从起点到终点的路径，该路径上的所有单元格都必须是安全的，并且每一步只能移动到相邻（上下左右）的单元格。
传统 Z3 建模的误区
在尝试使用 Z3 解决此类问题时，一个常见的直觉是为网格中的每个单元格创建一个布尔变量 cell_i_j，表示该单元格是否在路径上。然后，通过添加相邻单元格之间的连接约束来构建路径。然而，这种方法往往难以有效表达路径的连通性、唯一性以及从起点到终点的明确序列。特别是，它很难确保找到的是一个 路径，而不仅仅是一组分散的、满足局部连接条件的单元格。
正确的 Z3 建模思路：路径符号化
解决这类问题的关键在于改变建模视角：我们不应该尝试建模网格中的 每个单元格 是否在路径上，而是应该直接建模 路径本身。这意味着我们将路径表示为一个由符号整数坐标对组成的序列。Z3 的任务就是为这些符号坐标赋值，使其满足所有路径规则。
立即学习“Python免费学习笔记（深入）”；
例如，如果路径最长可能为 N 步，我们可以创建 N 对符号整数变量 (x_0, y_0), (x_1, y_1), ..., (x_{N-1}, y_{N-1})，其中 (x_i, y_i) 代表路径上第 i 个单元格的坐标。然后，我们对这些符号变量施加一系列约束：
- 起点约束：x_0 和 y_0 必须等于起始坐标。
- 移动合法性：对于任意连续的路径点 (x_i, y_i) 和 `(
