% mqueens.pi (by Neng-Fa Zhou, Sep. 25, 2013, tested by Hakan Kjellerstrand)
% http://www.hakank.org/constraint_programming/cp2013_competition_20130919.pdf
%
% Use the following command to solve an instance File
%
% picat mqueens < File
%
% or type 'test' to solve the included instance.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
import sat.
go =>
queens(11).
main =>
N = read_int(),
queens(N).
queens(N) =>
Q = new_array(N,N),
Q :: 0..1,
foreach(I in 1..N, J in 1..N) % every square is controlled
controlled(Q,I,J,N)
end,
foreach(I in 1..N) % no two queens in one row
sum([Q[I,J] : J in 1..N]) #=< 1
end,
foreach(J in 1..N) % no two queens in one column
sum([Q[I,J] : I in 1..N]) #=< 1
end,
foreach(K in 1-N..N-1) % no two queens in a diagonal
sum([Q[I,J] : I in 1..N, J in 1..N, I-J==K]) #=< 1
end,
foreach(K in 2..2*N)
sum([Q[I,J] : I in 1..N, J in 1..N, I+J==K]) #=< 1
end,
Obj #= sum([Q[I,J] : I in 1..N, J in 1..N]),
solve($[min(Obj),report(output(Q,N,Obj))],[Obj|Q]).
% the squre (I,J) is controlled by a queen
controlled(Q,I,J,N) =>
Squares = vars({[Q[I,J1] : J1 in 1..N],
[Q[I1,J] : I1 in 1..N],
[Q[I1,J1] : I1 in 1..N, J1 in 1..N, I1-J1==I-J],
[Q[I1,J1] : I1 in 1..N, J1 in 1..N, I1+J1==I+J]}),
sum(Squares) #>= 1.
output(Q,N,Obj) =>
Pos = [P : I in 1..N, (nth(P,[Q[I,J] : J in 1..N],1)->true; P=0)],
printf("q = %w;%n",Pos),
printf("obj = %w;%n",Obj),
printf("%% method = \"SAT\";%n").