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

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

    Extremal31_81_33(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];
	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];
	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=1;j<=6;j++) edge(0,j);
	for (int j=0;j<4;j++){
	    edge(1,j+7); edge(2,j+11); edge(3,j+15);
	    edge(4,j+19); edge(5,j+23); edge(6,j+27);
	}
	for (int j=7;j<31;j++) noEdge(0,j);
    }

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

    void degreeConstraints(){
	IntegerVariable five = constant(5);
	IntegerVariable six = constant(6);
	for (int i=7;i<31;i++) degree[i] = five;
	degree[7] = degree[8] = degree[9] = six;
	degree[11] = degree[12] = degree[13] = six;
	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]));
    }
    //
    // NOTE: basic
    //

    void codishSymmetryBreak(){
	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 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));
	    }
	}
    }

    void codishSymmetryBreakPlus(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));
	    }
	}
    }

    
    
    public static void main(String[] args)  throws ContradictionException {
	int n        = 31;
	int e        = 81;
	int d        = 5;
	int D        = 6;
	Extremal31_81_33 G = new Extremal31_81_33(e,d,D);

	G.edgeSum();
	G.codishSymmetryBreakPlus(7,9);
	G.codishSymmetryBreakPlus(11,13);
	G.codishSymmetryBreakPlus(15,18);
	G.codishSymmetryBreakPlus(19,22);
	G.codishSymmetryBreakPlus(23,26);
	G.codishSymmetryBreakPlus(27,30);
	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.flatA)));
	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++){
	    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 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++){
		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 if (A[i][j].isInstantiated())
			System.out.print(A[i][j].getVal());
		    else System.out.print("?");
		System.out.println();
	    }
	    System.out.println();
	}
	*/
	int count = 0;
	if(G.solver.solve()){
	    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 && A[i][j].isInstantiated() && A[i][j].getVal() == 1) {
			System.out.print(j +" ");
			count++;
			    }
		System.out.println(" deg: "+ G.solver.getVar(G.degree[i]).getVal());
	    }
	    System.out.println();
	}
	G.solver.printRuntimeSatistics();
	System.out.println(count);
	
    }
}