//
// For latex output
//
import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.kernel.model.Model;
import choco.kernel.model.variables.integer.IntegerVariable;
import choco.cp.solver.CPSolver;
import choco.kernel.solver.Solver;
import choco.kernel.solver.variables.integer.IntDomainVar;
import choco.cp.solver.search.integer.varselector.MinDomain;

public class Note {

    Model model;
    Solver solver;
    int n;                        // skippers
    int m;                        // boats
    int matches;                  // number of matches, all pairs
    int boatPairs;                // all pairs of boats
    int flights;                  // a flight is up to m boats
    IntegerVariable[][] match;    // match[i][j] = k <-> skippers i and j are in a match in flight k
    IntegerVariable[][] tMatch;   // transpose of match
    IntegerVariable[] fMatch;     // flattened match
    IntegerVariable[] flightSize; // maximum number of pairs in a flight, i.e. boatPairs

    Note (int n,int m) {
	this.n     = n;
	this.m     = m;
	matches    = n*(n-1)/2;
	boatPairs  = m/2;
	flights    = (int)Math.ceil((double)matches/(double)boatPairs);
	model      = new CPModel();
	solver     = new CPSolver();
	match      = new IntegerVariable[n][n];
	tMatch     = new IntegerVariable[n][n];	
	fMatch     = new IntegerVariable[matches];
	flightSize = makeIntVarArray("size",flights,0,boatPairs);

	for (int i=0,k=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++,k++){
		match[i][j] = match[j][i] = makeIntVar("match["+ i +"]["+ j +"]",1,flights);
		fMatch[k] = match[i][j];
	    }
	for (int i=0;i<n;i++) match[i][i] = constant(flights+1+i);

	for (int i=0;i<n;i++)
	    for (int j=0;j<n;j++)
		tMatch[i][j] = match[j][i];
	/*
	for (int i=0;i<n;i++)
	    for (int j=0;j<n;j++)
		System.out.println(i +" "+ j +" -> "+ match[i][j]);
	*/

	for (int i=0;i<n;i++) model.addConstraint(allDifferent(match[i]));
	//for (int i=0;i<n;i++) model.addConstraint(allDifferent(tMatch[i]));

	for (int i=1;i<flights;i++)
	    model.addConstraint(occurrence(i,flightSize[i-1],fMatch));
	//
	// each flight to have no more than boatPairs matches
	//

	for (int i=0;i<flights-1;i++)
	    model.addConstraint(geq(flightSize[i],flightSize[i+1]));
	//
	// attempt at symmetry breaking
	//

	model.addConstraint(eq(sum(flightSize),matches));

	solver.read(model);

	solver.setVarIntSelector(new MinDomain(solver,solver.getVar(fMatch)));
	//
	// decision variables are matches (flattened into fMatch)
    }

    boolean solve(){return solver.solve();}

    void result(){
	//System.out.println(n +" skippers  "+ m +" boats  "+ matches +" matches  "+ flights +" flights  "+ boatPairs +" boatPairs");
	for (int flight=1;flight<=flights;flight++){
	    System.out.print(flight +" & ");
	    for (int i=0;i<n-1;i++)
		for (int j=i+1;j<n;j++)
		    if (solver.getVar(match[i][j]).getVal() == flight) System.out.print(" ("+ (i+1) +","+ (j+1) +")");
	    System.out.println(" \\\\ ");
	}
    }

    void stats(){
	System.out.println("nodes: "+ solver.getNodeCount() +"   cpu: "+ solver.getTimeCount());
    }
     
    public static void main(String args[]) {
	int n = Integer.parseInt(args[0]);
	int m = Integer.parseInt(args[1]);
	Note bap = new Note(n,m);
	System.out.println(bap.solve());
	bap.stats();
	bap.result();
    }
}