% problem-set/puzzles/space_state/chekndom.ver1.in
% created : 07/09/86
% revised : 07/13/88

% description:
%
% This run solves "The Checkerboard and Dominoes Puzzle" using 
% hyper-resolution.
%
%           THE CHECKERBOARD AND DOMINOES PUZZLE
%
%    There is a checker board whose upper left and lower right
%    squares have been removed. There is a box of dominoes that
%    are one square by two squares in size. Can you exactly cover
%    the checker board with dominoes?

% representation:
%
% Procedural version:
% COMMENTS : Since the clause-set is satisfiable, there is no proof by .
%            contradiction.
% PREDICATES :
%             ACHIEVABLE(arg1,arg2): Gives the state of each row and the
%                                    individual squares in the row.
% FUNCTIONS  :
%             row(x): x in this function indicate the row number.
%             squares(): gives the state of each square in a particular
%             row. 'c' stands for covered, 'n' for not covered.
%                         and 'r' for removed.
%             compl(x): Changes the state of a square from x to another.
% For each row : If an adjacent pair of checkers are not covered then,  
% cover them , until every such pair in that row has been looked at..
 
set(hyper_res).


list(axioms).

% Place a domino horizontally, where possible

-ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) |
 ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)).
-ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) |
 ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)).
-ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) |
 ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)).
-ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) |
 ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)).
-ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) |
 ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)).
-ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) |
 ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)).
-ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) |
 ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)).  

% If the Row is complete then examine the Row directly below..
% Then depending, on the complementary function, change the state
% of the squares. This may place several dominoes vertically.

-ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) |
 ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2),
     compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))).
 
% The end condition (to stop when the 8th Row is finished)

 ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)).
 
end_of_list.


list(sos).

% Initial condition.

 ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,n,n)).

% If it is possible to cover the checkerboard using dominoes then the.
% resulting statement will unify with this clause giving a proof by.
% contradiction. If it is not possible, the set of support will be
% exhausted.

-ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,n)).

end_of_list.

list(demodulators).
 
 EQUAL(compl(c),n).
 EQUAL(compl(n),c).
 EQUAL(compl(r),n).
 EQUAL(succ(1),2).
 EQUAL(succ(2),3).
 EQUAL(succ(3),4).
 EQUAL(succ(4),5).
 EQUAL(succ(5),6).
 EQUAL(succ(6),7).
 EQUAL(succ(7),8).
 EQUAL(succ(8),9).

end_of_list.
