//
// 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 Temp {

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

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

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

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

     if (solver.solve().booleanValue()){
	 System.out.println(solver.getVar(d).getVal() +" "+ solver.getVar(D).getVal() +" "+ nodes +" "+ time);
	 Extremal02 G = new Extremal02(v,e,solver.getVar(d).getVal(),solver.getVar(D).getVal());
	 if(G.solver.solve()){G.display(); solved = true;}
	 nodes = nodes + G.solver.getNodeCount();
	 time = time + G.solver.getTimeCount();
	 while (!solved && solver.nextSolution().booleanValue()){
	     System.out.println(solver.getVar(d).getVal() +" "+ solver.getVar(D).getVal() +" "+ nodes +" "+ time);
	     G = new Extremal02(v,e,solver.getVar(d).getVal(),solver.getVar(D).getVal());
	     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);
  }
}