python z3 smt 有界模型

如何解决python z3 smt 有界模型

我开发了一款益智游戏。游戏状态可以表示为一个大小为 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())

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

goal = And(f(b,f(b,4)
    == 2,12) == 4)

a 是最大移动次数。 b 是解决问题的最小移动次数。 f 是状态数组。目标是最终获胜者状态。

def move(k):

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

    UP = And(f(k + 1,12))

    BOT = And(f(k + 1,12),10))

    LEFT = And(f(k + 1,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

如有任何建议，我们将不胜感激。

解决方法

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

阅读您的规则有点困难，下面是一个更简单的示例，其中状态只是一个整数。 （在您的情况下，您似乎有 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()

我添加了内嵌注释，希望它们应该易于阅读。在这个“游戏”中，我们在每一步都有 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（起始状态），可以转为73（最终状态），9步，通过序列1-2-4-8-9-18-36-72-73.

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

希望这能帮助您入门！

,

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

from z3 import *

# The state. In your case,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][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][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][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][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][1] == states[move_number-1][0],states[move_number][7] == states[move_number-1][1],states[move_number][8] == states[move_number-1][7],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()