//
// Are there n distinct integers in the range 1 to m such
// that the difference between any pair is not 5, not 6 and not 11?
// First question was for n=75 and m=230
// Second, prove false for n=76 and m=230
//
// Might also try (5,5) (10,21) (15,37) ... (25,69) (30,90)
//
// You might see a pattern and derive some maths, i.e. use CP to guide a proof
//
import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.Model;
import choco.cp.solver.search.integer.varselector.MinDomain;
import choco.kernel.solver.Solver;
import choco.kernel.model.variables.integer.IntegerVariable;
import java.util.*;

public class Select75 {    
  
  public static void main(String[] args) {

      Model model                = new CPModel();
      Solver solver              = new CPSolver(); 
      int n                      = Integer.parseInt(args[0]); // 75
      int m                      = Integer.parseInt(args[1]); // 230
      IntegerVariable tick[]     = new IntegerVariable[n];
      IntegerVariable diff[][]   = new IntegerVariable[n][n];

      for (int i=0;i<n;i++) 
	  tick[i] = makeIntVar("tick[" + i + "]",1,m);

      for (int i=0;i<n-1;i++)
	  for (int j=i+1;j<n;j++){
	      diff[i][j] = makeIntVar("diff[" + i + "," + j + "]",1,m-1);
	      diff[j][i] = diff[i][j];
	      model.addConstraint(neq(diff[i][j],5));
	      model.addConstraint(neq(diff[i][j],6));
	      model.addConstraint(neq(diff[i][j],11));
	  }

      for (int i=0;i<n-1;i++)
	  for (int j=i+1;j<n;j++)
	      model.addConstraint(eq(diff[i][j],abs(minus(tick[j],tick[i]))));
      // get the difference between pairs of ticks

      
      model.addConstraint(allDifferent(tick));
      // all ticks are different!

      for (int i=0;i<n-1;i++) 
	  model.addConstraint(lt(tick[i],tick[i+1]));
      //
      // symmetry break
      //

      solver.read(model); 
      solver.setVarIntSelector(new MinDomain(solver,solver.getVar(tick)));
      System.out.println(solver.solve(false)); 
      System.out.println("nodes: "+ solver.getNodeCount() +"  cpu: "+ solver.getTimeCount());

      for (int i=0;i<n;i++)
	  System.out.print(solver.getVar(tick[i]).getVal() + " ");

  }
}