examples/pbn.mod
author Alpar Juttner <alpar@cs.elte.hu>
Sun, 05 Dec 2010 17:35:23 +0100
changeset 2 4c8956a7bdf4
permissions -rw-r--r--
Set up CMAKE build environment
     1 /* PBN, Paint-By-Numbers Puzzle */
     2 
     3 /* Written in GNU MathProg by Andrew Makhorin <mao@gnu.org> */
     4 
     5 /* A paint-by-number puzzle consists of an m*n grid of pixels (the
     6    canvas) together with m+n cluster-size sequences, one for each row
     7    and column. The goal is to paint the canvas with a picture that
     8    satisfies the following constraints:
     9 
    10    1. Each pixel must be blank or white.
    11 
    12    2. If a row or column has cluster-size sequence s1, s2, ..., sk,
    13       then it must contain k clusters of black pixels - the first with
    14       s1 black pixels, the second with s2 black pixels, and so on.
    15 
    16    It should be noted that "first" means "leftmost" for rows and
    17    "topmost" for columns, and that rows and columns need not begin or
    18    end with black pixels.
    19 
    20    Example:
    21                   1   1
    22                   1   1
    23               2 1 1 1 1 1 2 3
    24               3 2 1 2 1 2 3 4 8 9
    25 
    26         3 6   # # # . # # # # # #
    27         1 4   # . . . . . # # # #
    28       1 1 3   . . # . # . . # # #
    29           2   . . . . . . . . # #
    30         3 3   . . # # # . . # # #
    31         1 4   # . . . . . # # # #
    32         2 5   # # . . . # # # # #
    33         2 5   # # . . . # # # # #
    34         1 1   . . . # . . . . . #
    35           3   . . # # # . . . . .
    36 
    37    (In Russia this sort of puzzles is known as "Japanese crossword".)
    38 
    39    References:
    40    Robert A. Bosch, "Painting by Numbers", 2000.
    41    <http://www.oberlin.edu/~math/faculty/bosch/pbn-page.html> */
    42 
    43 param m, integer, >= 1;
    44 /* the number of rows */
    45 
    46 param n, integer, >= 1;
    47 /* the number of columns */
    48 
    49 param row{i in 1..m, 1..n div 2}, integer, >= 0, default 0;
    50 /* the cluster-size sequence for row i (raw data) */
    51 
    52 param col{j in 1..n, 1..m div 2}, integer, >= 0, default 0;
    53 /* the cluster-size sequence for column j (raw data) */
    54 
    55 param kr{i in 1..m} := sum{t in 1..n div 2: row[i,t] > 0} 1;
    56 /* the number of clusters in row i */
    57 
    58 param kc{j in 1..n} := sum{t in 1..m div 2: col[j,t] > 0} 1;
    59 /* the number of clusters in column j */
    60 
    61 param sr{i in 1..m, t in 1..kr[i]} := row[i,t], integer, >= 1;
    62 /* the cluster-size sequence for row i */
    63 
    64 param sc{j in 1..n, t in 1..kc[j]} := col[j,t], integer, >= 1;
    65 /* the cluster-size sequence for column j */
    66 
    67 check{i in 1..m}: sum{t in 1..kr[i]} sr[i,t] <= n - (kr[i] - 1);
    68 /* check that the sum of the cluster sizes in each row is valid */
    69 
    70 check{j in 1..n}: sum{t in 1..kc[j]} sc[j,t] <= m - (kc[j] - 1);
    71 /* check that the sum of the cluster sizes in each column is valid */
    72 
    73 check: sum{i in 1..m, t in 1..kr[i]} sr[i,t] =
    74        sum{j in 1..n, t in 1..kc[j]} sc[j,t];
    75 /* check that the sum of the cluster sizes in all rows is equal to the
    76    sum of the cluster sizes in all columns */
    77 
    78 param er{i in 1..m, t in 1..kr[i]} :=
    79    if t = 1 then 1 else er[i,t-1] + sr[i,t-1] + 1;
    80 /* the smallest value of j such that row i's t-th cluster can be
    81    placed in row i with its leftmost pixel occupying pixel j */
    82 
    83 param lr{i in 1..m, t in 1..kr[i]} :=
    84    if t = kr[i] then n + 1 - sr[i,t] else lr[i,t+1] - sr[i,t] - 1;
    85 /* the largest value of j such that row i's t-th cluster can be
    86    placed in row i with its leftmost pixel occupying pixel j */
    87 
    88 param ec{j in 1..n, t in 1..kc[j]} :=
    89    if t = 1 then 1 else ec[j,t-1] + sc[j,t-1] + 1;
    90 /* the smallest value of i such that column j's t-th cluster can be
    91    placed in column j with its topmost pixel occupying pixel i */
    92 
    93 param lc{j in 1..n, t in 1..kc[j]} :=
    94    if t = kc[j] then m + 1 - sc[j,t] else lc[j,t+1] - sc[j,t] - 1;
    95 /* the largest value of i such that column j's t-th cluster can be
    96    placed in column j with its topmost pixel occupying pixel i */
    97 
    98 var z{i in 1..m, j in 1..n}, binary;
    99 /* z[i,j] = 1, if row i's j-th pixel is painted black
   100    z[i,j] = 0, if row i's j-th pixel is painted white */
   101 
   102 var y{i in 1..m, t in 1..kr[i], j in er[i,t]..lr[i,t]}, binary;
   103 /* y[i,t,j] = 1, if row i's t-th cluster is placed in row i with its
   104                  leftmost pixel occupying pixel j
   105    y[i,t,j] = 0, if not */
   106 
   107 var x{j in 1..n, t in 1..kc[j], i in ec[j,t]..lc[j,t]}, binary;
   108 /* x[j,t,i] = 1, if column j's t-th cluster is placed in column j with
   109                  its topmost pixel occupying pixel i
   110    x[j,t,i] = 0, if not */
   111 
   112 s.t. fa{i in 1..m, t in 1..kr[i]}:
   113      sum{j in er[i,t]..lr[i,t]} y[i,t,j] = 1;
   114 /* row i's t-th cluster must appear in row i exactly once */
   115 
   116 s.t. fb{i in 1..m, t in 1..kr[i]-1, j in er[i,t]..lr[i,t]}:
   117      y[i,t,j] <= sum{jp in j+sr[i,t]+1..lr[i,t+1]} y[i,t+1,jp];
   118 /* row i's (t+1)-th cluster must be placed to the right of its t-th
   119    cluster */
   120 
   121 s.t. fc{j in 1..n, t in 1..kc[j]}:
   122      sum{i in ec[j,t]..lc[j,t]} x[j,t,i] = 1;
   123 /* column j's t-th cluster must appear in column j exactly once */
   124 
   125 s.t. fd{j in 1..n, t in 1..kc[j]-1, i in ec[j,t]..lc[j,t]}:
   126      x[j,t,i] <= sum{ip in i+sc[j,t]+1..lc[j,t+1]} x[j,t+1,ip];
   127 /* column j's (t+1)-th cluster must be placed below its t-th cluster */
   128 
   129 s.t. fe{i in 1..m, j in 1..n}:
   130      z[i,j] <= sum{t in 1..kr[i], jp in er[i,t]..lr[i,t]:
   131                    j-sr[i,t]+1 <= jp and jp <= j} y[i,t,jp];
   132 /* the double coverage constraint stating that if row i's j-th pixel
   133    is painted black, then at least one of row i's clusters must be
   134    placed in such a way that it covers row i's j-th pixel */
   135 
   136 s.t. ff{i in 1..m, j in 1..n}:
   137      z[i,j] <= sum{t in 1..kc[j], ip in ec[j,t]..lc[j,t]:
   138                    i-sc[j,t]+1 <= ip and ip <= i} x[j,t,ip];
   139 /* the double coverage constraint making sure that if row i's j-th
   140    pixel is painted black, then at least one of column j's clusters
   141    covers it */
   142 
   143 s.t. fg{i in 1..m, j in 1..n, t in 1..kr[i], jp in er[i,t]..lr[i,t]:
   144      j-sr[i,t]+1 <= jp and jp <= j}: z[i,j] >= y[i,t,jp];
   145 /* the constraint to prevent white pixels from being covered by the
   146    row clusters */
   147 
   148 s.t. fh{i in 1..m, j in 1..n, t in 1..kc[j], ip in ec[j,t]..lc[j,t]:
   149      i-sc[j,t]+1 <= ip and ip <= i}: z[i,j] >= x[j,t,ip];
   150 /* the constraint to prevent white pixels from being covered by the
   151    column clusters */
   152 
   153 /* there is no need for an objective function here */
   154 
   155 solve;
   156 
   157 for {i in 1..m}
   158 {  printf{j in 1..n} " %s", if z[i,j] then "#" else ".";
   159    printf "\n";
   160 }
   161 
   162 data;
   163 
   164 /* These data correspond to the example above. */
   165 
   166 param m := 10;
   167 
   168 param n := 10;
   169 
   170 param row : 1 2 3 4 :=
   171          1  3 6 . .
   172          2  1 4 . .
   173          3  1 1 3 .
   174          4  2 . . .
   175          5  3 3 . .
   176          6  1 4 . .
   177          7  2 5 . .
   178          8  2 5 . .
   179          9  1 1 . .
   180         10  3 . . . ;
   181 
   182 param col : 1 2 3 4 :=
   183          1  2 3 . .
   184          2  1 2 . .
   185          3  1 1 1 1
   186          4  1 2 . .
   187          5  1 1 1 1
   188          6  1 2 . .
   189          7  2 3 . .
   190          8  3 4 . .
   191          9  8 . . .
   192         10  9 . . . ;
   193 
   194 end;