examples/shikaku.mod
changeset 1 c445c931472f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/examples/shikaku.mod	Mon Dec 06 13:09:21 2010 +0100
     1.3 @@ -0,0 +1,107 @@
     1.4 +/* A solver for the Japanese number-puzzle Shikaku
     1.5 + * http://en.wikipedia.org/wiki/Shikaku
     1.6 + *
     1.7 + * Sebastian Nowozin <nowozin@gmail.com>, 27th January 2009
     1.8 + */
     1.9 +
    1.10 +param ndim := 10;
    1.11 +set rows := 1..ndim;
    1.12 +set rows1 := 1..(ndim+1);
    1.13 +set cols := 1..ndim;
    1.14 +set cols1 := 1..(ndim+1);
    1.15 +param givens{rows, cols}, integer, >= 0, default 0;
    1.16 +
    1.17 +/* Set of vertices as (row,col) coordinates */
    1.18 +set V := { (i,j) in { rows, cols }: givens[i,j] != 0 };
    1.19 +
    1.20 +/* Set of all feasible boxes of the right size: only this boxes are possible.
    1.21 + * The box contains (i,j) and ranges from (k,l) to (m,n)
    1.22 + */
    1.23 +set B := { (i,j,k,l,m,n) in { V, rows, cols, rows1, cols1 }:
    1.24 +    i >= k and i < m and j >= l and j < n and   /* Contains (i,j) */
    1.25 +    ((m-k)*(n-l)) = givens[i,j] and /* Right size */
    1.26 +    card({ (s,t) in V: s >= k and s < m and t >= l and t < n }) = 1
    1.27 +        /* Contains only (i,j), no other number */
    1.28 +};
    1.29 +
    1.30 +var x{B}, binary;
    1.31 +
    1.32 +/* Cover each square exactly once */
    1.33 +s.t. cover_once{ (s,t) in { rows, cols } }:
    1.34 +    sum{(i,j,k,l,m,n) in B: s >= k and s < m and t >= l and t < n}
    1.35 +        x[i,j,k,l,m,n] = 1;
    1.36 +
    1.37 +minimize cost: 0;
    1.38 +
    1.39 +solve;
    1.40 +
    1.41 +/* Output solution graphically */
    1.42 +printf "\nSolution:\n";
    1.43 +for { row in rows1 } {
    1.44 +    for { col in cols1 } {
    1.45 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.46 +                col >= l and col <= n and (row = k or row = m) and
    1.47 +                x[i,j,k,l,m,n] = 1}) > 0 and
    1.48 +            card({(i,j,k,l,m,n) in B:
    1.49 +                row >= k and row <= m and (col = l or col = n) and
    1.50 +                x[i,j,k,l,m,n] = 1}) > 0} "+";
    1.51 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.52 +                col >= l and col <= n and (row = k or row = m) and
    1.53 +                x[i,j,k,l,m,n] = 1}) = 0 and
    1.54 +            card({(i,j,k,l,m,n) in B:
    1.55 +                row >= k and row <= m and (col = l or col = n) and
    1.56 +                x[i,j,k,l,m,n] = 1}) > 0} "|";
    1.57 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.58 +                row >= k and row <= m and (col = l or col = n) and
    1.59 +                x[i,j,k,l,m,n] = 1}) = 0 and
    1.60 +            card({(i,j,k,l,m,n) in B:
    1.61 +                col >= l and col <= n and (row = k or row = m) and
    1.62 +                x[i,j,k,l,m,n] = 1}) > 0} "-";
    1.63 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.64 +                row >= k and row <= m and (col = l or col = n) and
    1.65 +                x[i,j,k,l,m,n] = 1}) = 0 and
    1.66 +            card({(i,j,k,l,m,n) in B:
    1.67 +                col >= l and col <= n and (row = k or row = m) and
    1.68 +                x[i,j,k,l,m,n] = 1}) = 0} " ";
    1.69 +
    1.70 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.71 +            col >= l and col < n and (row = k or row = m) and
    1.72 +            x[i,j,k,l,m,n] = 1}) > 0} "---";
    1.73 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.74 +            col >= l and col < n and (row = k or row = m) and
    1.75 +            x[i,j,k,l,m,n] = 1}) = 0} "   ";
    1.76 +    }
    1.77 +    printf "\n";
    1.78 +
    1.79 +    for { (col,p) in { cols, 1 }: card({ s in rows: s = row }) = 1 } {
    1.80 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.81 +            row >= k and row < m and (col = l or col = n) and
    1.82 +            x[i,j,k,l,m,n] = 1}) > 0} "|";
    1.83 +        printf{0..0: card({(i,j,k,l,m,n) in B:
    1.84 +            row >= k and row < m and (col = l or col = n) and
    1.85 +            x[i,j,k,l,m,n] = 1}) = 0} " ";
    1.86 +        printf{0..0: card({ (i,j) in V: i = row and j = col}) > 0} " %2d", givens[row,col];
    1.87 +        printf{0..0: card({ (i,j) in V: i = row and j = col}) = 0} "  .";
    1.88 +    }
    1.89 +    printf{0..0: card({ r in rows: r = row }) = 1} "|\n";
    1.90 +}
    1.91 +
    1.92 +data;
    1.93 +
    1.94 +/* This Shikaku is from
    1.95 + * http://www.emn.fr/x-info/sdemasse/gccat/KShikaku.html#uid5449
    1.96 + */
    1.97 +param givens : 1 2 3 4 5 6 7 8 9 10 :=
    1.98 +           1   9 . . . 12 . . 5 . .
    1.99 +           2   . . . . . . . . . .
   1.100 +           3   . . . . . . . . . 6
   1.101 +           4   8 . 6 . 8 . . . . .
   1.102 +           5   . . . . . . . . . .
   1.103 +           6   . . . . . . . . . .
   1.104 +           7   . . . . . 6 . 8 . 12
   1.105 +           8   4 . . . . . . . . .
   1.106 +           9   . . . . . . . . . .
   1.107 +          10   . . 3 . . 9 . . . 4
   1.108 +           ;
   1.109 +
   1.110 +end;