//
// Mike's model with the tree rooted at v_30
// This permits simpler code for symmetry breaking between clusters
//
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;
import choco.kernel.solver.ContradictionException;

public class Extremal31a { 

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


    Extremal31a(int e,int d, int D){
	System.out.println(d +" "+ D);
	this.n   = 31;
	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;i<n-1;i++)
	    for (int j=i+1;j<n;j++)
		A[j][i] = A[i][j] = makeIntVar("A_"+ i +"_"+ j,0,1);
	for (int i=0;i<n;i++) A[i][i] = constant(0);
	makeStar_6_4();
	for (int i=0,k=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++,k++)
		flatA[k] = A[i][j];
	for (int i=0,k =0;i<n-1;i++)
	    for (int j=n-1;j>i;j--,k++)
		instOrd[k] = A[i][j];
	model  = new CPModel();
	solver = new CPSolver();
    }

    void edge(int i,int j){A[i][j] = A[j][i] = constant(1);}
    void noEdge(int i,int j){A[i][j] = A[j][i] = constant(0);}

    void makeStar_6_4(){
	for (int j=24;j<=29;j++) edge(30,j);
	for (int j=0;j<4;j++){
	    edge(24,j+0);  edge(25,j+4);  edge(26,j+8);
	    edge(27,j+12); edge(28,j+16); edge(29,j+20);
	}
    }

    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 symmetryBreak(){
	for (int i=0;i<n-1;i++)
	    model.addConstraint(lexeq(A[i],A[i+1]));
    }

    void symmetryBreak(int lwb,int upb){
	for (int i=lwb;i<upb;i++)
	    model.addConstraint(lexeq(A[i],A[i+1]));
    }

    void pairBreak(int i,int j){model.addConstraint(lexeq(A[i],A[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 symmetryBreakPlus(int lwb,int upb){
	for (int i=lwb;i<upb;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 symmetryBreakPlusPlus(int lwb,int upb){
	for (int i=lwb;i<upb;i++){
	    for (int j=i+1;j<=upb;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 pairBreakPlus(int i,int 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)  throws ContradictionException {
	int n        = 31;
	int e        = Integer.parseInt(args[0]);    // number of edges
	int d        = Integer.parseInt(args[1]);    // lower bound of degree
	int D        = Integer.parseInt(args[2]);    // upper bound of degree
	String style = args[3];                      // sym, sym+, sym++
	Extremal31a G = new Extremal31a(e,d,D);

	G.edgeSum();
	if (style.equals("sym++")){
		G.symmetryBreakPlusPlus(0,3);
		G.symmetryBreakPlusPlus(4,7);
		G.symmetryBreakPlusPlus(8,11);
		G.symmetryBreakPlusPlus(12,15);
		G.symmetryBreakPlusPlus(16,19);
		G.symmetryBreakPlusPlus(20,23);
		G.pairBreakPlus(0,4);   G.pairBreakPlus(0,8);  G.pairBreakPlus(0,12); G.pairBreakPlus(0,16); G.pairBreakPlus(0,20);
		G.pairBreakPlus(4,8);   G.pairBreakPlus(4,12); G.pairBreakPlus(4,16); G.pairBreakPlus(4,20);
		G.pairBreakPlus(8,12);  G.pairBreakPlus(8,16); G.pairBreakPlus(8,20);
		G.pairBreakPlus(12,16); G.pairBreakPlus(12,20);
		G.pairBreakPlus(16,20);
	}
	else if (style.equals("sym+")){
		G.symmetryBreakPlus(0,3);
		G.symmetryBreakPlus(4,7);
		G.symmetryBreakPlus(8,11);
		G.symmetryBreakPlus(12,15);
		G.symmetryBreakPlus(16,19);
		G.symmetryBreakPlus(20,23);
		G.pairBreakPlus(0,4);  
		G.pairBreakPlus(4,8); 
		G.pairBreakPlus(8,12);
		G.pairBreakPlus(12,16);
		G.pairBreakPlus(16,20);
	}
	else if (style.equals("sym")){
		G.symmetryBreak(0,3);
		G.symmetryBreak(4,7);
		G.symmetryBreak(8,11);
		G.symmetryBreak(12,15);
		G.symmetryBreak(16,19);
		G.symmetryBreak(20,23);
		G.pairBreak(0,4);  
		G.pairBreak(4,8); 
		G.pairBreak(8,12);
		G.pairBreak(12,16);
		G.pairBreak(16,20);
	}
	G.degreeConstraints();

	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.setVarIntSelector(new StaticVarOrder(G.solver.getVar(G.instOrd)));
	G.solver.setValIntIterator(new DecreasingDomain()); 
	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.propagate();
	
	System.out.println();
	for (int i=0;i<n;i++){
	    System.out.print("    ");
	    for (int j=0;j<n;j++)
		if (i==j) System.out.print("0 ");
		else if (A[i][j].isInstantiated())
		    System.out.print(A[i][j].getVal() +" ");
		else System.out.print("? ");
	    System.out.println();
	}
	System.out.println();

	if(G.solver.solve()){
	    System.out.println();
	    for (int i=0;i<n;i++){
		System.out.print("    ");
		for (int j=0;j<n;j++)
		    if (i==j) System.out.print("0 ");
		    else if (A[i][j].isInstantiated())
			System.out.print(A[i][j].getVal() +" ");
		    else System.out.print("?");
		System.out.println();
	    }
	    System.out.println();
	}
	G.solver.printRuntimeSatistics();
	
    }
}