Alloy Analyzer 30行でスリザーリンクの問題を解く ref: http://qiita.com/t2ru/items/c9a88b6f724fd4a75e99

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