SMTソルバーの書き方

Question

SMTソルバーを用いたパズルの解法を導きたいのですが以下のような条件を付けた場合、どのように続ければいいかアドバイスいただきたいです。画像のようなパズルを解きたいです。

from z3 import *

行と列
N = 10

黒いマス = { (1,3): '左', (1,7): ' ', (2,5): '上', (2,9): '左', (3,1): '上', (3,3): ' ', (3,7): '下', (4,5): '上', (4,8): '左', (4,10): '上', (5,2): '上', (5,4): '', (6,7): '', (6,9): '左', (7,1): '', (7,3): '上', (7,6): '上', (8,4): '右', (8,8): '', (8,10): '上', (9,2): '右', (9,6): '左', (10,4): '左', (10,8): '' }
入力

部屋番号 = {(1,1): 1, (1,2): 1, (1,3): 0, (1,4): 2, (1,5): 2, (1,6): 2, (1,7): 0, (1,8): 3, (1,9): 4, (1,10): 4,
       (2,1): 1, (2,2): 5, (2,3): 6, (2,4): 6, (2,5): 0, (2,6): 7, (2,7): 3, (2,8): 3, (2,9): 0, (2,10): 4, (3,1): 0, (3,2): 5,
        (3,3): 0, (3,4): 8, (3,5): 6, (3,6): 6, (3,7): 0, (3,8): 8, (3,9): 8, (3,10): 8, (4,1): 5, (4,2): 5, (4,3): 8, (4,4): 8,
         (4,5): 0, (4,6): 9, (4,7): 9, (4,8): 0, (4,9): 10, (4,10): 0, (5,1): 11, (5,2): 0, (5,3): 12, (5,4): 0, (5,5): 13, (5,6): 13,
          (5,7): 9, (5,8): 9, (5,9): 10, (5,10): 14, (6,1): 11, (6,2): 12, (6,3): 12, (6,4): 15, (6,5): 13, (6,6): 13, (6,7): 0, (6,8): 16,
           (6,9): 0, (6,10): 14, (7,1): 0, (7,2): 17, (7,3): 0, (7,4): 15, (7,5): 15, (7,6): 0, (7,7): 16, (7,8): 16, (7,9): 18, (7,10): 18,
            (8,1): 17, (8,2): 17, (8,3): 17, (8,4): 0, (8,5): 15, (8,6): 19, (8,7): 19, (8,8): 0, (8,9): 18, (8,10): 0, (9,1): 20, (9,2): 0,
             (9,3): 21, (9,4): 22, (9,5): 22, (9,6): 0, (9,7): 23, (9,8): 23, (9,9): 24, (9,10): 25, (10,1): 21, (10,2): 21, (10,3): 21,
              (10,4): 0, (10,5): 22, (10,6): 26, (10,7): 26, (10,8): 0, (10,9): 24, (10,10): 24 }

マスの数字 = { [i,j]: Int('数字[{}{}]'.format(i,j)) for i in range(1,N) for j in range(1,N) }


一より大きい = [ And(1 <= マスの数字[i,j],マスの数字[i,j]<= 4 ) for i in range(1,N) for j in range(1,N) ]   
              各 (i,j) について，マスの数字[i,j] は1以上であることを述べる

数字の条件 =[ マスの数字[i,j] <= list(部屋番号.values()).count(部屋番号[i,j]) for i in range(1,N) for j in range(1,N)]   
 (i,j)が属する部屋に属するマスの数は，list(部屋番号.values()).count(部屋番号[i,j])
 各 (i,j) について，マスの数字[i,j] は，(i,j)が属する部屋に属するマスの数以下である 


同じ部屋に属するマスの数字はすべて異なる = [ Distinct([部屋番号[i,j] for (i,j) in range(1,N) for j in range(1,N)if 部屋番号[i,j] == n]) for n in 部屋番号.values()]

 同じ部屋に属するマスの数字はすべて異なることをを述べる
部屋番号が n であるマスのリストは，辞書 部屋番号 から，値が n であるキーをすべて取り出して作ればよい．
[(i,j) for i in range(1,N) for j in range(1,N) if 部屋番号[i,j] == n] Distinct([部屋番号[i,j] for (i,j) in ... ]() のような書き方ができる．

        
def 隣接したマス(x,y):
    if x > 1:
        yield (x-1,y)
    if x <N :
        yield (x+1,y)
    if y > 1:
        yield (x,y-1)
    if y <N:
        yield (x,y+1)

左 = [ And([マスの数字 [x-1,y] >マスの数字[i,j] for (i,j) in 隣接したマス (x,y) if (i,j) != (x-1,y) ]) for (x,y) in 黒いマス if 黒いマス[x,y] == '左' ]

右 = [ And([マスの数字 [x+1,y] >マスの数字[i,j] for (i,j) in 隣接したマス (x,y) if (i,j) != (x+1,y) ]) for (x,y) in 黒いマス if 黒いマス[x,y] == '右' ]
 
上 = [ And([マスの数字 [x,y+1] >マスの数字[i,j] for (i,j) in 隣接したマス (x,y) if (i,j) != (x,y+1) ]) for (x,y) in 黒いマス if 黒いマス[x,y] == '上' ]

下 = [ And([マスの数字 [x,y-1] >マスの数字[i,j] for (i,j) in 隣接したマス (x,y) if (i,j) != (x,y-1) ]) for (x,y) in 黒いマス if 黒いマス[x,y] == '右' ]

    

c = 左 + 右 + 上 + 下 + マスの数字 + 一より大きい + 数字の条件 + 同じ部屋に属するマスの数字はすべて異なる

s = Solver()

Comments

[y_waiwai]

このままではコードが読めないので、質問を編集し、</>(コードの挿入)ボタンを押し、出てくる’’’の枠の中にコードを貼り付けてください

[mazitani]

修正しました。よろしくお願いします

Answer 1

とりあえず、現状誤っている点を並べておきます。

1. 行と列などの説明は、先頭に#を入れてコメントにすべき
2. N=10でrange(1,N)だと1から9までしか生成されない。今回は10まで必要なのでrange(1,N+1)にすべき
3. 部屋番号が間違っている。番号6や8が複数の部屋に振られている
4. マスの数字について、辞書のキーにリスト[i,j]は使えないので、タプル(i,j)にすべき
5. 黒いマスにまでマスの数字を割り振っている
6. 同じ部屋に属するマスの数字はすべて異なるについて、Distinctには変数を渡すべきなので、中身は部屋番号[i,j]ではなくマスの数字[i,j]
7. 同じ部屋に属するマスの数字はすべて異なるについて、for (i,j) in range(1,N)ではなくfor i in range(1,N+1)
8. 黒いマスなどのキーは(y,x)の順番なのに、左などの制約がすべて(x,y)の順番である前提で書かれている
9. 下の制約の条件がif 黒いマス[x,y] == '右'
10. cにマスの数字を足しこんでいるが、他がすべてリストなのにこれだけ辞書なのでエラーになる