Alloy Analyzer 30行でスリザーリンクの問題を解く

形式手法のツールAlloyでスリザーリンクの問題を30行で解いてみた。

スリザーリンクのルールは下記の通り。

1. 数字は周囲の線の本数を示す。
2. 線は交差や枝分かれしない。
3. 線は全体で一つの輪になる。

詳しい解説 http://www.nikoli.com/ja/puzzles/slitherlink/rule.html

短く書くポイントは、ルール2と3を次のように解釈すること。

• 要は線というのは内側エリアと外側エリアに分ける境界線。
• 内側マスは全部つながっている。
• 外側マスは辺の外側マスにつながっている。

こうすると、線の枝分かれとかループとかの判定は、特に必要ない。

alloy

abstract sig Board {
  maxadjs: Int
}

abstract sig Side {}
one sig Inside, Outside extends Side {}

abstract sig Cell {
  adjacent: some Cell,
  num: Int,
  side: one Side
}

fact { adjacent = ~adjacent }
fact { all c: Cell | c not in c.adjacent }

fun ourside: Cell -> Cell {
  {c0, c1: Cell | c1.side = c0.side and c1 in c0.adjacent}
}

fun adj_inside: Cell -> Cell {
  {c0, c1: Cell | c1.side = Inside and c1 in c0.adjacent}
}

fact { all c: Cell | c.side = Inside => c.num = sub[Board.maxadjs, #c.adj_inside] }
fact { all c: Cell | c.side = Outside => c.num = #c.adj_inside }

fact { all c0, c1: Cell | (c0 + c1).side = Inside => c1 in c0.*ourside }
fact { all c0: Cell | c0.side = Outside =>
  some c1: Cell | c1 in c0.*ourside and #(c1.adjacent) < Board.maxadjs }


// Example
// _ _ 3 _ _
// _ 3 _ 2 2
// 2 2 _ _ 2
// 3 _ 3 _ _
// _ _ _ 1 _

one sig SquareBoard extends Board {} { maxadjs = 4 }
one sig C_0_0 extends Cell {}
one sig C_0_1 extends Cell {}
one sig C_0_2 extends Cell {} { num = 3 }
one sig C_0_3 extends Cell {}
one sig C_0_4 extends Cell {}
one sig C_1_0 extends Cell {}
one sig C_1_1 extends Cell {} { num = 3 }
one sig C_1_2 extends Cell {}
one sig C_1_3 extends Cell {} { num = 2 }
one sig C_1_4 extends Cell {} { num = 2 }
one sig C_2_0 extends Cell {} { num = 2 }
one sig C_2_1 extends Cell {} { num = 2 }
one sig C_2_2 extends Cell {}
one sig C_2_3 extends Cell {}
one sig C_2_4 extends Cell {} { num = 2 }
one sig C_3_0 extends Cell {} { num = 3 }
one sig C_3_1 extends Cell {}
one sig C_3_2 extends Cell {} { num = 3 }
one sig C_3_3 extends Cell {}
one sig C_3_4 extends Cell {}
one sig C_4_0 extends Cell {}
one sig C_4_1 extends Cell {}
one sig C_4_2 extends Cell {}
one sig C_4_3 extends Cell {} { num = 1 }
one sig C_4_4 extends Cell {}

fact { C_0_0.adjacent = C_0_1 + C_1_0 }
fact { C_1_0.adjacent = C_1_1 + C_0_0 + C_2_0 }
fact { C_2_0.adjacent = C_2_1 + C_1_0 + C_3_0 }
fact { C_3_0.adjacent = C_3_1 + C_2_0 + C_4_0 }
fact { C_4_0.adjacent = C_4_1 + C_3_0 }
fact { C_0_1.adjacent = C_0_0 + C_0_2 + C_1_1 }
fact { C_1_1.adjacent = C_1_0 + C_1_2 + C_0_1 + C_2_1 }
fact { C_2_1.adjacent = C_2_0 + C_2_2 + C_1_1 + C_3_1 }
fact { C_3_1.adjacent = C_3_0 + C_3_2 + C_2_1 + C_4_1 }
fact { C_4_1.adjacent = C_4_0 + C_4_2 + C_3_1 }
fact { C_0_2.adjacent = C_0_1 + C_0_3 + C_1_2 }
fact { C_1_2.adjacent = C_1_1 + C_1_3 + C_0_2 + C_2_2 }
fact { C_2_2.adjacent = C_2_1 + C_2_3 + C_1_2 + C_3_2 }
fact { C_3_2.adjacent = C_3_1 + C_3_3 + C_2_2 + C_4_2 }
fact { C_4_2.adjacent = C_4_1 + C_4_3 + C_3_2 }
fact { C_0_3.adjacent = C_0_2 + C_0_4 + C_1_3 }
fact { C_1_3.adjacent = C_1_2 + C_1_4 + C_0_3 + C_2_3 }
fact { C_2_3.adjacent = C_2_2 + C_2_4 + C_1_3 + C_3_3 }
fact { C_3_3.adjacent = C_3_2 + C_3_4 + C_2_3 + C_4_3 }
fact { C_4_3.adjacent = C_4_2 + C_4_4 + C_3_3 }
fact { C_0_4.adjacent = C_0_3 + C_1_4 }
fact { C_1_4.adjacent = C_1_3 + C_0_4 + C_2_4 }
fact { C_2_4.adjacent = C_2_3 + C_1_4 + C_3_4 }
fact { C_3_4.adjacent = C_3_3 + C_2_4 + C_4_4 }
fact { C_4_4.adjacent = C_4_3 + C_3_4 }

run {} for 3

//Executing "Run run$1 for 3"
//   Solver=sat4j Bitwidth=4 MaxSeq=3 SkolemDepth=1 Symmetry=20
//   103562 vars. 1091 primary vars. 220440 clauses. 967ms.
//   Instance found. Predicate is consistent. 2199ms.

// Instance
// O O O X O 
// O X X X O 
// O O X O O 
// X O X O X 
// O O O O O 

Instanceの中のOは内側マス、Xは外側マスなので、その境界線がこの問題の解となる。

つながっている判定のところで、反射推移閉包を使っているせいかどうかは分からないが、あまり計算効率は良くない模様。