### solution 1: tests possibility of placing n queens on n*n board ### idea: x[i] means the id of column of queen on i-th row, constraints requires that no two variables have the same value (c1) and that difference of columns is different of difference of rows, avoiding two queens to be on the same diagonal (c2). Absolute values must be used, they are linearized by the system. ### The slowest one! param n := 20; param queens := n; set C := { 1 .. queens }; set P := { in C*C with i < j }; var x[C] integer >= 1 <= queens; subto c1 : forall in P do vabs ( x[i] - x[j] ) >= 1; subto c2 : forall in P do vabs ( vabs ( x [i] - x [j] ) - abs ( i - j ) ) >= 1; ### end of solution 1 ### solution 2: maximizes number of queens on column*column board ### idea: binary variable for each square on board, check numbers in all rows, cols and diagonals ### The fastest one! #param columns := 20 ; #set C := { 1 .. columns } ; #set CxC := C*C ; #var x [ CxC ] binary ; #maximize queens : sum in CxC : x[ i,j ] ; #subto row: forall in C do #sum in CxC: x[i,j] <= 1; #subto col: forall in C do #sum in CxC: x[i,j] <= 1; #subto diag_row_do: #forall in C: #sum in CxC with m-i == n-1: x[m,n] <= 1; #subto diag_row_up: #forall in C: #sum in CxC with m-i == 1-n: x[m,n] <=1; #subto diag_col_do: forall in C: #sum in CxC with m-1 == n-j: x[m,n] <= 1; #subto diag_col_up: forall in C: #sum in CxC with card(C) -m == n-j: x[m,n] <= 1; ### end of solution 2 ### solution 3: maximizes number of queens on column*column board ### idea: for every square, the set of forbidden (tabooized) squares is defined. If there is queen on square [i,j], there cannot be a queen on squares that are tabooized for [i,j]. ### three different ways of utilizing tabooized squares are proposed. 3a is the fastest, almost as fast as solution 2, 3b and 3c are a bit slower, however, still faster than solution 1. #param columns := 20 ; #set C := { 1 .. columns } ; #set CxC := C*C ; #var x [ CxC ] binary ; #maximize queens : sum in CxC : x[ i,j ] ; #set TABOO[ in CxC ] := { in CxC with (m != i or n != j ) #and (m == i or n == j or abs (m - i) == abs ( n-j ) ) } ; ## solution 3a: using vif function (solver has to transform it), n^2 constraints #subto c1 : forall in CxC do vif x[i,j] == 1 then #sum in TABOO[i,j] : x[m,n] <= 0 end ; ## solution 3b: function vif is "linearized" using simple trick, n^2 constraints #subto c2: forall in CxC do #card (TABOO[i,j])*x[i,j] + sum in TABOO[i,j] : x[m,n] <= card(TABOO[i,j]); ## solution 3c: there cannot be queens on a square and an associated tabooized square, O(n^3) constraints #subto c3: #forall in CxC: #forall in TABOO[i,j]: x[i,j] + x[m,n] <= 1;