examples/pbn.mod
changeset 1 c445c931472f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/examples/pbn.mod	Mon Dec 06 13:09:21 2010 +0100
     1.3 @@ -0,0 +1,194 @@
     1.4 +/* PBN, Paint-By-Numbers Puzzle */
     1.5 +
     1.6 +/* Written in GNU MathProg by Andrew Makhorin <mao@gnu.org> */
     1.7 +
     1.8 +/* A paint-by-number puzzle consists of an m*n grid of pixels (the
     1.9 +   canvas) together with m+n cluster-size sequences, one for each row
    1.10 +   and column. The goal is to paint the canvas with a picture that
    1.11 +   satisfies the following constraints:
    1.12 +
    1.13 +   1. Each pixel must be blank or white.
    1.14 +
    1.15 +   2. If a row or column has cluster-size sequence s1, s2, ..., sk,
    1.16 +      then it must contain k clusters of black pixels - the first with
    1.17 +      s1 black pixels, the second with s2 black pixels, and so on.
    1.18 +
    1.19 +   It should be noted that "first" means "leftmost" for rows and
    1.20 +   "topmost" for columns, and that rows and columns need not begin or
    1.21 +   end with black pixels.
    1.22 +
    1.23 +   Example:
    1.24 +                  1   1
    1.25 +                  1   1
    1.26 +              2 1 1 1 1 1 2 3
    1.27 +              3 2 1 2 1 2 3 4 8 9
    1.28 +
    1.29 +        3 6   # # # . # # # # # #
    1.30 +        1 4   # . . . . . # # # #
    1.31 +      1 1 3   . . # . # . . # # #
    1.32 +          2   . . . . . . . . # #
    1.33 +        3 3   . . # # # . . # # #
    1.34 +        1 4   # . . . . . # # # #
    1.35 +        2 5   # # . . . # # # # #
    1.36 +        2 5   # # . . . # # # # #
    1.37 +        1 1   . . . # . . . . . #
    1.38 +          3   . . # # # . . . . .
    1.39 +
    1.40 +   (In Russia this sort of puzzles is known as "Japanese crossword".)
    1.41 +
    1.42 +   References:
    1.43 +   Robert A. Bosch, "Painting by Numbers", 2000.
    1.44 +   <http://www.oberlin.edu/~math/faculty/bosch/pbn-page.html> */
    1.45 +
    1.46 +param m, integer, >= 1;
    1.47 +/* the number of rows */
    1.48 +
    1.49 +param n, integer, >= 1;
    1.50 +/* the number of columns */
    1.51 +
    1.52 +param row{i in 1..m, 1..n div 2}, integer, >= 0, default 0;
    1.53 +/* the cluster-size sequence for row i (raw data) */
    1.54 +
    1.55 +param col{j in 1..n, 1..m div 2}, integer, >= 0, default 0;
    1.56 +/* the cluster-size sequence for column j (raw data) */
    1.57 +
    1.58 +param kr{i in 1..m} := sum{t in 1..n div 2: row[i,t] > 0} 1;
    1.59 +/* the number of clusters in row i */
    1.60 +
    1.61 +param kc{j in 1..n} := sum{t in 1..m div 2: col[j,t] > 0} 1;
    1.62 +/* the number of clusters in column j */
    1.63 +
    1.64 +param sr{i in 1..m, t in 1..kr[i]} := row[i,t], integer, >= 1;
    1.65 +/* the cluster-size sequence for row i */
    1.66 +
    1.67 +param sc{j in 1..n, t in 1..kc[j]} := col[j,t], integer, >= 1;
    1.68 +/* the cluster-size sequence for column j */
    1.69 +
    1.70 +check{i in 1..m}: sum{t in 1..kr[i]} sr[i,t] <= n - (kr[i] - 1);
    1.71 +/* check that the sum of the cluster sizes in each row is valid */
    1.72 +
    1.73 +check{j in 1..n}: sum{t in 1..kc[j]} sc[j,t] <= m - (kc[j] - 1);
    1.74 +/* check that the sum of the cluster sizes in each column is valid */
    1.75 +
    1.76 +check: sum{i in 1..m, t in 1..kr[i]} sr[i,t] =
    1.77 +       sum{j in 1..n, t in 1..kc[j]} sc[j,t];
    1.78 +/* check that the sum of the cluster sizes in all rows is equal to the
    1.79 +   sum of the cluster sizes in all columns */
    1.80 +
    1.81 +param er{i in 1..m, t in 1..kr[i]} :=
    1.82 +   if t = 1 then 1 else er[i,t-1] + sr[i,t-1] + 1;
    1.83 +/* the smallest value of j such that row i's t-th cluster can be
    1.84 +   placed in row i with its leftmost pixel occupying pixel j */
    1.85 +
    1.86 +param lr{i in 1..m, t in 1..kr[i]} :=
    1.87 +   if t = kr[i] then n + 1 - sr[i,t] else lr[i,t+1] - sr[i,t] - 1;
    1.88 +/* the largest value of j such that row i's t-th cluster can be
    1.89 +   placed in row i with its leftmost pixel occupying pixel j */
    1.90 +
    1.91 +param ec{j in 1..n, t in 1..kc[j]} :=
    1.92 +   if t = 1 then 1 else ec[j,t-1] + sc[j,t-1] + 1;
    1.93 +/* the smallest value of i such that column j's t-th cluster can be
    1.94 +   placed in column j with its topmost pixel occupying pixel i */
    1.95 +
    1.96 +param lc{j in 1..n, t in 1..kc[j]} :=
    1.97 +   if t = kc[j] then m + 1 - sc[j,t] else lc[j,t+1] - sc[j,t] - 1;
    1.98 +/* the largest value of i such that column j's t-th cluster can be
    1.99 +   placed in column j with its topmost pixel occupying pixel i */
   1.100 +
   1.101 +var z{i in 1..m, j in 1..n}, binary;
   1.102 +/* z[i,j] = 1, if row i's j-th pixel is painted black
   1.103 +   z[i,j] = 0, if row i's j-th pixel is painted white */
   1.104 +
   1.105 +var y{i in 1..m, t in 1..kr[i], j in er[i,t]..lr[i,t]}, binary;
   1.106 +/* y[i,t,j] = 1, if row i's t-th cluster is placed in row i with its
   1.107 +                 leftmost pixel occupying pixel j
   1.108 +   y[i,t,j] = 0, if not */
   1.109 +
   1.110 +var x{j in 1..n, t in 1..kc[j], i in ec[j,t]..lc[j,t]}, binary;
   1.111 +/* x[j,t,i] = 1, if column j's t-th cluster is placed in column j with
   1.112 +                 its topmost pixel occupying pixel i
   1.113 +   x[j,t,i] = 0, if not */
   1.114 +
   1.115 +s.t. fa{i in 1..m, t in 1..kr[i]}:
   1.116 +     sum{j in er[i,t]..lr[i,t]} y[i,t,j] = 1;
   1.117 +/* row i's t-th cluster must appear in row i exactly once */
   1.118 +
   1.119 +s.t. fb{i in 1..m, t in 1..kr[i]-1, j in er[i,t]..lr[i,t]}:
   1.120 +     y[i,t,j] <= sum{jp in j+sr[i,t]+1..lr[i,t+1]} y[i,t+1,jp];
   1.121 +/* row i's (t+1)-th cluster must be placed to the right of its t-th
   1.122 +   cluster */
   1.123 +
   1.124 +s.t. fc{j in 1..n, t in 1..kc[j]}:
   1.125 +     sum{i in ec[j,t]..lc[j,t]} x[j,t,i] = 1;
   1.126 +/* column j's t-th cluster must appear in column j exactly once */
   1.127 +
   1.128 +s.t. fd{j in 1..n, t in 1..kc[j]-1, i in ec[j,t]..lc[j,t]}:
   1.129 +     x[j,t,i] <= sum{ip in i+sc[j,t]+1..lc[j,t+1]} x[j,t+1,ip];
   1.130 +/* column j's (t+1)-th cluster must be placed below its t-th cluster */
   1.131 +
   1.132 +s.t. fe{i in 1..m, j in 1..n}:
   1.133 +     z[i,j] <= sum{t in 1..kr[i], jp in er[i,t]..lr[i,t]:
   1.134 +                   j-sr[i,t]+1 <= jp and jp <= j} y[i,t,jp];
   1.135 +/* the double coverage constraint stating that if row i's j-th pixel
   1.136 +   is painted black, then at least one of row i's clusters must be
   1.137 +   placed in such a way that it covers row i's j-th pixel */
   1.138 +
   1.139 +s.t. ff{i in 1..m, j in 1..n}:
   1.140 +     z[i,j] <= sum{t in 1..kc[j], ip in ec[j,t]..lc[j,t]:
   1.141 +                   i-sc[j,t]+1 <= ip and ip <= i} x[j,t,ip];
   1.142 +/* the double coverage constraint making sure that if row i's j-th
   1.143 +   pixel is painted black, then at least one of column j's clusters
   1.144 +   covers it */
   1.145 +
   1.146 +s.t. fg{i in 1..m, j in 1..n, t in 1..kr[i], jp in er[i,t]..lr[i,t]:
   1.147 +     j-sr[i,t]+1 <= jp and jp <= j}: z[i,j] >= y[i,t,jp];
   1.148 +/* the constraint to prevent white pixels from being covered by the
   1.149 +   row clusters */
   1.150 +
   1.151 +s.t. fh{i in 1..m, j in 1..n, t in 1..kc[j], ip in ec[j,t]..lc[j,t]:
   1.152 +     i-sc[j,t]+1 <= ip and ip <= i}: z[i,j] >= x[j,t,ip];
   1.153 +/* the constraint to prevent white pixels from being covered by the
   1.154 +   column clusters */
   1.155 +
   1.156 +/* there is no need for an objective function here */
   1.157 +
   1.158 +solve;
   1.159 +
   1.160 +for {i in 1..m}
   1.161 +{  printf{j in 1..n} " %s", if z[i,j] then "#" else ".";
   1.162 +   printf "\n";
   1.163 +}
   1.164 +
   1.165 +data;
   1.166 +
   1.167 +/* These data correspond to the example above. */
   1.168 +
   1.169 +param m := 10;
   1.170 +
   1.171 +param n := 10;
   1.172 +
   1.173 +param row : 1 2 3 4 :=
   1.174 +         1  3 6 . .
   1.175 +         2  1 4 . .
   1.176 +         3  1 1 3 .
   1.177 +         4  2 . . .
   1.178 +         5  3 3 . .
   1.179 +         6  1 4 . .
   1.180 +         7  2 5 . .
   1.181 +         8  2 5 . .
   1.182 +         9  1 1 . .
   1.183 +        10  3 . . . ;
   1.184 +
   1.185 +param col : 1 2 3 4 :=
   1.186 +         1  2 3 . .
   1.187 +         2  1 2 . .
   1.188 +         3  1 1 1 1
   1.189 +         4  1 2 . .
   1.190 +         5  1 1 1 1
   1.191 +         6  1 2 . .
   1.192 +         7  2 3 . .
   1.193 +         8  3 4 . .
   1.194 +         9  8 . . .
   1.195 +        10  9 . . . ;
   1.196 +
   1.197 +end;