python z3 smt Bounded model

Question

I have developed a puzzle game. state of the game can be expressed as an Int array size of 12. the player can make only 4 moves. The aim of the game is to reach a certain state. I'm trying to solve this puzzle with python z3. here is the code.

a = Int('a')
b = Int('b')
s = Solver()
s.add(And(a >= 0, b >= 0, b <= a, a == 100))
f = Function('f', IntSort(), IntSort(), IntSort())

init = And(f(0, 1) == 1 , f(0, 2) == 1 , f(0, 3) == 1 , f(0, 4) == 2, f(0, 5) == 2 ,
    f(0, 6) == 2, f(0, 7) == 3, f(0, 8) == 3, f(0, 9) == 3 , f(0, 10) == 4 ,
    f(0, 11) == 4 , f(0, 12) == 4)

goal = And(f(b, 1) == 1 , f(b, 2) == 1 , f(b, 3) == 1 , f(b, 4)
    == 2 , f(b, 5) == 2 , f(b, 6) == 2 , f(b, 7) == 3 , f(b, 8) == 3 ,
    f(b, 9) == 3 , f(b, 10) == 4 , f(b, 11) == 4 , f(b, 12) == 4)

a is maximum number of moves. b is minimal number of moves to solve the problem. f is array of statess. goal is final-winner state.

def move(k):

    RIGHT = And(f(k + 1, 1) == f(k, 1), f(k + 1, 2) == f(k, 2), f(k + 1, 3) == f(k, 3),
            f(k + 1, 4) == f(k, 4), f(k + 1, 5) == f(k, 11) , f(k + 1, 6) == f(k, 5),
            f(k + 1, 7) == f(k, 6), f(k + 1, 8) == f(k, 8), f(k + 1, 9) == f(k, 7), 
            f(k + 1, 10) == f(k, 9), f(k + 1, 11) == f(k, 10), f(k + 1, 12) == f(k, 12))

    UP = And(f(k + 1, 1) == f(k, 1), f(k + 1, 2) == f(k, 8), f(k + 1, 3) == f(k, 2),
         f(k + 1, 4) == f(k, 3), f(k + 1, 5) == f(k, 5), f(k + 1, 6) == f(k, 4), 
         f(k + 1, 7) == f(k, 6), f(k + 1, 8) == f(k, 7), f(k + 1, 9) == f(k, 9),
         f(k + 1, 10) == f(k, 10), f(k + 1, 11) == f(k, 11), f(k + 1, 12) == f(k, 12))

    BOT = And(f(k + 1, 1) == f(k, 12), f(k + 1, 2) == f(k, 1), f(k + 1, 3) == f(k, 3),
          f(k + 1, 4) == f(k, 4), f(k + 1, 5) == f(k, 5), f(k + 1, 6) == f(k, 6), 
          f(k + 1, 7) == f(k, 7), f(k + 1, 8) == f(k, 2), f(k + 1, 9) == f(k, 8), 
          f(k + 1, 10) == f(k, 9), f(k + 1, 11) == f(k, 11), f(k + 1, 12) == f(k, 10))

    LEFT = And(f(k + 1, 1) == f(k, 3), f(k + 1, 2) == f(k, 2), f(k + 1, 3) == f(k, 4),
           f(k + 1, 4) == f(k, 5), f(k + 1, 5) == f(k, 11), f(k + 1, 6) == f(k, 6),
           f(k + 1, 7) == f(k, 7), f(k + 1, 8) == f(k, 8), f(k + 1, 9) == f(k, 9), 
           f(k + 1, 10) == f(k, 10), f(k + 1, 11) == f(k, 12), f(k + 1, 12) == f(k, 1))

    return Or(LEFT, UP, BOT, LEFT)

s.add(ForAll([b], move(b)))
s.add(init)
s.add(goal)
print(s.check())

move(k) express kth move that connects k+1 and k state. with s.add(ForAll([b], move(b))), I want for all integer k k>=0 k <=b to make move (I believe mistake is here). then I add, init and goal condition. solver never checks sat or unsat.

Any suggestions would be appreciated.

Your init and goal states are equivalent to each other. Is that intentional? — alias
Are these values sitting on some sort of a grid? Would be good if you can describe what that grid looks like visually for ease of understanding. — alias
that is intentional, but other values of init do the same. state of the game can be expressed as a one-dimensional array size of 12. values of the array are 1,2,3 and 4 each one 3 times. each move rearranges values in a certain way, that can be seen in the right, up, left and bot variables. I'm new to smt, tried my best to solve this problem. maybe other strategies could be better. let me know if something is not clear. — Aleksadnre Bibilashvili

alias alias · Accepted Answer · 2021-01-04T18:55:11

SMT solvers don't do well with quantifiers usually; and for solving puzzles of this sort, it's much better to use an iterative approach. That is, generate a list of symbolic moves, and ask the solver if that set can take the game from the initial state to the final state. We iteratively deepen, i.e., we search for solutions with 1-move, 2-moves, 3-moves, etc.; until some predetermined bound.

It's a bit hard to read your rules, below is a simpler example where the state is just one integer. (In your case, you seem to have a grid of 12.) But the coding style should still apply with appropriate modifications:

from z3 import *

# The state. In your case, you seem to have 12 values. For
# simplicity, here I'll just use one integer value.
a = Int('a')

# Rules of the game. Instead of swapping things around,
# I'll simply use a few arithmetic operations to represent
# the next value the state can take
def rule1(v):
    return v+1

def rule2(v):
    return v-3

def rule3(v):
    return v*2

# Allocate vars for moves. Allow for 100 moves at most.

moves = [Int('mv_' + str(cnt)) for cnt in range(100)]

# A move picks an arbitrary rule, and applies it
# to the state. We take a cnt argument, counting the moves.
def move(cnt):
    global a
    mv = moves[cnt]
    s.add(mv >= 1)
    s.add(mv <= 3)
    a = If(mv == 1, rule1(a),
        If(mv == 2, rule2(a),
                    rule3(a)));

s = Solver()

# Record the beginning state
s.add(a == 0)

cnt = 0
# To solve, we simply iterate and see if we reach the final state.
def solvePuzzle():
    global cnt
    global a
    if cnt == 100:
       print("Count reached 100, no solution found.")
    else:
       move(cnt)
       cnt = cnt+1
       # Check if the state implies the end condition
       # that a is 73. (Arbitrarily chosen for example.)
       s.push()
       s.add(a == 73)
       if s.check() == sat:
           # solved, print the moves:
           print("Solution found in step: %d" % cnt)
           m = s.model()
           for i in range(cnt):
               d = m[moves[i]].as_long()
               print("%3d. %s" % (i+1, ("rule 1", "rule 2", "rule 3")[d - 1]))
       else:
           print("No solutions with %d moves" % cnt)
           s.pop()
           solvePuzzle()

solvePuzzle()

I added inline comments, hopefully they should be easy to read. In this "game," we have 3-rules in each step. Increment by 1 (rule1), subtract 3 (rule2), double (rule3). We put an upper bound of 100 moves. Note the use of push and pop to make sure the end condition is checked at each call separately.

When I run this, I get:

No solutions with 1 moves
No solutions with 2 moves
No solutions with 3 moves
No solutions with 4 moves
No solutions with 5 moves
No solutions with 6 moves
No solutions with 7 moves
No solutions with 8 moves
Solution found in step: 9
  1. rule 1
  2. rule 3
  3. rule 3
  4. rule 3
  5. rule 1
  6. rule 3
  7. rule 3
  8. rule 3
  9. rule 1

Which says 0 (the starting state), can be turned to 73 (final state), in 9 moves, via the sequence 1-2-4-8-9-18-36-72-73.

Note that, by construction, this coding style finds the minimum possible number of moves.

Hope this gets you started!

python z3 smt Bounded model

2 Answers