Alloyでイラストロジックを解く - 西尾泰和のはてなダイアリー

ラボで昼休みにAlloyの話をしていたら中谷さん(id:n_shuyo)に「Alloyでイラストロジックは解けるの？」と質問されました。で、頑張ってみた結果、結局解けなかった、という話。

イラストロジックのルールと元データに関してはこちらを参照: ルールと解き方〜イラストロジック〜

1次元イラストロジック

まず問題は簡単な方から解こうということで、1次元のイラストロジック「10個のマスがあって、ヒントは[7]」を解かせてみる。

open util/ordering[Cell]

sig Cell {
	color: Color
}

enum Color {Black, White}

pred all_color(start, end : Cell, col: Color){
	all c: (start + start.nexts) & (end.prevs + end){
		c.color = col
	}
}

fact {
	some b : Cell { // block head
		let b7 = b.next.next.next.next.next.next {
			one b7
			all_color[first, b.prev, White]
			all_color[b, b7, Black]
			all_color[b7.next, last, White]
		}
	}
}
run {} for 3 but exactly 10 Cell

実行してみると、正しく4通りの解があることがわかる。「10個の全順序が導入されたCellの中にあるbが存在して「bの6回nextをたどったcellが存在し、bの手前までのcellが白で、bからb7までが黒、b7の次以降が白」が満たされている」という条件で探索したわけだ。

より難しい問題に挑戦する前に挙動が変わらないか観察しながらリファクタリング。

open util/ordering[Cell]

sig Cell {
	color: Color
}

enum Color {Black, White}

pred all_black(start, end : Cell, size: Int){
	let block = (start + start.nexts) & (end.prevs + end){
		#block = size
		all c: block{
			c.color = Black
		}
	}
}

pred all_white(start, end : Cell){
	let block = (start + start.nexts) & (end.prevs + end){
		all c: block{
			c.color = White
		}
	}
}

fact {
	some c: Cell {
		all_white[first, c.prev]
		some c2: Cell {
			all_black[c, c2, 7]
			all_white[c2.next, last]
		}
	}
}
run {} for 3 but exactly 10 Cell

nextを連打する代わりに集合のサイズで判定するようにした。

1次元イラストロジック、ヒントのブロックが複数

次はヒントが[6, 3]みたいなケースを考えてみよう。少し考えて、黒の塊ごとにsomeが2つ必要だと判断。

fact {
	some c: Cell {
		all_white[first, c.prev]
		some c2: c.nexts {
			all_black[c, c2, 6]
			some c3: c2.next.nexts {
				all_white[c2.next, c3.prev]
				some c4: c3.nexts{
					all_black[c3, c4, 3]
					all_white[c4.next, last]
				}
			}
		}
	}
}

あるセルcが存在して、最初のセルからcの手前までは白、cより後にあるセルc.nextsの中にc2があって、cからc2までは長さ6で全部黒、c2.nextは白なのでc2.nextより後にあるc3があって、c3の手前までは白、c3より後にc4があって、c3からc4までは長さ3で全部黒、c4より後は最後まで全部白、と書いてある。

実行してみると解が正しく1個だけ見つかる。これで1次元のイラストロジックは解けるようになった。

10x10の2次元イラストロジックに挑戦

イラストロジックを解くためには、このコードをヒントの個数だけ生成する必要がある。あと、1次元でないということは単純な全順序ではない。それぞれのセルが「縦方向の次」と「横方向の次」を持ってる。というわけでutil/orderingを使うのを諦めた。まずは正方形に並んだ100個のCellを表現するためのコードを生成。約300行。

abstract sig Cell {
  color: Color,
  hnext: lone Cell,
  vnext: lone Cell
}

(snip)

one sig Cell_0_0 extends Cell {}
one sig Cell_0_1 extends Cell {}
one sig Cell_0_2 extends Cell {}
(snip)
one sig Cell_9_7 extends Cell {}
one sig Cell_9_8 extends Cell {}
one sig Cell_9_9 extends Cell {}

fact matrix_adj {
  Cell_0_0.vnext = Cell_0_1
  Cell_0_1.vnext = Cell_0_2
  Cell_0_2.vnext = Cell_0_3
(snip)
  Cell_6_9.hnext = Cell_7_9
  Cell_7_9.hnext = Cell_8_9
  Cell_8_9.hnext = Cell_9_9
  no Cell_9_9.hnext
}

こんな感じで100個の名前がついたCellと、その間の隣接関係を定義して、10x10のマトリクスを無理やり生成しました。

パズルのヒントも生成。約200行:

fact {
  let next = hnext {
    some c1: from[Cell_0_0, next] {
      all_white[range[from[Cell_0_0, next], c1.~next, next]]
      some c2: c1.^next {
        all_black[range[c1, c2, next], 3]
        all_white[c2.^next]
      }
    }
    some c1: from[Cell_0_1, next] {
      all_white[range[from[Cell_0_1, next], c1.~next, next]]
      some c2: c1.^next {
        all_black[range[c1, c2, next], 2]
        some c1: c2.next.^next {
          all_white[range[c2.next.^next, c1.~next, next]]
          some c2: c1.^next {
            all_black[range[c1, c2, next], 2]
            all_white[c2.^next]
          }
        }
      }
    }
(以下略)

まあ、こんな一部省略したコードではわからないかと思うので
こちらに生成したAlloyのコード: https://github.com/nishio/learning_alloy/blob/master/illustlogic.als
こちらに生成するために書いたPythonのコード: https://github.com/nishio/learning_alloy/blob/master/tool/illulogic.py
を置くなどした。

結果はまだ出ていない。SATソルバに食わせるためのCNFの生成に時間が掛かっている。明日の朝起きて結果が出てたら追記する。

追記

約1時間で

Executing "Run run$1 for 5 int"
   Solver=minisatprover(jni) Bitwidth=5 MaxSeq=4 SkolemDepth=1 Symmetry=20
   Generating CNF...

An error has occurred!

異常終了していたｗ

追記

JNIでMiniSatを呼び出すのを辞めてSAT4Jにしてみた。メモリ割り当ては最大限まで引き上げた。

Executing "Run run$1 for 5 int"
   Solver=sat4j Bitwidth=5 MaxSeq=4 SkolemDepth=1 Symmetry=20
   Generating CNF...

Fatal Error: the solver ran out of memory!
Try simplifying your model or reducing the scope,
or increase memory under the Options menu.

An error has occurred!

それでも駄目か…

何か他にいじるべき設定があるのかな。それとも現状のsomeが6重ネストしているようなコードがダメなのかな。1ブロックごとにsomeを2個使ってブロックのサイズと数値を比較するんじゃなくて.next.next.nextみたいな書き方のコードを出力してsomeを半分に減らすとなんとかなるかな？？