import java.util.*;
import java.io.*;
import choco.Problem;
import choco.ContradictionException;
import choco.integer.*;
import choco.Constraint;
import choco.integer.search.DecreasingDomain;
import choco.Solver;
import choco.Solution;
import choco.search.*;

public class CSP {

    private int noCars;                // number of cars
    private int noOpt;                 // number of options
    private int noClass;               // number of classes
    private int[] p;                   // number of cars with option i in a block
    private int[] q;                   // size of a block for option i
    private int[] demand;              // demand for class i, i.e. number of cars of class i
    private int[][] option;            // option[i][j] = 1 <-> class i requires option j
    private int[] optDemand;           // demand for an option
    private MyProblem pb;
    private IntDomainVar[] position;   // the car that is made in position[i] of a sequence
    private IntDomainVar optPos[][];   // optPos[i][j] = 1 if option i is made in position j
    private int[] orderedDomain;
    private double[] heuVal;
	
    public CSP(String fname) throws Exception {
	MyIo fin      = new MyIo(fname);
	noCars        = fin.getNextInt();
	noOpt         = fin.getNextInt();
	noClass       = fin.getNextInt();
	p             = new int[noOpt];
	q             = new int[noOpt];
	demand        = new int[noClass];
	option        = new int[noClass][noOpt];
	optDemand     = new int[noOpt];
	orderedDomain = new int[noClass];
	heuVal        = new double[noClass];

	for (int i=0;i<noOpt;i++) p[i] = fin.getNextInt();
	for (int i=0;i<noOpt;i++) q[i] = fin.getNextInt();
	for (int i=0;i<noClass;i++){
	    fin.getNextInt();  // skip id number
	    demand[i] = fin.getNextInt();
	    for (int j=0;j<noOpt;j++)
		option[i][j] = fin.getNextInt();
	}
	fin.close();
	for (int j=0;j<noOpt;j++){
	    optDemand[j] = 0;
	    for (int i=0;i<noClass;i++) 
		optDemand[j] = optDemand[j] + option[i][j]*demand[i];
	}	    
	
	pb       = new MyProblem();
	position = pb.makeEnumIntVarArray("position",noCars,0,noClass-1);
	optPos   = pb.makeEnumIntVarArray("optPos",noOpt,noCars,0,1);
	
	for (int i=0;i<noOpt;i++) pqConstraint(p[i],q[i],i);
    for (int c=0;c<noClass;c++)
	    for (int pos=0;pos<noCars;pos++) classConstraint(c,pos);
	for (int c=0;c<noClass;c++) demandConstraint(c,demand[c]);
	for (int j=0;j<noOpt;j++) optionConstraint(j);
	for (int j=0;j<noOpt;j++) redundantOptionConstraint(j);
    }
    
    public int getNoCars(){return noCars;}
    public int getNoClass(){return noClass;}
    public IntDomainVar[] getPosition(){return position;}
    public MyProblem getMyProblem(){return pb;}

    public String look(){
	String s = noCars + " " + noOpt + " " + noClass + "\n";
	for (int i=0;i<noOpt;i++) s = s + p[i] + " ";
	s = s + "\n";
	for (int i=0;i<noOpt;i++) s = s + q[i] + " ";
	s = s + "\n";
	for (int i=0;i<noClass;i++){
	    s = s + i + " " + demand[i] + " ";
	    for (int j=0;j<noOpt;j++) s = s + option[i][j] + " ";
	    s = s + "\n";
	}
	for (int i=0;i<noClass;i++) s = s + heuVal[i] + "  ";
	s = s + "\n";
	for (int i=0;i<noClass;i++) s = s + orderedDomain[i] + "  ";
	s = s + "\n";
	for (int i=0;i<noOpt;i++) s = s + optDemand[i] + "  ";
	s = s + "\n";
	return s;
    }

    public String toString(){
	String s = "";
	for (int i=0;i<noCars;i++){
	    int c = position[i].getVal();
	    s = s + c + " ";
	    for (int j=0;j<noOpt;j++)
		s = s + option[c][j] + " ";
	    s = s + "\n";
	}
	//for (int i=0;i<noClass;i++) s = s + H(i) + "  ";
	//s = s + "\n";
	//int[] od = getOrderedDomain(h);
	//for (int i=0;i<noClass;i++) s = s + od[i] + "  ";
	return s;
    }
	
    public void pqConstraint(int p,int q,int opt){
	int n = noCars;
	IntDomainVar v[] = new IntDomainVar[q];
	for (int i=0;i<n-q;i++){
	    for (int j=0;j<q;j++) v[j] = optPos[opt][i+j];
	    pb.post(pb.leq(pb.sum(v),p));
	}
    }
    //
    // Given an option opt, constrain this such that at most
    // p of these options are allowed in a block of length q. 
    //

    /*
    public void classConstraint(int c,int i){
	for (int j=0;j<noOpt;j++)
	    pb.post(pb.implies(pb.eq(position[i],c),pb.eq(optPos[j][i],option[c][j])));
    }
    */

    public void classConstraint(int c,int i){
	Constraint[]C1 = new Constraint[noOpt + 1];
	Constraint[]C2 = new Constraint[noOpt];
	for (int j=0;j<noOpt;j++) {
	    C1[j] = pb.eq(optPos[j][i],option[c][j]);
	    C2[j] = pb.eq(optPos[j][i],1-option[c][j]);
	}
	//pb.post(pb.ifOnlyIf(pb.eq(position[i],c),pb.and(C)));
	//pb.post(pb.implies(pb.and(C),pb.eq(position[i],c)));
	C1[noOpt] = pb.eq(position[i],c);
	Constraint C3 = pb.and(C1);
	Constraint C4 = pb.or(C2);
	Constraint C5 = pb.and(C4,pb.neq(position[i],c));
	pb.post(pb.or(C3,C5));
    }
    //
    // A car of class c is being made in position i in the sequence
    // Constrain options in that position with respect to that class
    //


    public void optionConstraint(int j){
	int m = noClass;
	for (int i=0;i<noClass;i++) m = m - option[i][j];
	int[]v = new int[m];
	int k = 0;
	for (int i=0;i<noClass;i++){
	    if (option[i][j]==0){v[k] = i;k++;}
	}
	for (int i=0;i<noCars;i++){
	    Constraint[] C = new Constraint[m];
	    for (int x=0;x<m;x++) C[x] = pb.neq(position[i],v[x]);
	    pb.post(pb.ifOnlyIf(pb.and(C),pb.eq(optPos[j][i],1)));
	}
    }
    //
    // Given option j, find m number of classes that do NOT use this option
    // create an array v of length m.
    // fill v with classes that do not use option j
    // post a constraint that optPos[j][k]==1 <-> AND(position[j]!=i) 
    // for all positions k, where i is in v
    //

    public void redundantOptionConstraint(int j){
	for (int k=1;k<noCars/q[j];k++){
	    IntDomainVar v[] = new IntDomainVar[noCars-k*q[j]];
	    for (int i=0;i<noCars-k*q[j];i++) v[i] = optPos[j][i];
	    pb.post(pb.geq(pb.sum(v),optDemand[j]-k*p[j]));	    
	}
    }

    public void demandConstraint(int c, int quantity){
	pb.post(pb.occurrence(position,c,pb.makeConstantIntVar(demand[c])));
    }

    private double optionLoad(int j){
	int dj = optDemand[j];
	return ((double)dj)*(1.0 - ((double)p[j])/((double)q[j]));
    }

    public double H4(int i){
	double h = 0.0;
	for (int j=0;j<noOpt;j++) if (option[i][j]==1) h = h + optionLoad(j);
	return 1.0/h;
    }
    //
    // not H2
    //

    public double H3(int i){
	double h = 0.0;
	for (int j=0;j<noOpt;j++) h = h + (double)option[i][j];
	return 1.0/h;
    }
    //
    // not H1
    //

    public double H2(int i){
	double h = 0.0;
	for (int j=0;j<noOpt;j++) if (option[i][j]==1) h = h + optionLoad(j);
	return h;
    }
    //
    // heuristic value of selecting a car of class i
    //

    public double H1(int i){
	double h = 0.0;
	for (int j=0;j<noOpt;j++) h = h + (double)option[i][j];
	return h;
    }
    //
    // heuristic value just number of options
    //

    public double H0(int i){
	double h = (double)(noClass-i);
	return h;
    }
    //
    // heuristic value just index i
    //

    private void swap(int[]x,int i,int j){
	int temp = x[i];
	x[i] = x[j];
	x[j] = temp;
    }

    private void swap(double[]x,int i,int j){
	double temp = x[i];
	x[i] = x[j];
	x[j] = temp;
    }

    private void sort(double[]h,int[]d){
	boolean swapped = true;
	int n = h.length;
	while (swapped){
	    swapped = false;
	    for (int i=0;i<n-1;i++)
		if (h[i]<h[i+1]){
		    swap(h,i,i+1);
		    swap(d,i,i+1);
		    swapped = true;
		}
	}
    }
	

    public int[] getOrderedDomain(int x){
	int n     = noClass;
	boolean swapped = true;
	for (int i=0;i<n;i++){
	    if (x==0) heuVal[i] = H0(i);
	    if (x==1) heuVal[i] = H1(i);
	    if (x==2) heuVal[i] = H2(i);
	    orderedDomain[i] = i;
	}
	sort(heuVal,orderedDomain);
	return orderedDomain;
    }
}