Z3 to solve a puzzle(8 blocks tiles) please?

Question

I'm trying to solve the problem from the following description, and here is my code: my idea is the following.

1. empty space is expressed as 1524.
2. in each step s, a block moves into that empty space.
3. the block that moves in, has constraints. it can be either right, left, top or bottom from the empty space.
4. in the next round, values are swapped.

What's not working? currently, If I try to prevent more than 2 blocks moving, z3 does not give me sat. that is part:

(= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
)
)

However, if I remove, for example, the last ite (ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0), then z3 gives me sat. But I do not want that because then 3 values are changed in each step. I want only 2 blocks to change in each step (by swapping).

--------here begines the entire code

; (1,1) (1,2) (1,3) (2,1) (2,2) (2,3) (3,1) (3,2) (3,3)
; step, row, column
(declare-fun B (Int Int Int) Int)
(declare-const N Int)

(= 8 (B 0 1 1))
(= 7 (B 0 1 2))
(= 6 (B 0 1 3))
(= 5 (B 0 2 1))
(= 4 (B 0 2 2))
(= 3 (B 0 2 3))
(= 2 (B 0 3 1))
(= 1 (B 0 3 2))
(= 1524 (B 0 3 3))

;final state
(= 1 (B N 1 1))
(= 2 (B N 1 2))
(= 3 (B N 1 3))
(= 4 (B N 2 1))
(= 5 (B N 2 2))
(= 6 (B N 2 3))
(= 7 (B N 3 1))
(= 8 (B N 3 2))
(= 1524 (B N 3 3))

; only two blocks can move at a time
; not working at the moment..
(forall ((s Int))
(implies
(<= 0 s N)
(and 
; in each round, there is an empty block. an empty block...
; x1 and y1 are the coordinates of the block that will move in.
(exists ((x Int) (y Int) (x1 Int) (y1 Int))
(and
(<= 1 x 3)
(<= 1 y 3)
(<= 1 x1 3)
(<= 1 y1 3)
(= 1524 (B s x y))
(= 1
(+ ; it can be only one block out of the following options: top, bottom, right, left
;right
(ite (and (= x1 x) (= y1 (+ y 1))) 1 0)
;left
(ite (and (= x1 x) (= y1 (- y 1))) 1 0)
;top
(ite (and (= y1 y) (= x1 (+ x 1))) 1 0)
;bottom
(ite (and (= y1 y) (= x1 (- x 1))) 1 0)
)
)
(= (B (+ s 1) x y) (B s x1 y1))
(= (B (+ s 1) x1 y1) (B s x y))
))
)))

(forall ((s Int))
(implies
(<= 0 s N)
(= 1
(+
(ite (= 1524 (B s 1 1)) 1 0)
(ite (= 1524 (B s 1 2)) 1 0)
(ite (= 1524 (B s 1 3)) 1 0)
(ite (= 1524 (B s 2 1)) 1 0)
(ite (= 1524 (B s 2 2)) 1 0)
(ite (= 1524 (B s 2 3)) 1 0)
(ite (= 1524 (B s 3 1)) 1 0)
(ite (= 1524 (B s 3 2)) 1 0)
(ite (= 1524 (B s 3 3)) 1 0)
)
)
))

(not (exists ((s Int))
(implies
(<= 0 s N)
(<= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
))
)
))


))

help please!

Answer 1

Why unsat

The reason you're getting unsat is your last constraint:

(not (exists ((s Int))
(implies
(<= 0 s N)
(<= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
))
)
))

If you push the negation inside, this constraint is of the form:

forall s. not (implies (<= 0 s N) Q)

where I replaced the entire (<= 2 ...) part with Q.

If you replace not (implies a b) with its equivalent a && not b, we get:

forall s. (<= 0 s N) && not Q

To satisfy this, you have to satisfy both conjuncts, and in particular the following has to be sat:

forall s. (<= 0 s N)

What does it mean for a universally quantified formula to be satisfiable? Well, it has to be true. But clearly not all s is less than N, for any given N since integers are unbounded. So, this clause by itself is unsatisfiable.

This is the reason why you're getting unsat.

Modeling

You didn't ask, but implicit in your question is how to model such a puzzle using an SMT solver. There could be many ways to model it, of course, and your use of B to model the board as an uninterpreted function is an interesting one. In the presence of quantifiers, the logic is semi-decidable. Addition of uninterpreted-functions doesn't necessarily make the problem harder by itself, but it necessitates the use of quantifiers. That is, even if you were to fix your constraints to correctly capture the semantics, it may still be too hard for the solver to get a satisfying model.

Furthermore, problems such as these are usually not suitable for SMT solvers. Where SMT solvers shine is the T part: modulo-theories. There's no real theory based reasoning here. (The use of integers and comparisons is obviously arithmetic, but only at the surface level. There isn't really any "mathematical" reasoning going on here.) So, unless someone builds a satisfiability modulo "sliding-8-puzzle" theory, the solver ends up mostly relying on SAT reasoning, and these sorts of constraints lead to a huge number of clauses. If you add quantifiers to the story, it then becomes even more difficult.

But if your goal is to just use an SMT solver (even though it may not be the best tool), I'd recommend a different style of modeling. Avoid quantifiers. Instead, generate longer-and-longer lists of "moves". (Left-up-down, Left-left-up, etc.) Make these symbolic. Calculate the final board based on these symbolic moves, and see if you can match the final state starting from the first. By iteratively deepening the length of this sequence, you can find a solution eventually.

Note that this strategy, while decidable, isn't necessarily going to be efficient. If there's a solution in a small number of steps, say 10 or so, you can probably generate it fairly quickly. But with each additional length, it'll most likely suffer from combinatorial explosion. The particular starting state you chose, for instance, requires 62 moves (I think!), and it'd be unreasonable for the SMT solver to come up with that in a short amount of time. At least not for the state of the art.

Let us know how your explorations go; would love to hear if you can fix your current formalization and can get a solution in a reasonable amount of time.

One possible solution

Below is a possible implementation of the "iterative-deepening" idea I described above. I'll use z3py since SMTLib isn't really suitable for programming. (It's mostly intended for machine generated code.)

from z3 import *

Direction, (Up, Down, Left, Right) = EnumSort('Direction', ('Up', 'Down', 'Left', 'Right'))

class Grid:
    def __init__(self, board = None):
        self.board = board

        # Find the location of zero if a board is given
        if board:
           zeroLoc = [e for row in board for e in row].index(0)
           self.x  = zeroLoc // 3
           self.y  = zeroLoc %  3

# Pick a symbolic location from the grid
def pick(grid, x, y):
    val = 0
    for row in range(3):
        for col in range(3):
            val = If(And(row == y, col == x), grid.board[row][col], val)
    return val

# Move in a particular direction, if possible
def move(goodSofar, direction, grid):
    invalid = Or( And(direction == Up,    grid.y <= 0)
                , And(direction == Down,  grid.y >= 2)
                , And(direction == Left,  grid.x <= 0)
                , And(direction == Right, grid.x >= 2)
                , Not(goodSofar)
                )

    newGrid   = Grid()
    newGrid.x = If(invalid, grid.x, If(direction == Left, grid.x - 1, If(direction == Right, grid.x + 1, grid.x)))
    newGrid.y = If(invalid, grid.y, If(direction == Up,   grid.y - 1, If(direction == Down,  grid.y + 1, grid.y)))
    newVal    = pick(grid, newGrid.x, newGrid.y)

    newBoard  = [If(invalid, e, If(And(grid.x    == c, grid.y    == r), newVal,
                                If(And(newGrid.x == c, newGrid.y == r), 0, e)))
                 for (r, row) in enumerate(grid.board) for (c, e) in enumerate(row)]

    newGrid.board = [newBoard[0:3], newBoard[3:6], newBoard[6:9]]

    return (Not(invalid), newGrid)

# helper, for debugging
def prt(grid):
    print("%s-%s" % (simplify(grid.x), simplify(grid.y)))
    print("[%s, %s, %s]" % (simplify(grid.board[0][0]), simplify(grid.board[0][1]), simplify(grid.board[0][2])))
    print("[%s, %s, %s]" % (simplify(grid.board[1][0]), simplify(grid.board[1][1]), simplify(grid.board[1][2])))
    print("[%s, %s, %s]" % (simplify(grid.board[2][0]), simplify(grid.board[2][1]), simplify(grid.board[2][2])))

# Starting and ending boards
initBoard = [[8,7,6],[5,4,3],[2,1,0]]
hardBoard = [[1,2,3],[4,5,6],[7,8,0]]
easyBoard = [[0,8,7],[5,4,6],[2,1,3]]

finalBoard = easyBoard

if __name__ == "__main__":
  # Iteratively search for a solution
  moves = 0

  while True:
      print("Looking for a solution with %d moves.." % moves)

      symMoves = [Const("m_%d" % i, Direction) for i in range(moves)]

      moves += 1

      newBoard = Grid(initBoard)
      good     = True
      for d in symMoves:
          (valid, newBoard) = move(good, d, newBoard)
          good              = And(good, valid)

      s = Solver()
      s.add(good)
      for (req, got) in zip([e for row in finalBoard for e in row], [e for row in newBoard.board for e in row]):
          s.add(req == got)

      r = s.check()

      if r == unsat: continue

      if r == sat:
          print(s.model())
          break

      raise Exception("Solver said: %s", r)

Note that for finalBoard I picked something simple. When I run this, I get:

Looking for a solution with 0 moves..
Looking for a solution with 1 moves..
Looking for a solution with 2 moves..
Looking for a solution with 3 moves..
Looking for a solution with 4 moves..
[m_0 = Up, m_1 = Up, m_2 = Left, m_3 = Left]

and this is the correct solution. But, if you try setting finalBoard to be hardBoard (the one from your example), you'll see that it iteratively deepens, but each iteration is slower and slower. I haven't waited long enough than 19 moves. If you have a sufficiently large amount of memory and are willing to wait, I trust it'll solve the problem; but the wait times can be unreasonable.

You can try adding extra constraints the help the solver find a solution quicker perhaps. I did experiment with some simplifying clauses (like computing if the set of moves given is valid early enough). One can imagine other constraints (for instance you shouldn't have any sequence of moves where two subsequent moves undo each other, such as left-right, up-down etc). It isn't clear to me if such constraints would speed things up at all, but it might be worth exploring.