/*

n-queens problem in Comet.

From Pascal Van Hentenryck "The OPL Optimization Programming Language",
page 34.

This Comet model was created by Hakan Kjellerstrand (hakank@gmail.com)
Also, see my Comet page: http://www.hakank.org/comet

*/

// Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/

import cotfd;

int t0 = System.getCPUTime();

cout << "Number of Variables: ";
int n = cin.getInt();
range Domain = 1..n;

Solver<CP> m();
var<CP>{int} queens[Domain](m, Domain);

Integer num_solutions(0);

// exploreall<m> {
explore<m> {

forall(i in 1..n, j in 1..n : i < j) {
m.post(queens[i] != queens[j]);
m.post(queens[i] + i != queens[j] + j);
m.post(queens[i] - i != queens[j] - j);
}

} using {

labelFF(m);
num_solutions++;
cout << queens << endl;

}

cout << "\nnum_solutions: " << num_solutions << endl;

int t1 = System.getCPUTime();
cout << "time:      " << (t1-t0) << endl;
cout << "#choices = " << m.getNChoice() << endl;
cout << "#fail    = " << m.getNFail() << endl;
cout << "#propag  = " << m.getNPropag() << endl;