### 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;
*