Cod sursa(job #1597886)

Utilizator TeodorCotetCotet Teodor TeodorCotet Data 12 februarie 2016 14:05:32
Problema 2SAT Scor 0
Compilator cpp Status done
Runda Arhiva educationala Marime 3.23 kb
//============================================================================
// Name        : 2SAT.cpp
// Author      : Teodor Cotet
// Version     :
// Copyright   : Your copyright notice
// Description : SAT in O in O(N + M) C++, Ansi-style
//============================================================================
#include <fstream>
#include <vector>
#include <iostream>
#include <cstring>
#include <stack>
#include <set>

using namespace std;

const int NMAX = 100000;
const int MMAX = 200000;

ifstream fin("2sat.in");
ofstream fout("2sat.out");

int n; int m;

/*
 * constructors for vector:
 * v(int size)
 * v(int size, TYPE value)
 */

vector< vector<int> > g(NMAX * 2 + 1, vector<int>(0));
vector< vector<int> > gTranspose(NMAX * 2 + 1, vector<int>(0));

vector<int>::iterator it;

stack<int> s;

vector< vector<int> > strongComp;

int negateNode(int x) {

	return (x == n) ? (2 * n) : (x + n) % (2 *  n);
}

void read() {

	fin >> n >> m;

	for(int i = 0 ; i < m ; ++i) {

		int x; int y;
		fin >> x >> y;

		if(x < 0) x = -x + n;
		if(y < 0) y = -y + n;

		/* p v q <=> !p -> q sau !q ->p */

		//cout << x << " " << y << " " << negateNode(x) << " " << negateNode(y) << '\n';

		g[negateNode(x)].push_back(y);
		g[negateNode(y)].push_back(x);

		gTranspose[y].push_back(negateNode(x));
		gTranspose[x].push_back(negateNode(y));
	}
}

void dfs(int curent, vector< vector<int> >& g, bool visited[]) {

	visited[curent] = 1;
	//for(it = g[curent].begin(); it != g[curent].end(); ++it) {
	for(unsigned i = 0; i < g[curent].size(); ++i) {
		if(visited[g[curent][i]] == 0)
			dfs(g[curent][i], g, visited);
	}

	s.push(curent);
}

void dfsComponents(int curent, vector < vector<int> > gTranspose, bool visited[]) {

	visited[curent] = 1;
	strongComp[strongComp.size() - 1].push_back(curent);

	for(unsigned i = 0 ; i < gTranspose[curent].size(); ++i)
		if(visited[gTranspose[curent][i]] == 0)
			dfsComponents(gTranspose[curent][i], gTranspose, visited);

}

void getStrongConnected(vector< vector<int> >& g, vector< vector<int> >& gTranspose) {

	/* do a topological sort first */

	bool visited[NMAX * 2 + 1];
	//for(int i = 0 ; i < 2 * n + 1; ++i)
	//	visited[i] = 0;

	memset(visited, 0, 2 * n + 1);

	for(int i = 1; i <= 2 * n ; ++i) {
		if(visited[i] == 0)
			dfs(i, g, visited);
	}

	/* if there is a node which "enters" in the first node from the topological sort, it
	 * means they are in the same strong connected component, so we make a dfs in the transpose graph
	 */
	memset(visited, 0, 2 * n + 1);

	while( s.empty() == false) {

		int node = s.top();
		s.pop();

		if(visited[node] == 0) {
			strongComp.push_back(vector<int>(0));
			dfsComponents(node, gTranspose, visited);
		}
	}

}

bool checkSat(vector< vector<int> > strongComp) {

	/*
	 * check if node A and !A is in the same strong connected component=> is not satisfiable
	 */

	set<int> mul;

	for(unsigned i = 0 ; i < strongComp.size(); ++i) {

		mul.clear();

		for(it = strongComp[i].begin(); it != strongComp[i].end(); ++it) {
			if( mul.find(negateNode(*it)) == mul.end())
				return false;
			else
				mul.insert(*it);
		}
	}

	return true;
}

void solve() {

	getStrongConnected(g, gTranspose);

	if(checkSat(strongComp) == false) {
		fout << -1;
		return ;
	}
}

int main() {

	read();

	solve();

	return 0;
}