『不等号ナンプレ』(しんや+ドロップ)の表紙の問題をAlloyで解く

InequationalNumberPlace.als

abstract sig Number {
  data: Number -> one Number,
  lt : set Number
}
one sig N1, N2, N3, N4, N5 extends Number {}

fact {
  lt = ^(N1->N2 + N2->N3 + N3->N4 + N4->N5)
}

pred complete(rows, cols: set Number) {
  Number in data[rows, cols]
}

fact {
  all row: Number | complete[row, Number]
  all col: Number | complete[Number, col]
}

pred isLT(a, b : one Number) {
  a->b in lt
}

pred isGT(a, b : one Number) {
  b->a in lt
}

/*
『不等号ナンプレ』(しんや+ドロップ)の表紙の問題
http://www.amazon.co.jp/dp/4537208465

 > <5> <
v ^ v ^ ^
 < > <3< 
^ ^ v ^ v
 < > < > 
v v ^ ^ v
 <3< < > 
^ v v v ^
 > < >2< 
*/
pred problem {
  N1->N3->N5 +
  N2->N4->N3 +
  N4->N2->N3 +
  N5->N4->N2    
  in data

  -- 1行目の不等号
  isGT[data[N1,N1], data[N1,N2]]
  isLT[data[N1,N2], data[N1,N3]]
  isGT[data[N1,N3], data[N1,N4]]
  isLT[data[N1,N4], data[N1,N5]]

  -- 2行目の不等号
  isLT[data[N2,N1], data[N2,N2]]
  isGT[data[N2,N2], data[N2,N3]]
  isLT[data[N2,N3], data[N2,N4]]
  isLT[data[N2,N4], data[N2,N5]]

  -- 3行目の不等号
  isLT[data[N3,N1], data[N3,N2]]
  isGT[data[N3,N2], data[N3,N3]]
  isLT[data[N3,N3], data[N3,N4]]
  isGT[data[N3,N4], data[N3,N5]]

  -- 4行目の不等号
  isLT[data[N4,N1], data[N4,N2]]
  isLT[data[N4,N2], data[N4,N3]]
  isLT[data[N4,N3], data[N4,N4]]
  isGT[data[N4,N4], data[N4,N5]]

  -- 5行目の不等号
  isGT[data[N5,N1], data[N5,N2]]
  isLT[data[N5,N2], data[N5,N3]]
  isGT[data[N5,N3], data[N5,N4]]
  isLT[data[N5,N4], data[N5,N5]]

  -- 1列目の不等号
  isGT[data[N1,N1], data[N2,N1]]
  isLT[data[N2,N1], data[N3,N1]]
  isGT[data[N3,N1], data[N4,N1]]
  isLT[data[N4,N1], data[N5,N1]]

  -- 2列目の不等号
  isLT[data[N1,N2], data[N2,N2]]
  isLT[data[N2,N2], data[N3,N2]]
  isGT[data[N3,N2], data[N4,N2]]
  isGT[data[N4,N2], data[N5,N2]]

  -- 3列目の不等号
  isGT[data[N1,N3], data[N2,N3]]
  isGT[data[N2,N3], data[N3,N3]]
  isLT[data[N3,N3], data[N4,N3]]
  isGT[data[N4,N3], data[N5,N3]]

  -- 4列目の不等号
  isLT[data[N1,N4], data[N2,N4]]
  isLT[data[N2,N4], data[N3,N4]]
  isLT[data[N3,N4], data[N4,N4]]
  isGT[data[N4,N4], data[N5,N4]]

  -- 5列目の不等号
  isLT[data[N1,N5], data[N2,N5]]
  isGT[data[N2,N5], data[N3,N5]]
  isGT[data[N3,N5], data[N4,N5]]
  isLT[data[N4,N5], data[N5,N5]]
}

run problem
/*
solution:
4>2<5>1<3
v ^ v ^ ^
1<4>2<3<5
^ ^ v ^ v
3<5>1<4>2
v v ^ ^ v
2<3<4<5>1
^ v v v ^
5>1<3>2<4
*/