2.5.2 Light Up Puzzle (lightup1)

Run LPL Code  ,  PDF Document


The Light-Up puzzle consists of a rectangular grid of squares which are white or black. Every black filled square contains a number from 0 to 4, or may have no number. The aim is to place lights in the white squares so that

  1. Each white square is illuminated, that is, it can see a light through an uninterrupted horizontal or vertical line of white squares.

  2. No two lights can see each other.

  3. The number of lights adjacent to a numbered filled square is exactly the number in the filled square.

The puzzle is from MiniZinc Docs. An example of a puzzle is given in Figure 3.


Figure 3: A Light Up Puzzle

Modeling Steps

For the size w × h (width/height) of the grid, we define a set j,j1 W = {1,,w} and i,i1 H = {1,,h}. A parameter bi,j [-1,, 5] is declared for every square (i,j) in the grid: bi,j = -1 means the square is white, bi,j = 5 means the black square is empty, otherwise (bi,j [0,, 4]) the square is black and contains the digit bi,j.

Furthermore, a 4-dimensional relationship, called visible, V i,j,i1,j1 is defined which is true if square (i1,j1) is visible from square (i,j), otherwise V i,j,i1,j1 is false.

We want to know in which squares to put a light: a binary variable xi,j is introduced, it is = 1, if a light has to be placed in square (i,j), otherwise it is = 0.

There are four constraints:

(1) A black square does not have a light:

xi,j = 0   forall i ∈ H, j ∈ W, bi,j ⁄= - 1

(2) For a black numbered square (i,j), the number of lights in the four neighbours (left/right, top/down) must correspond to the number in the square:

            xi1,j1 = bi,j   forall i ∈ H, j ∈ W, bi,j ∈ [0, ...,4]

 whereR  (i,j,i1,j1) = i - 1 ≤ i1 ≤ i + 1 ∧  j - 1 ≤ j1 ≤ j + 1 ∧  |i1 - i| + |j1 - j| = 1

(3) For all white squares (i,j) that are visible from (i,j1) or from (i1,j), either (i,j1) or (i1,j) (or both) must have a light:

  ∨              ∨
       xi,j1 ∨          xi1,j   forall i ∈ H, j ∈ W, bi,j = - 1

j1|Vi,j,i,j1        i1|Vi,j,i1,j

(4) For two different squares (i,j) and (i1,j1) that are visible from each other, only one can have a light:

xi,j nand xi1,j1   forall (i,j,i1,j1 ) ∈ V, i ⁄= i1, j ⁄= j1, bi,j = bi1,j1 = - 1


The data file for LPL can be downloaded from lightup1.txt. The solution for this data is given in Figure 4, generated by the output model of LPL (see below).

Further Comments

LPL and MiniZinc are similar in the notation of a logical constraint (both use exist (exists), and ( /'  ), or ( ' / ) to express the constraint. In contrast to MiniZinc and depending on the the solver used, LPL translates the logical constraints into purely mathematical statements if using a MIP solver.

LPL code (run lightup)

model lightup1 "Light Up Puzzle"; 
  set i,i1,H;  // board height 
  set j,j1,W;  // board width 
  parameter b{i,j} [-1..5];  // board 
    E := -1;                 // empty square 
    F :=  5;           // empty black square 
  set visible{i,j,i1,j1}; 
  binary variable x{i,j}; // is there a light 
  constraint C1{i,j|b<>E}: x=0; 
  constraint C2{i,j|b=E nor b=F}: 
    sum{i1,j1|i-1<=i1<=i+1 and j-1<=j1<=j+1 and 
      Abs(i1-i)+Abs(j1-j)=1}  x[i1,j1] = b[i,j]; 
  constraint C3{i,j|b=E}: 
    exist{j1|visible[i,j,i,j1]} x[i,j1] or 
    exist{i1|visible[i,j,i1,j]} x[i1,j]; 
  constraint C4{visible[i,j,i1,j1]|i<>i1 or j<>j1}: 
      x[i,j] nand x[i1,j1]; 
model data "the data model"; 
  parameter h; w; 
  i:=1..h; j:=1..w; 
  Read{i}(',;1',{j} b); 
  visible{i,j,i1,j1} := 
  (i=i1) and and{j2 in W|Min(j,j1)<=j2<=Max(j,j1)}(b[i,j2]=E) or 
  (j=j1) and and{i2 in H|Min(i,i1)<=i2<=Max(i,i1)}(b[i2,j]=E); 

MiniZinc code (download lightup1.mzn)

int: h; set of int: H = 1..h; % board height 
int: w; set of int: W = 1..w; % board width 
array[H,W] of -1..5: b;       % board 
int: E = -1;                  % empty square 
set of int: N = 0..4;  % filled and numbered square 
int: F =  5;           % filled unnumbered square 
test visible(int: i1, int: j1, int: i2, int: j2) = 
  ((i1 == i2) /' forall(j in min(j1,j2)..max(j1,j2)) 
      (b[i1,j] == E)) ' / 
  ((j1 == j2) /' forall(i in min(i1,i2)..max(i1,i2)) 
      (b[i,j1] == E)); 
array[H,W] of var bool: x; % is there a light 
constraint forall(i in H, j in W where b[i,j] != E)(x[i,j] == false); 
constraint forall(i in H, j in W where b[i,j] in N)( 
    bool_sum_eq([ x[i1,j1] | i1 in i-1..i+1, 
     j1 in j-1..j+1 where abs(i1-i) + abs(j1-j) == 1 
       /' i1 in H /' j1 in W ], b[i,j])); 
constraint forall(i in H, j in W where b[i,j] == E)( 
 exists(j1 in W where visible(i,j,i,j1))(x[i,j1]) ' / 
 exists(i1 in H where visible(i,j,i1,j))(x[i1,j])); 
constraint forall(i1,i2 in H, j1,j2 in W where 
  (i1 != i2 ' / j1 != j2) /' b[i1,j1] == E 
  /' b[i2,j2] == E /' visible(i1,j1,i2,j2)) 
   (not x[i1,j1] ' / not x[i2,j2]); 
solve satisfy;

LPL output model is as follows

model output; 
  Write{i}('%2s ' n',{j} if(b<>E,b&'',x=1,'L','.')); 
  --{i,j} Draw.Rect(if(b=E or b=F,'',''&b),j,i,1,1,if(b=-1,1,0),0); 
  {i,j} Draw.Rect(if(b=E or b=F,'',''&b),j,i,1,1,if(b=-1,6,0),0); 
  {i,j|x} Draw.Circle(j+.5,i+.5,0.4,1,0); 

The output model generates the Figure 4


Figure 4: Solution of the Lightup Puzzle

output [ if b[i,j] != E then show(b[i,j]) 
         else if fix(x[i,j]) then "L" else "." endif 
         endif ++ if j == w then "' n" else " " endif 
         | i in H, j in W];

MiniZinc data file (download lightup1.dzn)

h = 7; 
w = 7; 
b = [| -1,-1,-1,-1, 0,-1,-1 
     | -1,-1,-1,-1,-1,-1,-1 
     |  0,-1,-1, 3,-1,-1,-1 
     | -1,-1, 2,-1, 4,-1,-1 
     | -1,-1,-1, 5,-1,-1, 1 
     | -1,-1,-1,-1,-1,-1,-1 
     |  1,-1, 2,-1,-1,-1,-1 |];