Pagini recente » Cod sursa (job #2583585) | Cod sursa (job #226805) | Cod sursa (job #723016) | Cod sursa (job #3185785) | Cod sursa (job #1597886)
//============================================================================
// 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;
}