examples/shikaku.mod
changeset 2 4c8956a7bdf4
equal deleted inserted replaced
-1:000000000000 0:246f2997151d
       
     1 /* A solver for the Japanese number-puzzle Shikaku
       
     2  * http://en.wikipedia.org/wiki/Shikaku
       
     3  *
       
     4  * Sebastian Nowozin <nowozin@gmail.com>, 27th January 2009
       
     5  */
       
     6 
       
     7 param ndim := 10;
       
     8 set rows := 1..ndim;
       
     9 set rows1 := 1..(ndim+1);
       
    10 set cols := 1..ndim;
       
    11 set cols1 := 1..(ndim+1);
       
    12 param givens{rows, cols}, integer, >= 0, default 0;
       
    13 
       
    14 /* Set of vertices as (row,col) coordinates */
       
    15 set V := { (i,j) in { rows, cols }: givens[i,j] != 0 };
       
    16 
       
    17 /* Set of all feasible boxes of the right size: only this boxes are possible.
       
    18  * The box contains (i,j) and ranges from (k,l) to (m,n)
       
    19  */
       
    20 set B := { (i,j,k,l,m,n) in { V, rows, cols, rows1, cols1 }:
       
    21     i >= k and i < m and j >= l and j < n and   /* Contains (i,j) */
       
    22     ((m-k)*(n-l)) = givens[i,j] and /* Right size */
       
    23     card({ (s,t) in V: s >= k and s < m and t >= l and t < n }) = 1
       
    24         /* Contains only (i,j), no other number */
       
    25 };
       
    26 
       
    27 var x{B}, binary;
       
    28 
       
    29 /* Cover each square exactly once */
       
    30 s.t. cover_once{ (s,t) in { rows, cols } }:
       
    31     sum{(i,j,k,l,m,n) in B: s >= k and s < m and t >= l and t < n}
       
    32         x[i,j,k,l,m,n] = 1;
       
    33 
       
    34 minimize cost: 0;
       
    35 
       
    36 solve;
       
    37 
       
    38 /* Output solution graphically */
       
    39 printf "\nSolution:\n";
       
    40 for { row in rows1 } {
       
    41     for { col in cols1 } {
       
    42         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    43                 col >= l and col <= n and (row = k or row = m) and
       
    44                 x[i,j,k,l,m,n] = 1}) > 0 and
       
    45             card({(i,j,k,l,m,n) in B:
       
    46                 row >= k and row <= m and (col = l or col = n) and
       
    47                 x[i,j,k,l,m,n] = 1}) > 0} "+";
       
    48         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    49                 col >= l and col <= n and (row = k or row = m) and
       
    50                 x[i,j,k,l,m,n] = 1}) = 0 and
       
    51             card({(i,j,k,l,m,n) in B:
       
    52                 row >= k and row <= m and (col = l or col = n) and
       
    53                 x[i,j,k,l,m,n] = 1}) > 0} "|";
       
    54         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    55                 row >= k and row <= m and (col = l or col = n) and
       
    56                 x[i,j,k,l,m,n] = 1}) = 0 and
       
    57             card({(i,j,k,l,m,n) in B:
       
    58                 col >= l and col <= n and (row = k or row = m) and
       
    59                 x[i,j,k,l,m,n] = 1}) > 0} "-";
       
    60         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    61                 row >= k and row <= m and (col = l or col = n) and
       
    62                 x[i,j,k,l,m,n] = 1}) = 0 and
       
    63             card({(i,j,k,l,m,n) in B:
       
    64                 col >= l and col <= n and (row = k or row = m) and
       
    65                 x[i,j,k,l,m,n] = 1}) = 0} " ";
       
    66 
       
    67         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    68             col >= l and col < n and (row = k or row = m) and
       
    69             x[i,j,k,l,m,n] = 1}) > 0} "---";
       
    70         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    71             col >= l and col < n and (row = k or row = m) and
       
    72             x[i,j,k,l,m,n] = 1}) = 0} "   ";
       
    73     }
       
    74     printf "\n";
       
    75 
       
    76     for { (col,p) in { cols, 1 }: card({ s in rows: s = row }) = 1 } {
       
    77         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    78             row >= k and row < m and (col = l or col = n) and
       
    79             x[i,j,k,l,m,n] = 1}) > 0} "|";
       
    80         printf{0..0: card({(i,j,k,l,m,n) in B:
       
    81             row >= k and row < m and (col = l or col = n) and
       
    82             x[i,j,k,l,m,n] = 1}) = 0} " ";
       
    83         printf{0..0: card({ (i,j) in V: i = row and j = col}) > 0} " %2d", givens[row,col];
       
    84         printf{0..0: card({ (i,j) in V: i = row and j = col}) = 0} "  .";
       
    85     }
       
    86     printf{0..0: card({ r in rows: r = row }) = 1} "|\n";
       
    87 }
       
    88 
       
    89 data;
       
    90 
       
    91 /* This Shikaku is from
       
    92  * http://www.emn.fr/x-info/sdemasse/gccat/KShikaku.html#uid5449
       
    93  */
       
    94 param givens : 1 2 3 4 5 6 7 8 9 10 :=
       
    95            1   9 . . . 12 . . 5 . .
       
    96            2   . . . . . . . . . .
       
    97            3   . . . . . . . . . 6
       
    98            4   8 . 6 . 8 . . . . .
       
    99            5   . . . . . . . . . .
       
   100            6   . . . . . . . . . .
       
   101            7   . . . . . 6 . 8 . 12
       
   102            8   4 . . . . . . . . .
       
   103            9   . . . . . . . . . .
       
   104           10   . . 3 . . 9 . . . 4
       
   105            ;
       
   106 
       
   107 end;