| CrackmesForBeginners (CFB) #2 |
z3py solver, the minimum path is N = 19 which is "SDDSSASSDDSSDDDSSDDD"
from z3 import *
maze = [ 0x00, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01,
0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x01,
0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01,
0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x01,
0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01,
0x01, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x01,
0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01,
0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x01,
0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01, 0x00, 0x00,
0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00, 0x02,
0x00, 0x00, 0x00, 0x00]
def try_solve(N):
s = Solver()
# one move variable per step, values 0/1/2/3 = A/D/S/W
move = [Int(f"move_{i}") for i in range(N)]
x = [Int(f"x_{i}") for i in range(N + 1)]
y = [Int(f"y_{i}") for i in range(N + 1)]
s.add(x[0] == 0, y[0] == 0)
for i in range(N):
s.add(Or(move[i] == 0, move[i] == 1, move[i] == 2, move[i] == 3))
for i in range(N):
s.add(x[i + 1] == If(move[i] == 0, x[i] - 1, If(move[i] == 1, x[i] + 1, x[i])))
s.add(y[i + 1] == If(move[i] == 2, y[i] + 1, If(move[i] == 3, y[i] - 1, y[i])))
for i in range(1, N + 1):
s.add(0 <= x[i], x[i] <= 9)
s.add(0 <= y[i], y[i] <= 9)
maze_arr = Array('maze', IntSort(), IntSort())
for idx, val in enumerate(maze):
maze_arr = Store(maze_arr, idx, val)
for i in range(1, N + 1):
s.add(Select(maze_arr, x[i] + 10 * y[i]) != 1)
s.add(x[N] == 9)
s.add(y[N] == 9)
mapping = {0: 'A', 1: 'D', 2: 'S', 3: 'W'}
if s.check() == sat:
m = s.model()
path = ''.join(mapping[m[move[i]].as_long()] for i in range(N))
print(path)
else:
print("unsat for N =", N)
for N in range(1, 30):
result = try_solve(N)
if result:
print(f"Found solution at N={N}: {result}")
break
else:
print("No solution found up to N=29") |
2026-07-14 23:49 |