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 Exists { 

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


    Exists(int n,int e,int d,int D,int minGirth){
	this.n  = n;
	this.e  = e;
	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];
	degree  = makeIntVarArray("deg",n,d,D);
	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();
	edgeSum();
	degreeConstraints();
	//model.addConstraint(eq(d,degree[0]));
	//model.addConstraint(eq(D,degree[n-1]));
	codishSymmetryBreakPlus();
	solver.read(model);
	solverA = new IntDomainVar[n][n];
	for (int i=0,k=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++,k++){
	      solverA[i][j] = solverA[j][i] = solver.getVar(A[i][j]);
	  }
	solver.setValIntIterator(new DecreasingDomain()); 
	solver.setVarIntSelector(new StaticVarOrder(solver.getVar(instOrd)));
	solver.post(new MinGirth(solver,solver.getVar(flatA),solverA,n,minGirth));
    }

    void display(){
	System.out.println();
	for (int i=0;i<n;i++){
	    if (i<10) System.out.print(" ");
	    System.out.print(" "+ i +" ");
	      for (int j=0;j<n;j++)
		  if (i==j) System.out.print("0");
		  else System.out.print(solverA[i][j].getVal());
	      System.out.println();
	}
	System.out.println();
    }

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

    void degreeConstraints(){
	for (int i=0;i<n;i++) model.addConstraint(eq(degree[i],sum(A[i])));
	model.addConstraint(eq(2*e,sum(degree)));
    }

    void codishSymmetryBreakPlus(){
	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));
	    }
	}
    }
    
    public static void main(String[] args) {
	if (args.length == 0){
	    System.out.println("java Exists #vertices #edges minGirth [witness]");
	    return;
	}
      int n        = Integer.parseInt(args[0]);    // number of vertices
      int e        = Integer.parseInt(args[1]);    // number of edges
      int minGirth = Integer.parseInt(args[2]);    // minimum girth
      Exists G     = new Exists(n,e,0,n-1,minGirth);

      if(args.length == 4 && args[3].equals("witness"))
	  if (G.solver.solve()) G.display();
	  else System.out.println("no witness");
      else System.out.println(G.solver.solve());
      G.solver.printRuntimeSatistics();
    }
}