-
Notifications
You must be signed in to change notification settings - Fork 11
Expand file tree
/
Copy pathtwo_sat.cpp
More file actions
116 lines (112 loc) · 2.63 KB
/
two_sat.cpp
File metadata and controls
116 lines (112 loc) · 2.63 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
#include <bits/stdc++.h>
#include <ext/pb_ds/assoc_container.hpp>
#include <ext/pb_ds/tree_policy.hpp>
using namespace std;
using namespace __gnu_pbds;
template <class T>
using ordered_set = tree<T, null_type, less<T>, rb_tree_tag, tree_order_statistics_node_update>;
#define int long long int
#define endl '\n'
#define pb push_back
#define pi pair<int, int>
#define pii pair<int, pi>
#define fir first
#define sec second
#define MAXN 200005
#define mod 1000000007
struct two_sat
{
int n;
vector<vector<int>> g, gr; // gr is the reversed graph
vector<int> comp, ord, ans; // comp[v]: ID of the SCC containing node v
vector<bool> vis;
two_sat() {}
two_sat(int sz)
{
n = sz;
g.assign(2 * n, vector<int>());
gr.assign(2 * n, vector<int>());
comp.resize(2 * n);
vis.resize(2 * n);
ans.resize(2 * n);
}
void add_edge(int u, int v)
{
g[u].push_back(v);
gr[v].push_back(u);
}
// int x, bool val: if 'val' is true, we take the variable to be x. Otherwise we take it to be x's complement (not x).
void implies(int i, bool f, int j, bool g) // a -> b
{
add_edge(i + (f ? 0 : n), j + (g ? 0 : n));
add_edge(j + (g ? n : 0), i + (f ? n : 0));
}
void add_clause_or(int i, bool f, int j, bool g) // At least one of them is true
{
add_edge(i + (f ? n : 0), j + (g ? 0 : n));
add_edge(j + (g ? n : 0), i + (f ? 0 : n));
}
void add_clause_xor(int i, bool f, int j, bool g) // only one of them is true
{
add_clause_or(i, f, j, g);
add_clause_or(i, !f, j, !g);
}
void add_clause_and(int i, bool f, int j, bool g) // both of them have the same value
{
add_clause_xor(i, !f, j, g);
}
void set(int i, bool f) // Set a variable
{
add_clause_or(i, f, i, f);
}
void top_sort(int u)
{
vis[u] = 1;
for (auto const &v : g[u])
{
if (!vis[v])
top_sort(v);
}
ord.push_back(u);
}
void scc(int u, int id)
{
vis[u] = 1;
comp[u] = id;
for (auto const &v : gr[u])
{
if (!vis[v])
scc(v, id);
}
}
bool solve()
{
fill(vis.begin(), vis.end(), 0);
for (int i = 0; i < 2 * n; i++)
{
if (!vis[i])
top_sort(i);
}
fill(vis.begin(), vis.end(), 0);
reverse(ord.begin(), ord.end());
int id = 0;
for (const auto &v : ord)
{
if (!vis[v])
scc(v, id++);
}
for (int i = 0; i < n; i++)
{
if (comp[i] == comp[i + n])
return 0;
ans[i] = (comp[i] > comp[i + n]) ? 1 : 0;
}
return 1;
}
};
signed main()
{
}
// https://codeforces.com/blog/entry/92977
// https://codeforces.com/blog/entry/16205
// https://cp-algorithms.com/graph/2SAT.html