import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.StringTokenizer;

import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.variables.integer.IntegerVariable;


public class DecisionProblemSolver {
	public static void main(String args[]){
		CPModel model = new CPModel();
		CPSolver solver = new CPSolver();
		String data;
		StringTokenizer tokens;
		ArrayList edge = new ArrayList();
		int n = 0,k;
		double p;
		
		try {
			BufferedReader fin = new BufferedReader(new FileReader(args[0]));
			
			if((data = fin.readLine()) != null){
				tokens = new StringTokenizer(data, " ");				
				n = Integer.parseInt(tokens.nextToken());				
				if (tokens.hasMoreTokens())
					p = Double.parseDouble(tokens.nextToken());
			}
			
			k = Integer.parseInt(args[1]);
			IntegerVariable [] vertex = makeIntVarArray("vertex",n,0,1);			
			
			while((data = fin.readLine()) != null){
				tokens = new StringTokenizer(data, " ");
				int [] temp = new int[2];
				temp[0] = Integer.parseInt(tokens.nextToken());
				temp[1] = Integer.parseInt(tokens.nextToken());
				
				edge.add(temp);
			}
//			for (int i = 0; i < edge.size(); i++)
//				System.out.println(((int[])(edge.get(i)))[0] + " " + ((int[])(edge.get(i)))[1]);
			
			for (int i = 0; i < edge.size(); i++)
				model.addConstraint(lt(sum(vertex[((int[])(edge.get(i)))[0]],vertex[((int[])(edge.get(i)))[1]]),2));
			
			
			model.addConstraint(geq(sum(vertex),k));
		} catch (FileNotFoundException e) {
			System.out.println("File Not Found!");
		} catch (IOException e) {
			System.out.println("IO Error!");
		}
		
		solver.read(model);
		if (solver.solve())
			System.out.println("true");			
			
		else System.out.println("false");
		System.out.println(solver.getNodeCount() +" "+ solver.getTimeCount());
		solver.printRuntimeSatistics();
	}
}