//
// Given v and e, how many {C3,C4}-free graphs are there?
//
import java.util.*;
import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.Model;
import choco.kernel.solver.Solver;
import choco.kernel.model.variables.integer.IntegerVariable;
import choco.cp.solver.search.integer.varselector.StaticVarOrder;
import choco.cp.solver.search.integer.valiterator.DecreasingDomain;
import choco.kernel.solver.variables.integer.IntDomainVar;

public class ExtremalAll03 { 

    int n;                      // number of vertices
    IntegerVariable [][] A;     // A[i][j] = 1 <-> adjacent(i,j);
    IntegerVariable [] flatA;   // A[][] flattened
    IntegerVariable [] instOrd; // instantiation order
    IntegerVariable e;          // number of edges
    CPModel model;
    CPSolver solver;


    ExtremalAll03(int n,int e){
	this.n  = n;
	A       = new IntegerVariable[n][n]; // A[i][j] == 1 <-> adjacent(i,j);
	flatA   = new IntegerVariable[n*(n-1)/2];
	instOrd = new IntegerVariable[n*(n-1)/2];
	this.e  = constant(e);
	for (int i=0,k=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++,k++)
		flatA[k] = A[j][i] = A[i][j] = makeIntVar("A_"+ i +"_"+ j,0,1);
	for (int i=0,k =0;i<n-1;i++)
	    for (int j=n-1;j>i;j--,k++)
		instOrd[k] = A[i][j];
	for (int i=0;i<n;i++) A[i][i] = constant(0);
	model  = new CPModel();
	solver = new CPSolver();
    }

    void edgeSum(){model.addConstraint(eq(sum(flatA),e));}

    void symmetryBreak(){
	for (int i=0;i<n-1;i++)
	    model.addConstraint(lexeq(A[i],A[i+1]));
    }
    //
    // NOTE: stronger as A[i] < A[j] for all i < j
    //

    void symmetryBreakPlus(){
	for (int i=0;i<n-1;i++){
	    IntegerVariable [] X = new IntegerVariable[n-2];
	    IntegerVariable [] Y = new IntegerVariable[n-2];
	    for (int j=0;j<i;j++) X[j] = A[i][j];
	    for (int j=i+2;j<n;j++) X[j-2] = A[i][j];
	    for (int j=0;j<i;j++) Y[j] = A[i+1][j];
	    for (int j=i+2;j<n;j++) Y[j-2] = A[i+1][j];
	    model.addConstraint(lexeq(X,Y));
	}
    }

    void symmetryBreakPlusPlus(){
	for (int i=0;i<n-1;i++){
	    for (int j=i+1;j<n;j++){
		IntegerVariable [] X = new IntegerVariable[n-1];
		IntegerVariable [] Y = new IntegerVariable[n-1];
		for (int k=0;k<j;k++) X[k] = A[i][k];
		for (int k=j+1;k<n;k++) X[k-1] = A[i][k];
		for (int k=0;k<i;k++) Y[k] = A[j][k];
		for (int k=i+1;k<n;k++) Y[k-1] = A[j][k];
		model.addConstraint(lexeq(X,Y));
	    }
	}
    }

    void display(){
	//System.out.println();
	for (int i=0;i<n;i++){
	    System.out.print("[");
	      for (int j=0;j<n-1;j++)
		  if (i==j) System.out.print("0,");
		  else System.out.print(solver.getVar(A[i][j]).getVal()+",");
	      if (i==n-1)
		  System.out.println("0]");
	      else 
		  System.out.println(solver.getVar(A[i][n-1]).getVal()+"]");
	}
	System.out.println();
	System.out.println();
    }
  
    public static void main(String[] args) {
      int n           = Integer.parseInt(args[0]);    // number of vertices
      int e           = Integer.parseInt(args[1]);    // number of edges
      ExtremalAll03 G = new ExtremalAll03(n,e);

      G.edgeSum();

      if (args[2].equals("sym")){
	  G.symmetryBreak();
	  //System.out.println("sym v="+ n);
      }
      else if (args[2].equals("sym+")){
	  G.symmetryBreakPlus();
	  //System.out.println("sym+ v="+ n);
      }
      else if (args[2].equals("sym++")){
	  G.symmetryBreakPlusPlus();
	  //System.out.println("sym++ v="+ n);
      }
      
      G.solver.read(G.model);

      IntDomainVar[][] A = new IntDomainVar[n][n];
      for (int i=0,k=0;i<n-1;i++)
	  for (int j=i+1;j<n;j++,k++){
	      A[i][j] = A[j][i] = G.solver.getVar(G.A[i][j]);
	  }
      G.solver.post(new NoTriangles(G.solver,G.solver.getVar(G.flatA),A,n));
      G.solver.post(new NoSquares(G.solver,G.solver.getVar(G.flatA),A,n));
      //G.solver.post(new NoPentagons(G.solver,G.solver.getVar(G.flatA),A,n));

      G.solver.setVarIntSelector(new StaticVarOrder(G.solver.getVar(G.instOrd)));
      G.solver.setValIntIterator(new DecreasingDomain()); 

      int count = 0;
      if (G.solver.solve()){
	  G.display();
	  count++;
	  while (G.solver.nextSolution()){G.display(); count++;}
	}
      //System.out.println(count);
      //G.solver.printRuntimeSatistics();
      
    }
}