//
// 0/1 encoding using x[i][j] = 1 <-> i \in V1 and j \in V2 and they map
//
import java.io.*;
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.variables.integer.IntDomainVar;
import choco.kernel.solver.ContradictionException;
import choco.cp.solver.search.integer.varselector.StaticVarOrder;
import choco.cp.solver.search.integer.varselector.MinDomain;
import choco.cp.solver.search.integer.varselector.DomOverDeg;
import choco.cp.solver.search.integer.valiterator.DecreasingDomain;

public class MCIScp2 extends MCIS {

    Model model;  
    Solver solver; 
    IntegerVariable[][] x;
    IntegerVariable[][] transX;
    IntegerVariable[] flatX;
    IntegerVariable size;

     public MCIScp2(int[][] A1,int[][] A2){
	super();
        startTime  = System.currentTimeMillis();
	timeout    = false;
	timeLimit  = Integer.MAX_VALUE;
	n1         = A1.length;
	n2         = A2.length;
	model      = new CPModel();
	solver     = new CPSolver();
	model      = new CPModel();
	solver     = new CPSolver();
	x          = new IntegerVariable[n1][n2]; //x[i][j] = 1 <-> vertex i in G1 maps to vertex j in G2
	transX     = new IntegerVariable[n2][n1]; // transpose of x
	flatX      = new IntegerVariable[n1*n2];  // flattened x
	size       = makeIntVar("size",1,Math.min(n1,n2));
	for (int i=0,k=0;i<n1;i++)
	    for (int j=0;j<n2;j++,k++)
		flatX[k] = transX[j][i] = x[i][j] = makeIntVar("x_"+i+"_"+j,0,1);
	for (int i=0;i<n1-1;i++)
	    for (int j=i+1;j<n1;j++)
		for (int k=0;k<n2-1;k++)
		    for (int l=k+1;l<n2;l++)
			if (A1[i][j] != A2[l][k]){
			    model.addConstraint(lt(plus(x[i][l],x[j][k]),2));
			    model.addConstraint(lt(plus(x[i][k],x[j][l]),2));
			}
	for (int i=0;i<n1;i++) model.addConstraint(leq(sum(x[i]),1)); // map to a single vertex	
	for (int i=0;i<n2;i++) model.addConstraint(leq(sum(transX[i]),1)); // as above
	model.addConstraint(eq(size,sum(flatX)));	
	solver.read(model);
	solver.setVarIntSelector(new DomOverDeg(solver,solver.getVar(flatX)));
	solver.setValIntIterator(new DecreasingDomain()); // accept then reject
	long buildTime = System.currentTimeMillis() - startTime;
     }

     void solve(){
	searchTime = System.currentTimeMillis();
	solver.maximize(solver.getVar(size),false);
	searchTime = System.currentTimeMillis() - searchTime;
	totalTime  = System.currentTimeMillis() - startTime;
	timeout    = (int)totalTime >= timeLimit; // did we get a timeout?
    }

    void setTimeLimit(int timeLimit){
	this.timeLimit = timeLimit - (int)(System.currentTimeMillis() - startTime);
	solver.setTimeLimit(timeLimit);
    }

    void display(){	
	if (timeout) 
	    System.out.print(-solver.getVar(size).getVal() + " "); // negative size
	else
	    System.out.print(solver.getVar(size).getVal() + " ");
	System.out.println(solver.getNodeCount() +" "+ buildTime +" "+ searchTime +" "+ totalTime);
	if (!timeout)
	    for (int i=0;i<n1;i++)
		for (int j=0;j<n2;j++)
		    if (solver.getVar(x[i][j]).getVal() == 1) System.out.println(i +" "+ j);
    }

    public static void main(String[] args) throws IOException {
	int[][] A1   = readDIMACS(args[0]);
	int[][] A2   = readDIMACS(args[1]);
	MCIScp2 mcis = new MCIScp2(A1,A2);
	if (args.length > 2) mcis.setTimeLimit(1000 * Integer.parseInt(args[2]));
	mcis.solve();
	mcis.display();
    }
}