Cod sursa(job #1542858)

Utilizator baetucBaetu Ciprian baetuc Data 5 decembrie 2015 18:52:28
Problema 2SAT Scor 70
Compilator cpp Status done
Runda Arhiva educationala Marime 3.88 kb
#include<iostream>
#include<fstream>
#include<vector>

using namespace std;

#define INPUT "2sat.in"
#define OUTPUT "2sat.out"
#define MAX_LIT 100000
#define MAX_DISJUNCTIONS 200000

int literals;
int conjunctions;

bool viz[2 * MAX_LIT];
int connexComponent[2 * MAX_LIT];
vector<int> adjacencyLists[2 * MAX_LIT];
vector<int> revertedAdjacencyLists[2 * MAX_LIT];

int noOfStronglyConnectedComp;

vector<int> component[2 * MAX_LIT + 1];

vector<int> orderList;

bool truth[MAX_LIT + 1];


void clearArray(int* arr, int n) {
	for (int i = 0; i < n; ++i) {
		arr[i] = 0;
	}
}

void clearBoolArray(bool* arr, int n) {
	for (int i = 0; i < n; ++i) {
		arr[i] = false;
	}
}

int getIndex(int i) {
	if (i < 0) {
		return i + literals;
	}
	return i + literals - 1;
}

void constructEdge(int left, int right) {
	adjacencyLists[getIndex(-left)].insert(adjacencyLists[getIndex(-left)].end(), getIndex(right));
	adjacencyLists[getIndex(-right)].insert(adjacencyLists[getIndex(-right)].end(), getIndex(left));
}

void readInput() {
	ifstream in(INPUT);
	in >> literals;
	in >> conjunctions;
	int left, right;
	for (int i = 0; i < conjunctions; ++i) {
		in >> left;
		in >> right;
		constructEdge(left, right);
	}
	in.close();
}

void firstDFS(int node) {
	viz[node] = true;
	for (int i = 0; i < adjacencyLists[node].size(); ++i) {
		if (!viz[adjacencyLists[node].at(i)]) {
			firstDFS(adjacencyLists[node].at(i));
		}
	}
	orderList.insert(orderList.begin(), node);
}

void constructOrderList() {
	orderList.clear();
	clearBoolArray(viz, 2 * literals);
	for (int i = 0; i < 2 * literals; ++i) {
		if (!viz[i]) {
			firstDFS(i);
		}
	}
}

void constructRevertedAdjacencyLists() {
	for (int i = 0; i < 2 * literals; ++i) {
		for (int j = 0; j < adjacencyLists[i].size(); ++j) {
			revertedAdjacencyLists[adjacencyLists[i].at(j)].insert(revertedAdjacencyLists[adjacencyLists[i].at(j)].end(), i);
		}
	}
}

void secondDFS(int i, int t) {
	connexComponent[i] = t;
	component[t].insert(component[t].end(), i);
	for (int j = 0; j < revertedAdjacencyLists[i].size(); ++j) {
		if (!connexComponent[revertedAdjacencyLists[i].at(j)]) {
			secondDFS(revertedAdjacencyLists[i].at(j), t);
		}
	}
}

void constructComponents() {
	noOfStronglyConnectedComp = 1;
	clearArray(connexComponent, 2 * literals);
	for (int i = 0; i < 2 * literals; ++i) {
		if (!connexComponent[orderList.at(i)]) {
			secondDFS(orderList.at(i), noOfStronglyConnectedComp);
			++noOfStronglyConnectedComp;
		}
	}
}

void constructStronglyConnectedComponents() {
	constructOrderList();
	constructRevertedAdjacencyLists();
	constructComponents();
}

bool areOpposite(int i, int j) {
	return (i + j == 2 * literals - 1);
}

bool isFormulaeSatisfiable() {
	for (int i = 0; i < literals; ++i) {
		if (connexComponent[i] == connexComponent[2 * literals - 1 - i]) {
			return false;
		}
	}
	return true;

}

void giveValues() {
	clearBoolArray(viz, literals + 1);
	for (int i = 1; i <= noOfStronglyConnectedComp; ++i) {

		for (int j = 0; j < component[i].size(); ++j) {
			int node = component[i].at(j);
			if (node < literals) {
				if (!viz[literals - node]) {
					truth[literals - node] = true;
					viz[literals - node] = true;
				}
			}
			else {
				if (!viz[node - literals + 1]) {
					truth[node - literals + 1] = false;
					viz[node - literals + 1] = true;
				}
			}
		}
	}
}

void printResult() {
	ofstream out(OUTPUT, fstream::trunc | fstream::out);
	if (!isFormulaeSatisfiable()) {
		out << -1;
	}
	else {
		giveValues();
		if (truth[1] == false) {
			out << "0";
		}
		else {
			out << "1";
		}
		for (int i = 2; i <= literals; ++i) {
			if (truth[i] == false) {
				out << " 0";
			}
			else {
				out << " 1";
			}
		}
	}
	out.close();
}


int main() {
	readInput();
	constructStronglyConnectedComponents();
	printResult();
}