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.model.constraints.Constraint;
import choco.cp.solver.search.integer.varselector.*;
import java.util.*;

public class Skipper {

    Model model;
    int id; // identification number
    int n; // number of skippers, controls domains size for a time slot
    int m; // size of a round
    int matches; // number of matches
    int rounds; // number of rounds
    int timeSlots;
    int boats;
    IntegerVariable[] timeSlot; // array of timeslots for a skipper
    IntegerVariable[] isMinusTwo; //
    IntegerVariable[] isMinusOne; //
    IntegerVariable[] isGeqZero; //
    IntegerVariable[] state; // there is a state for each round for the skipper
    IntegerVariable[] decVar; // decision variables
    IntegerVariable[] change; // when a boat change takes place
    IntegerVariable[][] position; // position[i][j] = 1 <-> there is a match in position i in round j
    IntegerVariable[] imbalance; // imbalance[i] is how far from perfect balance in position i
    IntegerVariable maxImbalance; // maximum imbalance for this skipper
    IntegerVariable changes; // number of boat changes made
    final int FIRST = 1;
    final int MID   = 2;
    final int LAST  = 3;
    final int BYE   = 4;
    final int END   = 5;

    Skipper(Model model,int id,int n,int m,int boats){
	this.model  = model;
	this.id     = id;
	this.n      = n;
	this.m      = m;
	this.boats  = boats;
	matches     = n*(n-1)/2;
	rounds      =  (int)Math.ceil((double)matches/(double)m);
	timeSlots   = rounds * m;
	timeSlot    = makeIntVarArray("timeSlot_"+ id,timeSlots,-2,n-1);
	isMinusTwo  = makeIntVarArray("isMinusTwo",timeSlots,0,1);
	isMinusOne  = makeIntVarArray("isMinusOne",timeSlots,0,1);
	isGeqZero   = makeIntVarArray("isGeqZero",timeSlots,0,1);
	state       = makeIntVarArray("state_"+ id,rounds,1,5);
	decVar      = new IntegerVariable[timeSlots + rounds];
	change      = makeIntVarArray("change",rounds-1,0,1);
	changes     = makeIntVar("changes",0,n-1);
	position    = makeIntVarArray("position",m,rounds,0,1);
	imbalance   = makeIntVarArray("imbalance",m,0,n-1);
	maxImbalance = makeIntVar("maxImbalance",0,n-1);

	for (int i=0;i<timeSlots;i++){
	    model.addConstraint(ifOnlyIf(eq(isMinusTwo[i],1),eq(timeSlot[i],-2)));
	    model.addConstraint(ifOnlyIf(eq(isMinusOne[i],1),eq(timeSlot[i],-1)));
	    model.addConstraint(ifOnlyIf(eq(isGeqZero[i],1),geq(timeSlot[i],0)));
	}	    
	//
	// Channeling between the array of timeslots and what is in each timeslot
	// isMinustTwo, isMinusOne, isGeqZero are used to compute the state of a round
	//
	// NOTE: we will also use the transpose of isGeqZero to constrain the schedule
	//       such that 2 or 0 skippers are in a match in any given timeslot.
	// NOTE: we can also use this information to sort rounds so that
	//       shortest rounds are carried out last
	// NOTE: if state[i] is a bye and state[i+1] is not a bye 
	//       then we have a boat change for this skipper at timeslot i+1
	//

	for (int round=0;round<rounds;round++){
	    end(round);
	    bye(round);
	    first(round);
	    mid(round);
	    last(round);
	}
	//
	// Channel between the implicit rounds in the timeslots
	// and the state of each round
	//

	////////////////
	//            //
	//   RULES    //
	//            //
	////////////////

	// STATE 5: end
	for (int round=0;round<rounds-1;round++) 
	  model.addConstraint(implies(eq(state[round],END),eq(state[round+1],END)));
	//
	// if it's the end it really is the end
	//

	// STATE 4: bye
	if (boats < n)
	    for (int round=0;round<rounds-1;round++) 
		model.addConstraint(implies(eq(state[round],BYE),and(neq(state[round+1],END),neq(state[round+1],FIRST))));
	//
	// if it's a bye then next state isn't the end (for DFM) and isn't first (rule 12)
	//


	// STATE 3: last in round
	for (int round=0;round<rounds-1;round++) 
	    model.addConstraint(implies(eq(state[round],LAST),neq(state[round+1],FIRST)));
	//
	// if you're last, next state you cannot be first (rule 4)
	//

	// STATE 3: last in round
	if (boats < n)
	    for (int round=0;round<rounds-1;round++) 
		model.addConstraint(implies(eq(state[round],LAST),neq(state[round+1],BYE)));
	//
	// if you're last, next state cannot be a bye (rule 11)
	//

	// Non-accepting state: bye
	model.addConstraint(neq(state[rounds-1],BYE));
	//
	// last state is not a bye
	//

	// Illegal transition from start: to end
	model.addConstraint(neq(state[0],END));
	//
	// start state is not the end
	//

	/////////////////////////////////////////////////////////////
	//
	// global cardinality on a skippers timeslots
	// The skipper must compete once against every other skipper
	// and does not compete against himself
	// Here we fake that by disallowing n/3
	//
	//////////////////////////////////////////////////////////////
	int[] values = new int[n];
	int[] lwb    = new int[n];
	int[] upb    = new int[n];
	Arrays.fill(lwb,1);
	Arrays.fill(upb,1);
	for (int i=0;i<n;i++) values[i] = i;
	lwb[id] = upb[id] = 0; // cannot compete with self
	model.addConstraint(globalCardinality(timeSlot,values,lwb,upb));

	//////////////////////////////////////////////////////////////
	//
	// Set up decision variables
	//
	//////////////////////////////////////////////////////////////
	for (int i=0;i<timeSlots;i++) decVar[i] = timeSlot[i];
	for (int round=0;round<rounds;round++) decVar[timeSlots + round] = state[round];

	//////////////////////////////////////////////////////////////
	//
	// changes!
	//
	/////////////////////////////////////////////////////////////
	for (int round=0;round<rounds-1;round++)
	    model.addConstraint(ifOnlyIf(eq(change[round],1),and(eq(state[round],BYE),lt(state[round+1],BYE))));
	model.addConstraint(eq(changes,sum(change)));

	//////////////////////////////////////////////////////////////
	//
	// Criteria 6: balance
	//
	/////////////////////////////////////////////////////////////
	for (int round=0;round<rounds;round++)
	    for (int pos=0;pos<m;pos++){
		int t = round*m + pos;
		model.addConstraint(ifOnlyIf(eq(1,position[pos][round]),geq(timeSlot[t],0)));
	}
	for (int i=0;i<m;i++) model.addConstraint(eq(imbalance[i],abs(minus(sum(position[i]),(n-1)/m))));
	model.addConstraint(eq(maxImbalance,max(imbalance)));
    }

    void end(int round){
	IntegerVariable[] x = new IntegerVariable[m];
	for (int i=0;i<m;i++) x[i] = isMinusTwo[round*m+i];
	model.addConstraint(ifOnlyIf(eq(state[round],5),eq(sum(x),m)));
    }
    //
    // A round is an end state if all its timeslots are -2
    //
    
    void bye(int round){
	IntegerVariable[] x = new IntegerVariable[m];
	for (int i=0;i<m;i++) x[i] = isMinusOne[round*m+i];
	model.addConstraint(ifOnlyIf(eq(state[round],4),eq(sum(x),m)));
    }
    //
    // A round is a bye if all its timeslots are -1
    //

    void first(int round){
	IntegerVariable[] x = new IntegerVariable[m];
	for (int i=0;i<m;i++) x[i] = isMinusOne[round*m+i];
	model.addConstraint(ifOnlyIf(eq(state[round],1),and(eq(sum(x),m-1),eq(1,isGeqZero[round*m]))));
    }
    //
    // A round is first, if the first timeslot is greater than or equal to zero, i.e. it is another skipper
    // and all other timeslots in the round (m-1 of them) are -1
    //	

    void mid(int round){
	IntegerVariable[] x = new IntegerVariable[m];
	for (int i=0;i<m;i++) x[i] = isMinusOne[round*m+i];
	IntegerVariable[] y = new IntegerVariable[m];
	for (int i=0;i<m;i++) y[i] = isGeqZero[round*m+i];
	model.addConstraint(ifOnlyIf(eq(state[round],2),and(eq(sum(x),m-1),eq(sum(y),1),eq(isMinusOne[round*m],1),eq(isMinusOne[round*m + m-1],1))));
    }	
    //
    // A round is a mid if the first and last timeslots are -1, there are m-1 timeslots that are -1
    // and there is a single timeslot that is greater than or equal to zero, i.e. another skipper
    //

    void last(int round){
	IntegerVariable[] x = new IntegerVariable[m];
	for (int i=0;i<m;i++) x[i] = isMinusOne[round*m+i];
	model.addConstraint(ifOnlyIf(eq(state[round],3),and(eq(sum(x),m-1),eq(1,isGeqZero[round*m +m-1]))));
    }	
    //
    // A round is last if it has m-1 timeslots that are -1 and the last timeslot in the
    // round is a skipper (>= 0)
    //

    public void output(Solver solver){
	System.out.print(id +": ");
	for (int round=0;round<rounds;round++){
	    int i = solver.getVar(state[round]).getVal();
	    String s = "X ";
	    if (i==1) s = "F ";
	    if (i==2) s = "M ";
	    if (i==3) s = "L ";
	    if (i==4) s = "B ";
	    if (i==5) s = "E ";
	    System.out.print(s);
	}
	System.out.print(" changes: "+ solver.getVar(changes).getVal());
	System.out.println();
    }

    public void show(Solver solver){
	System.out.print(id +": ");
	for (int round=0;round<rounds;round++){
	    System.out.print(solver.getVar(state[round]).pretty() +" ");
	}
	System.out.println();
    }
    
    public static void main(String[] args) {	
	int n          = Integer.parseInt(args[0]); // number of rounds
	int boats      = Math.min(n,Integer.parseInt(args[1])); // number of boats
	int m          = boats/2; // size of a round
	int matches    = n*(n-1)/2;
	int rounds     = (int)Math.ceil((double)matches/(double)m);
	int timeSlots  = rounds * m;
	Model model    = new CPModel();     
	Skipper skip   = new Skipper(model,0,n,m,boats);
        Solver solver  = new CPSolver(); 

	solver.read(skip.model);   
	solver.setVarIntSelector(new MinDomain(solver,solver.getVar(skip.decVar)));

	System.out.println("blip");
	
	if (solver.solve().booleanValue()){
	    for (int round=0;round<rounds;round++){
		for (int i=0;i<m;i++){
		    int x = solver.getVar(skip.timeSlot[round*m+i]).getVal();
		    if (x == -2) System.out.print("*");
		    if (x == -1) System.out.print("-");
		    if (x >= 0) System.out.print(x);
		}
		System.out.print(" ");
	    }
	    System.out.println();
	    while (solver.nextSolution().booleanValue()){
		for (int round=0;round<rounds;round++){
		    for (int i=0;i<m;i++){
			int x = solver.getVar(skip.timeSlot[round*m+i]).getVal();
			if (x == -2) System.out.print("*");
			if (x == -1) System.out.print("-");
			if (x >= 0) System.out.print(x);
		    }
		    System.out.print(" ");
		}
		System.out.println();
	    }
	}
    }
}