int: n; array [1..n] of var 1..n: q; % queen in column i is in row q[i] include "alldifferent.mzn"; constraint alldifferent(q); % distinct rows constraint alldifferent([ q[i] + i | i in 1..n]); % distinct diagonals constraint alldifferent([ q[i] - i | i in 1..n]); % upwards+downwards include "lex_lesseq.mzn"; % Symmetry breaking constraint symmetry_breaking_constraint( let { % Alternative Boolean model: % Map each position i,j to a Boolean telling us whether there is a queen at i,j array[1..n,1..n] of var bool: qb; } in % Channeling constraint forall (i,j in 1..n) ( qb[i,j] <-> (q[i]=j) ) % Lexicographic symmetry breaking constraints /\ lex_lesseq(array1d(qb), [ qb[j,i] | i,j in 1..n ]) /\ lex_lesseq(array1d(qb), [ qb[i,j] | i in reverse(1..n), j in 1..n ]) /\ lex_lesseq(array1d(qb), [ qb[j,i] | i in 1..n, j in reverse(1..n) ]) /\ lex_lesseq(array1d(qb), [ qb[i,j] | i in 1..n, j in reverse(1..n) ]) /\ lex_lesseq(array1d(qb), [ qb[j,i] | i in reverse(1..n), j in 1..n ]) /\ lex_lesseq(array1d(qb), [ qb[i,j] | i,j in reverse(1..n) ]) /\ lex_lesseq(array1d(qb), [ qb[j,i] | i,j in reverse(1..n) ]) ); % search solve :: int_search(q, first_fail, indomain_min) satisfy; output [ if fix(q[j]) == i then "Q" else "." endif ++ if j == n then "\n" else "" endif | i,j in 1..n]