python z3 smt 有界模型

Question

我开发了一款益智游戏。游戏的状态可以表示为一个大小为 12 的 Int 数组。玩家只能进行 4 次移动。游戏的目的是达到某种状态。我正在尝试用 python z3 解决这个难题。这是代码。

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 是最大移动次数。 b 是解决问题的最小移动次数。 f 是状态数组。目标是最终获胜者状态。

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) 表示连接 k+1 和 k 状态的第 k 个移动。使用 s.add(ForAll([b], move(b)))，我希望所有整数 k k>=0 k

任何建议将不胜感激。

Answer 1

SMT 求解器通常不能很好地处理量词；为了解决这类难题，使用迭代方法要好得多。也就是说，生成一个符号移动列表，并询问求解器该集合是否可以将游戏从初始状态带到最终状态。我们迭代地加深，即我们用 1-move、2-move、3-move 等搜索解决方案；直到某个预定的界限。

阅读您的规则有点困难，下面是一个更简单的示例，其中状态只是一个整数。 （在您的情况下，您似乎有 12 个网格。）但编码风格仍应适用，并进行适当的修改：

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()

我添加了内联 cmets，希望它们应该易于阅读。在这个“游戏”中，我们每一步都有 3 条规则。加 1 (rule1)，减 3 (rule2)，加倍 (rule3)。我们设置了 100 步的上限。请注意使用push 和pop 以确保在每次调用时分别检查结束条件。

当我运行它时，我得到：

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

上面写着0（起始状态），可以通过1-2-4-8-9-18-36-72-73.序列在9步内转换为73（最终状态）

请注意，通过构造，这种编码风格会找到尽可能少的移动次数。

希望这能让你开始！

Answer 2

感谢别名代码示例，我已经解决了这个问题。代码：

from z3 import *

# The state. In your case, you seem to have 12 values. For
# simplicity, here I'll just use one integer value.
states = [[Int('a_' + str(k) + '_' + str(n)) for n in range(12)] for k in range(101)]
max_moves = 100
moves = [Int('mv_' + str(cnt)) for cnt in range(1, 101)]


s = Solver()
def init_state(args):
    s.add(And(states[0][0] == args[0], states[0][1] == args[1], states[0][2] == args[2],
        states[0][3] == args[3], states[0][4] == args[4], states[0][5] == args[5],
        states[0][6] == args[6], states[0][7] == args[7], states[0][8] == args[8],
        states[0][9] == args[9], states[0][10] == args[10], states[0][11] == args[11]))
init_state_indexes = []
print('welcome to bibilcubic solver program!')
print('Enter init state colors "red" as "0", "green" as "1", "yellow" as "" or "blue" as "4" ')



for i in range(12):
    a = input(f"Enter {i} color state: ").lower()
    while a != '0' and a != '1' and a != '2' and a != '3':
        a = input(f"illegal input please, enter again {i} color state: ")

        init_state_indexes.append(int(a))

init_state(init_state_indexes)





def left(move_number):
    global states
    global moves

    #0->2->3->4->10->11->0
    bool = And(moves[move_number - 1] == 0,
        states[move_number][0] == states[move_number-1][11], states[move_number][1] == states[move_number-1][1], states[move_number][2] == states[move_number-1][0],
        states[move_number][3] == states[move_number-1][2], states[move_number][4] == states[move_number-1][3], states[move_number][5] == states[move_number-1][5],
        states[move_number][6] == states[move_number-1][6], states[move_number][7] == states[move_number-1][7], states[move_number][8] == states[move_number-1][8],
        states[move_number][9] == states[move_number-1][9], states[move_number][10] == states[move_number-1][4], states[move_number][11] == states[move_number-1][10])

    return bool

def up(move_number):
    global states
    global moves


    #1->2->3->5->6->7->1
    bool = And(moves[move_number - 1] == 1,
        states[move_number][0] == states[move_number-1][0], states[move_number][1] == states[move_number-1][7], states[move_number][2] == states[move_number-1][1],
        states[move_number][3] == states[move_number-1][2], states[move_number][4] == states[move_number-1][4], states[move_number][5] == states[move_number-1][3],
        states[move_number][6] == states[move_number-1][5], states[move_number][7] == states[move_number-1][6], states[move_number][8] == states[move_number-1][8],
        states[move_number][9] == states[move_number-1][9], states[move_number][10] == states[move_number-1][10], states[move_number][11] == states[move_number-1][11])

    return bool

def right(move_number):
    global states
    global moves

    #4->5->6->8->9->10->4
    bool = And(moves[move_number - 1] == 2,
        states[move_number][0] == states[move_number-1][0], states[move_number][1] == states[move_number-1][1], states[move_number][2] == states[move_number-1][2],
        states[move_number][3] == states[move_number-1][3], states[move_number][4] == states[move_number-1][10], states[move_number][5] == states[move_number-1][4],
        states[move_number][6] == states[move_number-1][5], states[move_number][7] == states[move_number-1][7], states[move_number][8] == states[move_number-1][6],
        states[move_number][9] == states[move_number-1][8], states[move_number][10] == states[move_number-1][9], states[move_number][11] == states[move_number-1][11])

    return bool

def bot(move_number):
    global states
    global moves

    #0->1->7->8->9->11->0
    bool = And(moves[move_number - 1] == 3,
        states[move_number][0] == states[move_number-1][11], states[move_number][1] == states[move_number-1][0], states[move_number][2] == states[move_number-1][2],
        states[move_number][3] == states[move_number-1][3], states[move_number][4] == states[move_number-1][4], states[move_number][5] == states[move_number-1][5],
        states[move_number][6] == states[move_number-1][6], states[move_number][7] == states[move_number-1][1], states[move_number][8] == states[move_number-1][7],
        states[move_number][9] == states[move_number-1][8], states[move_number][10] == states[move_number-1][10], states[move_number][11] == states[move_number-1][9])

    return bool


def move(move_number):

    global s

    return Or(left(move_number), up(move_number),
            right(move_number), bot(move_number))

cnt = 1
            # To solve, we simply iterate and see if we reach the final state.
def solvePuzzle():

    global cnt
    global current_state

    if cnt == 100:
        print("Count reached 500, no solution found.")
    else:

        # Check if the state implies the end condition
        a = move(cnt)
        s.add(a)
        s.push()
        s.add(And(states[cnt][0] == 0, states[cnt][1] == 0, states[cnt][2] == 0,
            states[cnt][3] == 1, states[cnt][4] == 1, states[cnt][5] == 1,
            states[cnt][6] == 2, states[cnt][7] == 2, states[cnt][8] == 2,
            states[cnt][9] == 3, states[cnt][10] == 3, states[cnt][11] == 3))

        cnt = cnt+1
        # that a is 73. (Arbitrarily chosen for example.)

        if s.check() == sat:
            # solved, print the moves:
            print(f"Solution found in step: {cnt - 1}")
            m = s.model()
            for i in range(cnt-1):
                d = m[moves[i]].as_long()
                print(f"{i+1} move is: {('left', 'up', 'right', 'bot')[d]}")

            else:
                print(f"No solutions with {cnt - 1} moves")
                s.pop()

                solvePuzzle()

solvePuzzle()