/*

  Place number puzzle in Comet.

  http://ai.uwaterloo.ca/~vanbeek/Courses/Slides/introduction.pdf
  """
  Place numbers 1 through 8 on nodes
  - each number appears exactly once
  - no connected nodes have consecutive numbers
       2 - 5 
     / | X | \
   1 - 3 - 6 - 8
     \ | X | /
       4 - 7
  """

  Compare with my MiniZinc model http://www.hakank.org/minizinc/place_number.mzn

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

 */

import cotfd;
int t0 = System.getCPUTime();

int m = 32;
int graph[1..m, 1..2] = 
[
  [1,2],
  [1,3],
  [1,4],
  [2,1],
  [2,3],
  [2,5],
  [2,6],
  [3,2],
  [3,4],
  [3,6],
  [3,7],
  [4,1],
  [4,3],
  [4,6],
  [4,7],
  [5,2],
  [5,3],
  [5,6],
  [5,8],
  [6,2],
  [6,3],
  [6,4],
  [6,5],
  [6,7],
  [6,8],
  [7,3],
  [7,4],
  [7,6],
  [7,8],
  [8,5],
  [8,6],
  [8,7]
];

Solver<CP> cp();

int n = 8;
var<CP>{int} x[1..n](cp, 1..8);

Integer num_solutions(0);
exploreall<cp> {

  cp.post(alldifferent(x));

  forall(i in 1..m) 
    cp.post(abs(x[graph[i,1]]-x[graph[i,2]]) > 1);

  // symmetry breaking
  cp.post(x[1] < x[n]);

} using {
      
  label(cp);

  num_solutions := num_solutions + 1;
      
  cout << x << endl;

}

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