set(arithmetic).
assign(domain_size,24).     
assign(max_models,-1).

formulas(unique_values_in_white_cells).
  all x all y1 all y2 (f(x,y1) = f(x,y2) & (x > 0) & (x < 4) & 
      (y1 > 0) & (y1 < 4) & (y2 > 0) & (y2 < 4) -> y1 = y2).
  all x1 all x2 all y (f(x1,y) = f(x2,y) & (x1 > 0) & (x1 < 4) & 
      (x2 > 0) & (x2 < 4) & (y > 0) & (y < 4)-> x1 = x2).
  all x ((x > 0 & x < 4) -> (f(4,2) != f(x,2)) & (f(4,3) != f(x,3))).   
  all y ((y > 0 & y < 4) -> (f(2,4) != f(2,y)) & (f(3,4) != f(3,y))).
  f(4,2) != f(4,3).    f(2,4) != f(3,4).
end_of_list.

formulas(5x5_left_upper_corner).
  all x all y (((x > 4) | (y > 4)) -> f(x,y) = 0).     %out 5x5 is black 
  f(0,0)  = 0. f(4,0)  = 0. f(0,4)  = 0.  f(4,4) = 0.  %corners are black  

  all x all y (((x > 0) & (x < 4)) & ((y > 0) & (y < 4)) 
        -> ((f(x,y) > 0) & (f(x,y) < 10))).

  f(2,4) >= 1 & f(2,4) <= 9.       f(3,4) >= 1 & f(3,4) <= 9.
  f(4,2) >= 1 & f(4,2) <= 9.       f(4,3) >= 1 & f(4,3) <= 9.
end_of_list.

formulas(sample_puzzle).
  f(0,1) = 23.  f(0,2) = 16.   f(0,3) = 10.     %first line
  f(1,0) = 14.  f(2,0) = 16.   f(3,0) = 14.     %first column
  f(4,1) = 8.   f(1,4) = 3.                     %last line & last column
                                
  f(1,0) = f(1,1) + f(1,2) + f(1,3).            %sum(white) on line 1
  f(2,0) = f(2,1) + f(2,2) + f(2,3) + f(2,4).   %sum(white) on line 2
  f(3,0) = f(3,1) + f(3,2) + f(3,3) + f(3,4).   %sum(white) on line 3
  f(4,1) = f(4,2) + f(4,3).                     %sum(white) on line 4
  f(0,1) = f(1,1) + f(2,1) + f(3,1).            %sum(white) on column 1
  f(0,2) = f(1,2) + f(2,2) + f(3,2) + f(4,2).   %sum(white) on column 2
  f(0,3) = f(1,3) + f(2,3) + f(3,3) + f(4,3).   %sum(white) on column 3
  f(1,4) = f(2,4) + f(3,4).                     %sum(white) on column 4
end_of_list.

