-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy path2sat.cpp
More file actions
128 lines (102 loc) · 2.46 KB
/
2sat.cpp
File metadata and controls
128 lines (102 loc) · 2.46 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
#include <bits/stdc++.h>
using namespace std;
#define MAINRET(x) in##x
#define what_is(x) cout << #x << " is " << x << endl;
#define LL long long
void solve();
MAINRET(t) main(void) {
std::cin.tie(nullptr);
std::cin.sync_with_stdio(false);
solve();
}
constexpr int INF = (int)1e9 + 100;
constexpr LL LINF = LLONG_MAX / 2;
constexpr LL MX = 3 * 1e5;
constexpr int MD = (int)1e9 + 7;
int n, m, grp[MX], ass[MX];
vector<int> adj[MX], rev[MX], scc[MX];
vector<bool> vis(MX, false);
vector<int> order, comp, rts;
void dfs1(int u) {
vis[u] = true;
for (auto &v : adj[u]) {
if (!vis[v]) {
dfs1(v);
}
}
order.push_back(u);
}
void dfs2(int u) {
vis[u] = true;
comp.push_back(u);
for (auto &v : rev[u]) {
if (!vis[v]) {
dfs2(v);
}
}
}
void solve() {
cin >> n >> m;
int a, b;
char c, d;
for (int i = 0; i < n; i++) {
cin >> c >> a >> d >> b;
a--; b--;
// Create the graph
bool na = c == '-';
bool nb = d == '-';
a = 2*a ^ na;
b = 2*b ^ nb;
int nega = a ^ 1;
int negb = b ^ 1;
adj[nega].push_back(b);
adj[negb].push_back(a);
rev[b].push_back(nega);
rev[a].push_back(negb);
// Note: c, d == pos or neg
// (c(a) OR d(b)) AND ( ...etc )
//adj[a].push_back(b);
//rev[b].push_back(a);
}
for (int i = 0; i < m*2; i++) {
if (!vis[i]) {
dfs1(i);
}
}
vis.assign(m*2, false);
reverse(order.begin(), order.end());
int j = 1;
for (auto &v : order) {
if (!vis[v]) {
dfs2(v);
int rt = comp.front();
for (auto &u : comp) {
grp[u] = j;
}
rts.push_back(rt);
j++;
comp.clear();
}
}
for (int i = 0; i < m*2; i+=2) {
if (grp[i] == grp[i+1]) {
cout << "IMPOSSIBLE\n";
return;
}
// If neg comes later in scc, it will be set
// x will be set to true. i/2 = x, i is a, i+1 is neg a.
// Below, we set i/2 to be false when grp[i] < grp[i+1]
// so we set i/2 to be true when grp[i] > grp[i+1]
ass[i/2] = grp[i] > grp[i+1];
}
for (int i = 0; i < m*2; i+=2) {
if (ass[i/2]) {
cout << '+' << ' ';
} else {
cout << '-' << ' ';
}
}
cout << endl;
}
/*
*/