Alloyガール番外編「イラストロジック」
ここまでの話はこちら: Alloy
ある日
JS: ねえねえ、Alloyでイラストロジックって解けるの？
僕: え、えーと、どうやって書けばできるかはすぐには答えられないけど、SATの性能的には当然解けると思うよ！
JS: ふーん、そうなんだー
その日の夜
僕: むむむ、そもそも2次元にセルが並んでいるとかどうやって表現するんだ。
…
僕: PythonでAlloyのコードを出力するプログラムを作った！！500行ｗｗｗ
…
僕: 実行しても結果が返ってこない。あっ、メモリ不足で死んだ…。
次の日
僕: というわけでAlloyはイラストロジックに向いていない！(キリッ *1
Alloy: そんなわけないじゃない。あなたの書き方が悪いんでしょ、ほらこれでも読んで勉強しなさい！ イラストロジックをAlloyで解く - たけをの日記＠天竺から帰ってきたよ
僕: ぐはっ、精進させて頂きます。
セルが2次元に並んでいる
僕: なるほど「セルが2次元に並んでいる」をこう表現するのか…
open util/ordering[Col] as cols
open util/ordering[Row] as rows
abstract sig Region {}
sig Col extends Region {
cell: Row -> Cell
}
sig Row extends Region {}
enum Cell { Black, White }
fact {
all c: Col, r: Row | one cell [c, r]
}Alloy: どこかの誰かさんはコード生成で300行くらい作ってたけど、頭をつかう前に力技に頼るのは悪い癖ね。
僕: 返す言葉もございません。cellという関係がCol -> Row -> Cellなのがコツですね。僕の力技では100個のCellを作っていたけど、これだとColが10個、Rowが10個、Cell(て言うよりColor)が2個ですむ。コンパクトだー。
Alloy: 時間とか比較してみたらいいんじゃない？ちょっと10個って指定して実行してみて。
run{
#Col = 10
#Row = 10
} for 10 but 5 int僕: bonotakeさんのエレガントな解だと20msだね。
Executing "Run run$1 for 10 but 5 int" Solver=minisat(jni) Bitwidth=5 MaxSeq=10 SkolemDepth=1 Symmetry=20 511 vars. 200 primary vars. 500 clauses. 13ms. . found. Predicate is consistent. 7ms.
Alloy: あなたのエレファントな解だと80倍くらい遅いわね。
Executing "Run run$1" Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 60363 vars. 20000 primary vars. 99382 clauses. 1514ms. . found. Predicate is consistent. 67ms.
僕: ぐぬぬ。
Alloy: bonotakeさんの解だと「200 primary vars」なのにあなたの解では「20000 primary vars」なのね。80倍遅いのも、大部分がSATに渡すためのCNFを作っているところにかかってるわね。
JS: CNFって何？
Alloy: see 乗法標準形 - Wikipedia
僕: 要するに、論理式を渡すとそれを満たす解を探してくれるツールがあって(SAT)、それに渡すためには綺麗な形の論理式(CNF)にしなきゃいけない、ってことね。Alloyさんがやってるのは人間に読みやすい形のソースコードを解釈してCNFを作り、それをSATに渡して解かせて、結果を人間にわかりやすい形で見せてくれる、っていう通訳みたいな仕事なんだよ。
JS: そうなんだー、そのシーエヌエフを見る方法ってあるの
僕: えっ、どうだろう。わかんない。
Alloy: Output CNF to Fileってオプションがあるわよ
僕: 試してみたけど読み方がわからないなぁ
p cnf 14 15 -2 -1 -4 0 4 -8 0 -1 5 0 -2 5 0 1 2 -5 0 -5 -3 -6 0 6 -8 0 3 5 -7 0 7 -8 0 -1 2 -9 0 9 -13 0 -2 3 -11 0 11 -13 0 8 0 13 0
Intの配列はIntからIntへの関係である
僕: Alloyに配列はない、と思ってたけど、そうか配列ってのはIntが定義域である関係だとみなせるのか。
0 -> 1 + 1 -> 1 + 2 -> 1
JS: んん？ 0 -> 2 -> 3 -> 1？？
僕: いや、そうじゃないよ。(->)の方が優先度が高い。
(0 -> 1) + (1 -> 1) + (2 -> 1)
JS: 矢印の足し算とかよくわからないなぁ。(0 -> 1) + (1 -> 1)ってなんなんだろー？
僕: それは「(0 -> 1)が1個だけ入った集合」と「(1 -> 1)が1個だけ入った集合」の和集合だね。
JS: なるほど☆
シーケンス
僕: seqってなんだっけ。付録Bの言語リファレンスにも書いてない。
Alloy: 付録F「Alloy4の構文的機能」に、リファレンスに載ってない付加機能が書かれているわよ。
僕: ぐぬぬ。そういえばdisjもenumもここで発見したんだった。
Alloy: どうせまた最初と最後のページだけ読んだんでしょ。付箋でも貼っときなさい。
僕: はーい。
Alloy: p.329からアトムのシーケンスについて説明されているわ。sig BookはInt -> Bookである。
僕: あっ、じゃあ配列みたいなものじゃん。うわ、subseqとかindexOfとか便利そうなものがいっぱいある！
ソート
僕: なるほど、こうやって集合をソートするのか
pred headsSeqInCol (c: Col, s: seq Row) {
// sの要素はブロック先頭の集合と同一
s.elems = headsInCol[c]
// sは単調増加
all i: s.butlast.inds | lt [s[i], s[plus[i, 1]]]
}Alloy: ソートって表現がとても手続き型脳ね。
僕: 母国語がPythonなんでそこは仕方がない！
Alloy: まあ「あるIntの集合と要素が同一で、かつ隣接する2要素に小なりが成立するシークエンス」をソートと呼びたくなる気持ちは理解できるわ。
反射推移閉包
僕: なんかアスタリスクとかいう見慣れない演算子が出てきたぞ
start.*cols/next - end.^cols/next
Alloy: 反射推移閉包演算子ね
僕: あー、それ教科書に出てきたけど意味がわからないからスルーしたんだった。
Alloy: 推移閉包が理解できてるなら難しいことじゃないわ。推移閉包^rが与えられた関係rを含む推移律*2を満たす最小の集合だったように、反射推移閉包*rは与えられた関係rを含む推移律と反射律*3を満たす最小の集合なだけよ。
僕: いや、僕の理解では推移閉包はそういうものじゃないなぁ。「a.^rはa.r + a.r.r + a.r.r.r + ...と関係rを1回以上繰り返して適用したもの」という理解。
Alloy: とっても手続き型脳ね。
僕: …。で、反射推移閉包は反射律を満たすってことは、恒等射を含むってことだから、要するに手続き型脳な僕にわかりやすいようにぶっちゃけて説明すると「a.*rはa + a.r + a.r.r + a.r.r.r + ...と関係rを0回以上繰り返して適用したもの」という理解でOK？
Alloy: その解釈でも矛盾はないわね。
僕: で、要するにこれは「start以上end以下の集合」ってことね？
start.*cols/next - end.^cols/next
Alloy: そうね。
ヒント読解
僕: つまりこういうことか
pred rowHint (j: Int, sizes: seq Int) {
let r = Int2Row[j] | some cs: seq Col {
#sizes = #cs
// csは黒ブロックの先頭の位置のソートされたシークエンス
headsSeqInRow [r, cs]
all i: sizes.inds {
// cs[i]をstart, startの位置にsize[i]を足して1を引いた位置にあるColをendと呼ぶ
let start = cs [i], end = Int2Col [plus [Col2Int [start], minus[sizes [i], 1] ]] {
// endが存在する
some end
// startからendまで全部黒
all c: start.*cols/next - end.^cols/next | cell [c, r] in Black
// endの次がないか、または白
no end.next or cell [end.next, r] in White
}
}
}
}
結果を可視化
JS: 答えでたの？見せて見せて！えいっ、ギャー
Alloy: Cellの色の情報がCol->Row->Colorの形だから読みづらいわね。XMLでエクスポートしたらいいわよ。
僕: XMLか…。
<field label="cell" ID="6" parentID="4"> <tuple> <atom label="Col$0"/> <atom label="Row$0"/> <atom label="White$0"/> </tuple> <tuple> <atom label="Col$0"/> <atom label="Row$1"/> <atom label="White$0"/> </tuple> <tuple> <atom label="Col$0"/> <atom label="Row$2"/> <atom label="White$0"/> </tuple> (以下略)
僕: …まあ適当にスクリプト書いて、っと。じゃじゃーん、できましたー！
■■■ ■■ ■■ ■ ■ ■ ■■■ ■■■ ■■■■■ ■■■■■■■ ■■■■■■■ ■■■■■■■ ■■■■■■■ ■■■■■
