使用Z3 Solver进行路径搜索时的移动约束建模错误解决

错误原因 #

你代码中的核心错误有两处：

1. 语法逻辑错误：s.add(x,y = ...) 完全不符合Z3的约束添加规则。s.add() 接收的是逻辑约束表达式，不能使用Python的赋值语法 =，且单步直接让Agent跳到终点的逻辑不成立——路径是多步移动的过程，而非一步到位。
2. Solver与solve函数混用：solve() 是Z3的独立求解函数，不能和手动创建的Solver对象一起使用，正确流程是通过Solver.add()添加所有约束后，调用Solver.check()求解。

正确建模思路 #

要实现Agent避障寻路，需要建模多步移动的状态序列：

• 为每一步的位置定义变量，记录Agent在不同步数的坐标
• 约束每一步的移动只能是上下左右的合法操作（不越界、不碰障碍物）
• 设置目标条件：存在某一步的位置与硬币坐标重合
• 可选：限制最大步数，避免无限求解

完整修正代码示例 #

from z3 import *

# 网格基础参数
GRID_SIZE = 7
OBSTACLES = {(2,3), (2,5), (3,1), (4,3), (4,4)}
AGENT_START = (2, 2)
COIN_POS = (4, 6)
MAX_STEPS = 20  # 限制最大步数，避免无限求解

# 定义每一步的位置变量：pos[i] = (x_i, y_i)，i为步数
pos = [(Int(f"x_{i}"), Int(f"y_{i}")) for i in range(MAX_STEPS + 1)]

s = Solver()

# 初始位置约束：第0步在Agent的起始点
s.add(pos[0][0] == AGENT_START[0])
s.add(pos[0][1] == AGENT_START[1])

# 每一步的移动约束
for i in range(MAX_STEPS):
    x_curr, y_curr = pos[i]
    x_next, y_next = pos[i+1]
    
    # 定义四个方向的移动规则
    move_right = And(x_next == x_curr + 1, y_next == y_curr)
    move_left = And(x_next == x_curr - 1, y_next == y_curr)
    move_up = And(x_next == x_curr, y_next == y_curr + 1)
    move_down = And(x_next == x_curr, y_next == y_curr - 1)
    
    # 约束下一步必须是四个合法移动之一
    s.add(Or(move_right, move_left, move_up, move_down))
    
    # 约束下一步位置合法：在网格内部，且不是障碍物
    s.add(x_next >= 1, x_next <= GRID_SIZE - 2)
    s.add(y_next >= 1, y_next <= GRID_SIZE - 2)
    for ox, oy in OBSTACLES:
        s.add(Not(And(x_next == ox, y_next == oy)))

# 目标约束：存在某一步到达硬币位置
goal = Or([And(pos[k][0] == COIN_POS[0], pos[k][1] == COIN_POS[1]) for k in range(MAX_STEPS + 1)])
s.add(goal)

# 求解并输出结果
if s.check() == unsat:
    print('Problem not solvable')
else:
    m = s.model()
    path = []
    for i in range(MAX_STEPS + 1):
        x_val = m.eval(pos[i][0]).as_long()
        y_val = m.eval(pos[i][1]).as_long()
        path.append((x_val, y_val))
        if (x_val, y_val) == COIN_POS:
            break
    print("Found path:")
    for step, (x, y) in enumerate(path):
        print(f"Step {step}: ({x}, {y})")

关键说明 #

1. 多步状态建模：用pos[i]记录第i步的坐标，符合路径逐步移动的实际逻辑。
2. 移动合法性约束：每一步只能选择四个方向之一，同时保证移动后的位置不在边界或障碍物上。
3. 目标条件：通过Or组合所有步数的终点条件，让Z3自动寻找最早到达硬币的路径。
4. 可选优化：如果需要避免路径循环，可以添加约束确保每个位置只被访问一次，不过会增加求解时间，短路径场景下可省略。

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