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.