set(integer_ring).  % <+,-,*> is ring of integers mod n (-- is binary minus)
set(order_domain).  % < and <= order the domain

formulas(assumptions).

% n-Queens Puzzle
%
% In this representation, Q(i)=n means that Row i Column n has a queen.
% The constraint that no queens can be in the same row is always satisfied
% in this representation, because Q is a function; that is,
% Q(x) != Q(z) -> x != z  is always satisfied.

x != z -> Q(x) != Q(z).   % No 2 queens in the same column.

% We have to be careful that diagonals do not wrap around, because
% modular arithmetic wraps around.  Thus, the < conditions.

x < z & Q(x) < Q(z) ->  z -- x != Q(z) -- Q(x).  % No 2 queens in \ diagonal.

x < z & Q(z) < Q(x) ->  z -- x != Q(x) -- Q(z).  % No 2 queens in / diagonal.

end_of_list.
