014: Solitaire Battleships

% new zinc file SolitaireBattleships.mzn
% At attempt to build a solution entirely within the IDE
% By Peter Stuckey August 2009
% Solitaire Battleships is a puzzle where
% we are given a partially filled in board and the number
% of ships in each row and column and have to fill it with ships

% "Improved" version does not introduce reified set_in

int: width;   % height of board (usually 10)
int: height;  % width of board (usually 10)
int: maxship; % maximal length of ship (usually 4)


set of int: ROWS = 1..width;
set of int: COLS = 1..height;
set of int: XROWS = 0..width+1;    % extended rows
set of int: XCOLS = 0..height+1;   % extended cols

%% ship types enumerated type
set of int: SHIPS = 1..maxship;  % different ship types
int: submarine = 1;
int: destroyer = 2;
int: cruiser = 3;
int: battleship = 4;


%% the PIECES enumerated type!
set of int: PIECES = 1..7;
int: w = 1; % water
int: c = 2; % circle (submarine)
int: l = 3; % left end of ship
int: r = 4; % right end of ship
int: t = 5; % top of ship
int: b = 6; % bottom of ship
int: m = 7; % middle of ship
array[PIECES] of string: code = [".","c","l","r","t","b","m"];

array[ROWS,COLS] of 0..7: hint; % the initial board configuration
array[ROWS] of int: rowsum;     % sums for each row
array[COLS] of int: colsum;     % sums for each col
array[SHIPS] of int: ship; % the number of each type of ship (usually [4,3,2,1]).



% variables 
array[XROWS,XCOLS] of var PIECES: board;  % the board
 
array[XROWS,XCOLS] of var 0..1: fill;     % which pieces are ships

array[PIECES] of var 0..width*height: npiece; % number of pieces of each type


% model

% ensure hints are respected
constraint forall(i in ROWS, j in COLS)(
			   if hint[i,j] != 0 then
			   		board[i,j] == hint[i,j]
			   else true endif
	       ); 

% make extended rows and cols empty
constraint forall(i in XROWS)(board[i,0] == w /\ board[i,width+1] == w);
constraint forall(j in COLS)(board[0,j] == w /\ board[height+1,j] == w);

% ensure that the fill array matches the board
constraint forall(i in XROWS, j in XCOLS)(
			   fill[i,j] = bool2int(board[i,j] != w)
	       ); 

% spacing constraints: gaps betwen ships
constraint forall(i in ROWS, j in COLS)(
	   (board[i,j] == w \/ board[i+1,j+1] == w)
	/\ (board[i,j] == w \/ board[i+1,j-1] == w)   % diagonal constraints
            /\ (board[i,j] in {c,l,r,t} -> board[i-1,j] == w)
            /\ (board[i,j] in {c,l,r,b} -> board[i+1,j] == w)
            /\ (board[i,j] in {c,l,t,b} -> board[i,j-1] == w)
            /\ (board[i,j] in {c,r,t,b} -> board[i,j+1] == w)
           );
               			                       
% ship shape constraints
constraint forall(i in ROWS, j in COLS)(
               %% a left piece needs a right piece or middle to the right
			   (board[i,j] == l -> (board[i,j+1] == r \/ board[i,j+1] == m))
			/\ (board[i,j] == r -> (board[i,j-1] == l \/ board[i,j-1] == m))
			/\ (board[i,j] == t -> (board[i+1,j] == b \/ board[i+1,j] == m))
			/\ (board[i,j] == b -> (board[i-1,j] == t \/ board[i-1,j] == m))
			   %% a middle piece has to have two opposite sides filled
			/\ (board[i,j] == m -> (   fill[i-1,j] == fill[i+1,j]
			                        /\ fill[i,j-1] == fill[i,j+1]
			                        /\ fill[i-1,j] + fill[i,j-1] == 1))
		   );
		   
% sum up pieces
constraint forall(p in PIECES)(
			   sum(i in ROWS, j in COLS)(bool2int(board[i,j] == p)) == npiece[p]
		   );

% piece sum constraints
constraint npiece[c] == ship[submarine]; % submarines
constraint npiece[l] == npiece[r]; % left right (probably redundant)
constraint npiece[t] == npiece[b]; % top bottom
constraint npiece[l] + npiece[t] == sum(s in destroyer..maxship)(ship[s]); 
                                   % no of ends
constraint npiece[m] == sum(s in cruiser..maxship)(ship[s] * (s - 2)); 
                                   % no of middles 		   
		    
% count number of bigger ships
% at least for standard battleships you can probably simply
% enforce this constraint for s in destroyer..destroyer		
% and still be guaranteed a correct solution    
constraint forall(s in destroyer..maxship)(
	           sum(i in ROWS,j in COLS)(bool2int(
			       if j + s - 1 <= width then
			          board[i,j] == l /\ board[i,j+s-1] == r     % ship length s lr
			       /\ forall(k in j+1..j+s-2)(board[i,k] == m)
			       else false endif
			    \/
			       if i + s - 1 <= height then
			          board[i,j] == t /\ board[i+s-1,j] == b     % ship length s tb
			       /\ forall(k in i+1..i+s-2)(board[k,j] == m)
			       else false endif
		       )) = ship[s]
		   );		    
		    		    

% row sums respected
constraint forall(i in ROWS)(
               sum(j in COLS)(fill[i,j]) == rowsum[i]
           );
           
% column sums respected           
constraint forall(j in COLS)(
               sum(i in ROWS)(fill[i,j]) == colsum[j]
           );           


solve :: int_search([ fill[i,j] | i in ROWS, j in COLS], 
      		  input_order, indomain_min, complete)
      satisfy;

output [ code[fix(board[i,j])] ++ 
		 if j == width then " " ++ show(rowsum[i]) ++ "\n"
		 else "" endif
	   | i in ROWS, j in COLS ]  ++
	   [ show(colsum[j]) | j in COLS ] ++ ["\n"];