Pagini recente » Cod sursa (job #578371) | Cod sursa (job #2664687) | Cod sursa (job #2662599) | Cod sursa (job #2802662) | Cod sursa (job #3230185)
/**
* https://codeforces.com/blog/entry/16205
*/
#include <fstream>
#include <iostream>
#include <vector>
#include <stack>
using std::vector, std::stack;
class Graph2SAT {
private:
vector<vector<int>>neighbours_transpose;
int nodes;
int comp_cnt;
int threshold_comp;
public:
vector<vector<int>>neighbours;
Graph2SAT(int literals) {
this->nodes = 2 * literals;
neighbours.assign(2 * literals, vector<int>());
neighbours_transpose.assign(2 * literals, vector<int>());
}
vector<int>comp; // component number
static int pozitive_literal(int literal) { return (literal << 1); }
static int negative_literal(int literal) { return (literal << 1) | 1; }
void implies(int literal1, int literal2) {
// std::cout << "add " << literal1 << " " << literal2 <<"\n";
neighbours[literal1].push_back(literal2);
neighbours_transpose[literal2].push_back(literal1);
// std::cout << "done implies\n";
}
void dfs_util_topo_sort(int node, bool visited[], stack<int> &st) {
visited[node] = true;
for (const auto &x: neighbours[node]) {
if (!visited[x]) {
dfs_util_topo_sort(x, visited, st);
}
}
st.push(node);
}
void dfs_util_kosaraju(int node, int _comp_cnt) {
comp[node] = _comp_cnt;
for (const auto &x: neighbours_transpose[node]) {
if (comp[x] < 0) {
dfs_util_kosaraju(x, _comp_cnt);
}
}
}
void strongly_connected_components() {
stack<int>st;
bool visited[nodes];
for (int i = 0; i < nodes; i++)
visited[i] = false;
for (int i = 0; i < nodes; i++) {
if (!visited[i]) {
dfs_util_topo_sort(i, visited, st);
// std::cout << "visited ";
// for (int j = 0; j < nodes; j++) {
// std::cout << visited[j] << " ";
// }
// std::cout << "\n";
}
}
std::cout << "after dfs util topo sort\n";
comp.assign(nodes, -1);
comp_cnt = 1;
while (!st.empty()) {
if (comp[st.top()] < 0) {
dfs_util_kosaraju(st.top(), comp_cnt);
comp_cnt++;
}
st.pop();
}
}
};
int main() {
std::ifstream fin("2sat.in");
std::ofstream fout("2sat.out");
int N, M;
fin >> N >> M;
int x, y, c;
Graph2SAT graph(N);
for (int i = 0; i < M; i++) {
fin >> x >> y;
c=0;
// x--;
// y--;
switch (c)
{
case 0:
int literal1, literal2;
if (x < 0) {
literal1 = Graph2SAT::negative_literal(-x - 1);
} else literal1 = Graph2SAT::pozitive_literal(x - 1);
if (y < 0) {
literal2 = Graph2SAT::negative_literal(-y - 1);
} else literal2 = Graph2SAT::pozitive_literal(y - 1);
// not (x) => y
graph.implies(literal1 ^ 1, literal2);
// not (y) => x
graph.implies(literal2 ^ 1, literal1);
break;
case 1:
// not(x) => not(y)
graph.implies(Graph2SAT::negative_literal(x), Graph2SAT::negative_literal(y));
break;
case 2:
// not(y) => not(x)
graph.implies(Graph2SAT::negative_literal(y), Graph2SAT::negative_literal(x));
break;
case 3:
// x => not(y)
graph.implies(Graph2SAT::pozitive_literal(x), Graph2SAT::negative_literal(y));
// y => not(x)
graph.implies(Graph2SAT::pozitive_literal(y), Graph2SAT::negative_literal(x));
break;
default:
break;
}
}
// for (int i = 0; i < N; i++) {
// std::cout << "neighbours of pozitive " << i << "\t";
// for (const auto &x: graph.neighbours[2 * i]) {
// std::cout << x << " ";
// }
// std::cout << "\n";
// std::cout << "neighbours of negative " << i << "\t";
// for (const auto &x: graph.neighbours[2 * i + 1]) {
// std::cout << x << " ";
// }
// std::cout << "\n";
// }
// std::cout << "read done\n";
graph.strongly_connected_components();
// std::cout << "components:\t";
// for (int i = 0; i < 2 * N; i++) {
// std::cout << graph.comp[i] << " ";
// }
// std::cout <<"\n";
int cnt = 0;
vector<int>literal_value(N);
for (int i = 0; i < N; i++) {
if (graph.comp[i * 2] > graph.comp[2 * i + 1]) {
literal_value[i] = 1;
cnt++;
}
}
for (int i = 0; i < N; i++) {
// if (literal_value[i]) {
fout << literal_value[i] << " ";
// }
}
std::cout << "finish\n";
return 0;
}