//
// By Ciaran McCreesh, November 2012
//
import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.cp.solver.search.integer.varselector.StaticVarOrder;
import choco.cp.solver.search.integer.varselector.MinDomain;
import choco.kernel.model.Model;
import choco.kernel.solver.Solver;
import choco.kernel.model.variables.integer.IntegerExpressionVariable;
import choco.kernel.model.variables.integer.IntegerVariable;
import choco.kernel.model.constraints.Constraint;
import choco.kernel.solver.ContradictionException;

public class Knights
{
    static Constraint validMove(IntegerVariable i, IntegerVariable j, IntegerVariable size)
    {
        IntegerExpressionVariable x_i = div(i, size);
        IntegerExpressionVariable y_i = mod(i, size);
        IntegerExpressionVariable x_j = div(j, size);
        IntegerExpressionVariable y_j = mod(j, size);
        return or(
                (and(eq(x_j, plus(x_i, +1)), eq(y_j, plus(y_i, +2)))),
                (and(eq(x_j, plus(x_i, +2)), eq(y_j, plus(y_i, +1)))),
                (and(eq(x_j, plus(x_i, +2)), eq(y_j, plus(y_i, -1)))),
                (and(eq(x_j, plus(x_i, +1)), eq(y_j, plus(y_i, -2)))),
                (and(eq(x_j, plus(x_i, -1)), eq(y_j, plus(y_i, -2)))),
                (and(eq(x_j, plus(x_i, -2)), eq(y_j, plus(y_i, -1)))),
                (and(eq(x_j, plus(x_i, -2)), eq(y_j, plus(y_i, +1)))),
                (and(eq(x_j, plus(x_i, -1)), eq(y_j, plus(y_i, +2)))));
    }

    public static void main(String[] args) throws ContradictionException
    {
        Model model = new CPModel();

        // Arguments: problem size, and whether or not we want a circuit.
        int size = Integer.parseInt(args[0]);
        boolean circuit = Boolean.parseBoolean(args[1]);

        // Our tour is t0 -> t1 -> t2 -> ... -> t(size^2 - 1). Values of t are
        // positions on the board, which we number from (0 .. size^2 - 1).
        IntegerVariable[] cycle = makeIntVarArray("t", size * size, 0, size * size - 1);
        model.addConstraint(allDifferent(cycle));

        // If we're looking for a circuit, WLOG we can start at the top left.
        if (circuit)
            model.addConstraint(eq(cycle[0], 0));

        // div doesn't work with an int as the second argument. It's fixed in Choco 2.1.5.
        IntegerVariable sizeAsIntegerVariable = makeIntVar("size", size, size);

        // t(n) -> t(n+1) must be a valid move. If we're looking for a circuit,
        // t(size^2 - 1) -> t0 needs to be a valid move too.
        for (int s = 0 ; s < (circuit ? (size * size) : (size * size) - 1) ; ++s)
            model.addConstraint(validMove(cycle[s], cycle[(s + 1) % (size * size)], sizeAsIntegerVariable));

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

        // This is terrible.
        solver.setVarIntSelector(new MinDomain(solver, solver.getVar(cycle)));

        if (solver.solve(false)) {
            for (int s = 0 ; s < size ; ++s)
                for (int t = 0 ; t < size ; ++t)
                    System.out.printf("(%d, %d) -> ",
                            solver.getVar(cycle[s * size + t]).getVal() / size,
                            solver.getVar(cycle[s * size + t]).getVal() % size);

            if (circuit)
                System.out.printf("(%d, %d)\n",
                        solver.getVar(cycle[0]).getVal() / size,
                        solver.getVar(cycle[0]).getVal() % size);

            System.out.println();
        } else {
            System.out.println("No solution");
        }
        solver.printRuntimeSatistics();
    }
}