//
// Given a graph with v vertices and e edges what are the degrees of
// vertices such that the graph has no triangles and no squares?
// See D.K Garnick, Y.H. Harris Kwong & F. Lazebnik "Extremal Graphs without Three-Cycles
// or Four-Cycles". In particular Propositions 2.6 and 2.7
//
// v    = number of vertices
// e    = number of edges
// d    = minimum degree
// D    = maximum degree
// f(v) = maximum number of edges in a graph with v vertices that has no triangle or square
//
// Proposition 2.5:   v >= 1+D.d >= 1+d.d
// Proposition 2.7:   d >= e-f(v-1)
//                    D >= ceiling(2.e/v)
//
// This CP takes on the command line arguments v, e and f(v-1) and enumerates all graphical degree sequences
//

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.kernel.solver.ContradictionException;


public class ExtremalWithDegreeSequence {

    static int ceiling(int x,int y){
	int z = x/y;
	if (x%y > 0) z = z + 1;
	return z;
    }
    //
    //  ceiling(x/y)
    //

    static void swap(int i, int j, int[] x){
	int temp = x[i]; 
	x[i] = x[j];
	x[j] = temp;
    }

    static void sort(int[] x){
	Arrays.sort(x);
	int n = x.length;
	for (int i=0;i<n/2;i++)
	    swap(i,n-1-i,x);
    }
    //
    // sort in descending order
    //

    static boolean isGraphical(int[] degSeq){
	int n = degSeq.length;
	int[] d = Arrays.copyOf(degSeq,n);
	for (int i=0;i<n;i++){
	    sort(d);
	    //for (int k=0;k<n;k++) System.out.print(d[k] + " "); System.out.println();
	    int x = d[0];
	    for (int j=1;j<=x;j++)d[j] = d[j] - 1;
	    d[0] = 0;
	}
	for (int i=0;i<n;i++) if (d[i] != 0) return false;
	return true;
    }
  
  public static void main(String[] args) throws ContradictionException {

     Model model               = new CPModel();    
     int v                     = Integer.parseInt(args[0]);
     int e                     = Integer.parseInt(args[1]); 
     int f_v                   = Integer.parseInt(args[2]); 
     int x                     = ceiling(2*e,v);
     IntegerVariable d         = makeIntVar("d",0,v-1);
     IntegerVariable D         = makeIntVar("D",0,v-1);
     IntegerVariable [] degree = makeIntVarArray("deg",v,0,v-1);
     int[] degSeq              = new int[v];
 
     model.addConstraint(geq(D,d));
     model.addConstraint(geq(v,plus(mult(D,d),1)));
     model.addConstraint(geq(plus(1,mult(D,d)),plus(1,mult(d,d))));
     model.addConstraint(geq(d,e - f_v));
     model.addConstraint(geq(D,x));
     
     for (int i=0;i<v-1;i++) model.addConstraint(geq(degree[i],degree[i+1]));
     for (int i=0;i<v;i++) model.addConstraint(geq(degree[i],d));
     for (int i=0;i<v;i++) model.addConstraint(leq(degree[i],D));
     model.addConstraint(eq(2*e,sum(degree)));

     Solver solver = new CPSolver(); 
     solver.read(model);    

     //System.out.println(solver.solve(true));
     //System.out.println(solver.getNbSolutions());
     //solver.printRuntimeSatistics();

     boolean solved = false;
     int nodes = 0;
     int time = 0;

     if (solver.solve().booleanValue()){
	 for (int i=0;i<v;i++) degSeq[i] = solver.getVar(degree[i]).getVal();
	 if (isGraphical(degSeq)){
	     for (int i=0;i<v;i++) System.out.print(" "+ degSeq[i]);
	     System.out.println("   "+ solver.getNodeCount() +"  "+ nodes +" "+ time);
	     Extremal02 G = new Extremal02(v,e,degSeq);
	     if(G.solver.solve()){G.display(); solved = true;}
	     nodes = nodes + G.solver.getNodeCount();
	     time = time + G.solver.getTimeCount();
	 }
	 while (!solved && solver.nextSolution().booleanValue()){ 
	     for (int i=0;i<v;i++) degSeq[i] = solver.getVar(degree[i]).getVal();
	     if (isGraphical(degSeq)){
		 for (int i=0;i<v;i++) System.out.print(" "+ degSeq[i]);
		 System.out.println("   "+ solver.getNodeCount() +"  "+ nodes +" "+ time);
		 Extremal02 G = new Extremal02(v,e,degSeq);
		 if(G.solver.solve()){G.display(); solved = true;}
		 nodes = nodes + G.solver.getNodeCount();
		 time = time + G.solver.getTimeCount();
	     }
	 }
     }
     nodes = nodes + solver.getNodeCount();
     time = time + solver.getTimeCount();
     System.out.println("nodes: "+ nodes +"  time: "+ time);
  }
}