「イラストロジックはAlloyに向かない」
って書いておくと id:bonotake さんが解決してくれないかな(チラッ)
ちょｗｗｗ
いやいや、そういうムチャぶりはやめてください（^^;
というか実際のところ、自信ありません(^^;;;
イラストロジックがAlloyに向くか向かないかは微妙なところがあります。数独なんかもそうですが、この手のニコリ系パズルは書き方間違えると簡単に計算が爆発しちゃうんですよ。
うーんでも、話を振られた以上は、やってみないとダメかなぁ、でも最近時間ないしなぁ…と思っていたのですが、うまい具合に今日奥様からインフルエンザをもらって仕事ができなくなり（ぇ 予定外の時間ができたのでちょっとやってみました。
なお、id:nishiohirokazuさんの記事と同様、イラストロジックの定義と例題はこちらからお借りしました。
とりあえず、僕の書いたイラストロジックのモデル（空行とか含めて約90行＋問題の定義約20行）。Gistにも貼ってます。
見てもらうとわかりますが、ほぼ同様の記述が行と列で別々に書き分けてあって、コードクローンが発生しております。なので、まとめたらもっと短く書けると思います。
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]
}
-- about rows
pred blackHeadInRow (c: Col, r: Row) {
c in first or cell[c.prev, r] in White
cell[c, r] in Black
}
fun headsInRow (r: Row): set Col {
{ c: Col | blackHeadInRow[c, r] }
}
fact noOtherHeadsInRow {
no c: Col, r: Row | c not in headsInRow[r] and blackHeadInRow[c, r]
}
pred headsSeqInRow (r: Row, s: seq Col) {
s.elems = headsInRow[r]
all i: s.butlast.inds | lt [s[i], s[plus[i, 1]]]
}
fun Int2Row (i: Int): Row {
{r: Row | #(r.prevs) = i}
}
fun Row2Int (r: Row): Int {
#(r.prevs)
}
pred rowHint (j: Int, sizes: seq Int) {
let r = Int2Row[j] | some cs: seq Col {
#sizes = #cs
headsSeqInRow [r, cs]
all i: sizes.inds |
let start = cs [i], end = Int2Col [plus [Col2Int [start], minus[sizes [i], 1] ]] {
some end
all c: start.*cols/next - end.^cols/next | cell [c, r] in Black
no end.next or cell [end.next, r] in White
}
}
}
-- about cols
pred blackHeadInCol (c: Col, r: Row) {
r in first or cell[c, r.prev] in White
cell[c, r] in Black
}
fun headsInCol (c: Col): set Row {
{ r: Row | blackHeadInCol[c, r] }
}
fact noOtherHeadsInCol {
no c: Col, r: Row | r not in headsInCol[c] and blackHeadInCol[c, r]
}
pred headsSeqInCol (c: Col, s: seq Row) {
s.elems = headsInCol[c]
all i: s.butlast.inds | lt [s[i], s[plus[i, 1]]]
}
fun Int2Col (i: Int): Col {
{c: Col | #(c.prevs) = i}
}
fun Col2Int (c: Col): Int {
#(c.prevs)
}
pred colHint (j: Int, sizes: seq Int) {
let c = Int2Col[j] | some rs: seq Row {
#sizes = #rs
headsSeqInCol [c, rs]
all i: sizes.inds |
let start = rs [i], end = Int2Row [plus [Row2Int [start], minus[sizes [i], 1] ]] {
some end
all r: start.*rows/next - end.^rows/next | cell [c, r] in Black
no end.next or cell [c, end.next] in White
}
}
}
-- riddle from http://homepage1.nifty.com/sabo10/rulelog/illust.html
solve: run {
rowHint [0, 0 -> 3]
rowHint [1, 0 -> 2 + 1 -> 2]
rowHint [2, 0 -> 1 + 1 -> 1 + 2 -> 1]
rowHint [3, 0 -> 3 + 1 -> 3]
rowHint [4, 0 -> 5]
rowHint [5, 0 -> 7]
rowHint [6, 0 -> 7]
rowHint [7, 0 -> 7]
rowHint [8, 0 -> 7]
rowHint [9, 0 -> 5]
colHint [0, 0 -> 4]
colHint [1, 0 -> 6]
colHint [2, 0 -> 7]
colHint [3, 0 -> 9]
colHint [4, 0 -> 2 + 1 -> 7]
colHint [5, 0 -> 1 + 1 -> 6]
colHint [6, 0 -> 2 + 1 -> 4]
colHint [7, 0 -> 3]
colHint [8, 0 -> 1]
colHint [9, 0 -> 2]
} for 10 but 5 Intで、動かしてみると、こんな感じ。約2.5秒。予想外に(^^; 結構さっくり解けました。
5年前のサブノートPCでこれくらいなので、最近のPCならもっと速いでしょう。
結果は元サイトのと同じになるので、動かしてみてください。見づらいですが（誰かの書いたビューワ使い回せないだろうか…みんな同じようなパズルAlloyで解いて、その度にビューワ書いてる気がする。）
あ、そうそう。最近時間なくて反応できてませんが、id:nishiohirokazuさんの最近のAlloy関連記事、面白いですよ。皆さんもぜひご一読ください。Alloyガールの続きまだかなー （・∀・ ）っ/凵⌒☆ﾁﾝﾁﾝ
cf. Alloyまとめ - 西尾泰和のはてなダイアリー
追記: モデルの中にコメントも何も書いてなかったので、そのへんぼちぼち追加しながら説明を書き足そうかな、と思っていたら、id:nishiohirokazuさんがさっさと解読・解説する記事をAlloyガールで書いてくれました。うはー。
