使用像 z3 这样的 SMT 求解器确实可以进行这种搜索，尽管看起来您的方法并不合适。 （正如 cmets 中所指出的，就此而言，您的代码甚至不是有效的 Python 或 z3Py。）
考虑这个问题的最佳方法是双管齐下：
以下是按照这些思路解决您的问题的方法。我放在这里是为了让你更深入地学习和理解。如果这是你的家庭作业或学校项目或其他东西，提交它不会让你走得太远！除了我上面所说的，我特意不放置任何 cmet，希望您能研究它并在处理它时提出具体问题。
from z3 import *
Grid = [ ['T', 'T', 'T', 'T', 'T', 'T', 'T']
, ['T', ' ', ' ', ' ', ' ', ' ', 'T']
, ['T', ' ', 'A', 'O', ' ', 'O', 'T']
, ['T', 'O', ' ', ' ', ' ', ' ', 'T']
, ['T', ' ', ' ', 'O', 'O', 'C', 'T']
, ['T', ' ', ' ', ' ', ' ', ' ', 'T']
, ['T', 'T', 'T', 'T', 'T', 'T', 'T']
]
Cell, (Wall, Empty, Agent, Obstacle, Coin) = EnumSort('Cell', ('Wall', 'Empty', 'Agent', 'Obstacle', 'Coin'))
def mkCell(c):
if c == 'T':
return Wall
elif c == ' ':
return Empty
elif c == 'A':
return Agent
elif c == 'O':
return Obstacle
else:
return Coin
def grid(x, y):
result = Wall
for i in range (len(Grid)):
for j in range (len(Grid[0])):
result = If(And(x == IntVal(i), y == IntVal(j)), mkCell(Grid[i][j]), result)
return result
def validStart(x, y):
return grid(x, y) == Agent
def validEnd(x, y):
return grid(x, y) == Coin
def canMoveTo(x, y):
n = grid(x, y)
return Or(n == Empty, n == Coin, n == Agent)
def moveLeft(x, y):
return [x, If(canMoveTo(x, y-1), y-1, y)]
def moveRight(x, y):
return [x, If(canMoveTo(x, y+1), y+1, y)]
def moveUp(x, y):
return [If(canMoveTo(x-1, y), x-1, x), y]
def moveDown(x, y):
return [If(canMoveTo(x+1, y), x+1, x), y]
Dir, (Left, Right, Up, Down) = EnumSort('Dir', ('Left', 'Right', 'Up', 'Down'))
def move(d, x, y):
xL, yL = moveLeft (x, y)
xR, yR = moveRight(x, y)
xU, yU = moveUp (x, y)
xD, yD = moveDown (x, y)
xN = If(d == Left, xL, If (d == Right, xR, If (d == Up, xU, xD)))
yN = If(d == Left, yL, If (d == Right, yR, If (d == Up, yU, yD)))
return [xN, yN]
def solves(seq, x, y):
def walk(moves, curX, curY):
if moves:
nX, nY = move(moves[0], curX, curY)
return walk(moves[1:], nX, nY)
else:
return [curX, curY]
xL, yL = walk(seq, x, y)
return And(validStart(x, y), validEnd(xL, yL))
pathLength = 0
while(pathLength != 20):
print("Trying to find a path of length:", pathLength)
s = Solver()
seq = [Const('m' + str(i), Dir) for i in range(pathLength)]
x, y = Ints('x, y')
s.add(solves(seq, x, y))
if s.check() == sat:
print("Found solution with length:", pathLength)
m = s.model()
print(" Start x:", m[x])
print(" Start y:", m[y])
for move in seq:
print(" Move", m[move])
break;
else:
pathLength += 1
运行时，打印：
Trying to find a path of length: 0
Trying to find a path of length: 1
Trying to find a path of length: 2
Trying to find a path of length: 3
Trying to find a path of length: 4
Trying to find a path of length: 5
Found solution with length: 5
Start x: 2
Start y: 2
Move Down
Move Right
Move Right
Move Right
Move Down
因此，它找到了 5 步的解决方案；你可以在你的网格中追逐它，看看它确实是正确的。 （编号从左上角的 0,0 开始；随着向右和向下移动而增加。）
希望这可以帮助您在学习时取得进步并创建自己的版本。随时提出澄清问题；但请记住，如果这是家庭作业，那么按原样提交无疑会让您陷入困境，除非您真正理解此处提供的解决方案。