//
// Maximum Common Induced Subgraph (MCIS)
// Given graphs G1 and G2 deliver the largest
// common subgraph with the maximum number of vertices
// This is a mapping of a subset of vertices in G1 to a subset 
// of vertices in G2, respecting connectivity
//

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.cp.solver.search.integer.varselector.MinDomain;

public class MCIScp1 extends MCIS {
    Model model;  
    Solver solver; 
    IntegerVariable[] x;
    IntegerVariable[] penalty;
    IntegerVariable cost;
    
    public MCIScp1(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();
	x          = new IntegerVariable[n1];
	penalty    = makeIntVarArray("penalty",n1,0,1);
	cost       = makeIntVar("cost",Math.max(0,n1-n2),n1);

	for (int i=0;i<n1;i++){
	    int[] domain = new int[n2+1];
	    for (int j=0;j<n2;j++) domain[j] = j;
	    domain[n2] = n2+i; // to make better use of value ordering.
	    x[i] = makeIntVar("x_"+i,domain);
	}

	model.addConstraint(allDifferent(x));

	for (int i=0;i<n1-1;i++)
	    for (int j=i+1;j<n1;j++)
		for (int v=0;v<n2-1;v++)
		    for (int w=v+1;w<n2;w++)
			if (A1[i][j] != A2[v][w]){
			    model.addConstraint(or(neq(x[i],v),neq(x[j],w)));
			    model.addConstraint(or(neq(x[i],w),neq(x[j],v)));
			}
	
	for (int i=0;i<n1;i++) model.addConstraint(ifOnlyIf(geq(x[i],n2),eq(penalty[i],1)));

	model.addConstraint(eq(cost,sum(penalty)));
	
	solver.read(model);
	solver.setVarIntSelector(new MinDomain(solver,solver.getVar(x)));
	buildTime = System.currentTimeMillis() - startTime;
    }

    void solve(){
	searchTime = System.currentTimeMillis();
	solver.minimize(solver.getVar(cost),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(-(n1-solver.getVar(cost).getVal()) + " "); // negative size
	else
	    System.out.print(n1-solver.getVar(cost).getVal() + " ");
	System.out.println(solver.getNodeCount() +" "+ buildTime +" "+ searchTime +" "+ totalTime);
	if (!timeout)
	    for (int i=0;i<n1;i++)
		if (solver.getVar(x[i]).getVal() < n2) System.out.println(i +" "+ solver.getVar(x[i]).getVal());
    }

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