// Arup Guha
// 7/25/2011
// Example for COT 4210 written in class.
// Edited on 11/17/2011 for Program #2 solution and separated out into a single file.

import java.io.*;
import java.util.*;

// Stores an instance of 3-SAT
public class sat {

	public int numClauses;
	public int numVariables;
	public int[][] clauses;
	
	// Assumes fin is reading from a file that describes
	// a 3-sat instance.
	public sat(Scanner fin) {
	
		// Read in the number of clauses and variables.
		numClauses = fin.nextInt();
		numVariables = fin.nextInt();
		
		// Read through each variable in each clause.
		clauses = new int[numClauses][3];
		for (int i=0; i<numClauses; i++)
			for (int j=0; j<3; j++)
				clauses[i][j] = fin.nextInt();	
	}
	
	// Returns true iff x and y have equal magnitude and have
	// opposite signs.
	public static boolean oppose(int x, int y) {
		return x+y == 0;
	}
	
	public graphk reduceToClique() {
	
		// Make the graph the correct size.
		boolean[][] graph = new boolean[3*numClauses][3*numClauses];
		
		for (int i=0; i<graph.length; i++) {
			for (int j=i+1; j<graph.length; j++) {
				
				// These two variables are in the same clause.
				if (i/3 == j/3) continue;
				
				// These two variables are direct opposites.
				if (oppose(clauses[i/3][i%3], clauses[j/3][j%3]))
				    continue;
					 
				// If we get here, we must connect these two vertices by
				// an edge.
				graph[i][j] = true;
				graph[j][i] = true;
			}
		}
		
		// Returns the appropriate instance of Clique.
		return new graphk(graph, numClauses);	
	}
	
	public graphk reduceToVC() {
		
		int len = 3*numClauses+2*numVariables;
		boolean[][] graph = new boolean[len][len];
		
		// Fill in all triangles.
		for (int i=0; i<3*numClauses; i+=3) {
			for (int j=0; j<3; j++) {
				graph[i+j][i+(j+1)%3] = true;
				graph[i+(j+1)%3][i+j] = true;	
			}
		}
		
		// Fill in the bars.
		for (int i=3*numClauses; i<len; i+=2) {
			graph[i][i+1] = true;
			graph[i+1][i] = true;
		}
		
		// Fill in connections between nodes with the same labels.
		for (int i=0; i<numClauses; i++) {
			for (int j=0; j<3; j++) {
				int var = clauses[i][j];
				int vertexNumber;
				
				// Figure out which vertex is represented by this variable - 2 cases.
				if (var > 0)
					vertexNumber = 3*numClauses+2*(var-1);
				else 
					vertexNumber = 3*numClauses+2*(-var)-1;
					
				// Fill in this edge from the triangle vertex to the appropriate bar vertex.
				graph[3*i+j][vertexNumber] = true;
				graph[vertexNumber][3*i+j] = true;
			}
		}
		
		return new graphk(graph, 2*numClauses + numVariables);
	}
	
}