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

    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;


    Extremal24(int e,int d, int D){
	this.n   = 24;
	this.e   = e;
	model    = new CPModel();
	solver   = new CPSolver();
	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_5_3();
	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];
    }

    void edge(int i,int j){model.addConstraint(eq(1,A[i][j]));}
    void noEdge(int i,int j){model.addConstraint(eq(0,A[i][j]));}

    void makeStar_5_3(){
	for (int j=1;j<=5;j++) edge(0,j);
	for (int j=1;j<=3;j++){
	    edge(1,j+5); edge(2,j+8); edge(3,j+11);
	    edge(4,j+14); edge(5,j+17);
	}
    }

    void edgeSum(){model.addConstraint(eq(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)));

	model.addConstraint(eq(4,degree[1]));
	model.addConstraint(eq(4,degree[2]));
	model.addConstraint(eq(4,degree[3]));
	model.addConstraint(eq(4,degree[4]));
	model.addConstraint(eq(4,degree[5]));
	/*
	for (int i=6;i<=18;i=i+3){
	    model.addConstraint(leq(degree[i],degree[i+1]));
	    model.addConstraint(leq(degree[i+1],degree[i+2]));
	}	    
	model.addConstraint(leq(degree[21],degree[22]));
	model.addConstraint(leq(degree[22],degree[23]));
	*/
    }

    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));
	    }
	}
    }

    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));
    }

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


    
    
    public static void main(String[] args)  throws ContradictionException {
	int n        = 24;
	int e        = 54; 
	int d        = 4; 
	int D        = 5; 
	Extremal24 G = new Extremal24(e,d,D);

	G.edgeSum();
	G.degreeConstraints();

	G.codishSymmetryBreakPlus(6,8);
	G.codishSymmetryBreakPlus(9,11);
	G.codishSymmetryBreakPlus(12,14);
	G.codishSymmetryBreakPlus(15,17);
	G.codishSymmetryBreakPlus(18,20);

	//G.codishSymmetryBreakPlus(1,3);

	G.codishSymmetryBreakPlus(21,23);
	
	G.pairBreakPlus(6,6,9);
	G.pairBreakPlus(6,9,12);
	G.pairBreakPlus(6,12,15);
	G.pairBreakPlus(6,15,18);
	
	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.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(count++);
	    while (G.solver.nextSolution()) System.out.println(count++);
	}
	G.solver.solve(true);
	System.out.println("nbSol: "+ G.solver.getNbSolutions());
	*/

	G.solver.printRuntimeSatistics();
    }
}