Skip to content

Commit

Permalink
Split SCC out from 2SAT
Browse files Browse the repository at this point in the history
  • Loading branch information
baluteshih committed Apr 6, 2024
1 parent be58eb4 commit 575e298
Show file tree
Hide file tree
Showing 3 changed files with 39 additions and 38 deletions.
46 changes: 9 additions & 37 deletions codebook/2_Graph/2SAT.cpp
Original file line number Diff line number Diff line change
@@ -1,47 +1,19 @@
struct SAT { // 0-base
int low[N], dfn[N], bln[N], n, Time, nScc;
bool instack[N], istrue[N];
stack<int> st;
vector<int> G[N], SCC[N];
void init(int _n) {
n = _n; // assert(n * 2 <= N);
for (int i = 0; i < n + n; ++i) G[i].clear();
}
void add_edge(int a, int b) { G[a].pb(b); }
int n;
vector<bool> istrue;
SCC scc;
SAT(int _n): n(_n), istrue(n + n), scc(n + n) {}
int rv(int a) {
if (a >= n) return a - n;
return a + n;
return a >= n ? a - n : a + n;
}
void add_clause(int a, int b) {
add_edge(rv(a), b), add_edge(rv(b), a);
}
void dfs(int u) {
dfn[u] = low[u] = ++Time;
instack[u] = 1, st.push(u);
for (int i : G[u])
if (!dfn[i])
dfs(i), low[u] = min(low[i], low[u]);
else if (instack[i] && dfn[i] < dfn[u])
low[u] = min(low[u], dfn[i]);
if (low[u] == dfn[u]) {
int tmp;
do {
tmp = st.top(), st.pop();
instack[tmp] = 0, bln[tmp] = nScc;
} while (tmp != u);
++nScc;
}
scc.add_edge(rv(a), b), scc.add_edge(rv(b), a);
}
bool solve() {
Time = nScc = 0;
for (int i = 0; i < n + n; ++i)
SCC[i].clear(), low[i] = dfn[i] = bln[i] = 0;
for (int i = 0; i < n + n; ++i)
if (!dfn[i]) dfs(i);
for (int i = 0; i < n + n; ++i) SCC[bln[i]].pb(i);
scc.solve();
for (int i = 0; i < n; ++i) {
if (bln[i] == bln[i + n]) return false;
istrue[i] = bln[i] < bln[i + n];
if (scc.bln[i] == scc.bln[i + n]) return false;
istrue[i] = scc.bln[i] < scc.bln[i + n];
istrue[i + n] = !istrue[i];
}
return true;
Expand Down
27 changes: 27 additions & 0 deletions codebook/2_Graph/SCC.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
struct SCC { // 0-base
int n, dft, nscc;
vector<int> low, dfn, bln, instack, stk;
vector<vector<int>> G;
void dfs(int u) {
low[u] = dfn[u] = ++dft;
instack[u] = 1, stk.pb(u);
for (int v : G[u])
if (!dfn[v])
dfs(v), low[u] = min(low[u], low[v]);
else if (instack[v] && dfn[v] < dfn[u])
low[u] = min(low[u], dfn[v]);
if (low[u] == dfn[u]) {
for (; stk.back() != u; stk.pop_back())
bln[stk.back()] = nscc, instack[stk.back()] = 0;
instack[u] = 0, bln[u] = nscc++, stk.pop_back();
}
}
SCC(int _n): n(_n), dft(), nscc(), low(n), dfn(n), bln(n), instack(n), G(n) {}
void add_edge(int u, int v) {
G[u].pb(v);
}
void solve() {
for (int i = 0; i < n; ++i)
if (!dfn[i]) dfs(i);
}
}; // scc_id(i): bln[i]
4 changes: 3 additions & 1 deletion codebook/content.tex
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,9 @@ \subsection{BCC Vertex*} % test by Library Checker Biconnected Components, block
\lstinputlisting{2_Graph/BCC_Vertex.cpp}
\subsection{Bridge*} % test by Library Checker Two-Edge-Connected Components
\lstinputlisting{2_Graph/Bridge.cpp}
\subsection{2SAT (SCC)*} % SCC test by TIOJ 2143, 2SAT test by ARC069 F
\subsection{SCC*} % SCC test by Library Checker Strongly Connected Components
\lstinputlisting{2_Graph/SCC.cpp}
\subsection{2SAT*} % test by ARC069 F
\lstinputlisting{2_Graph/2SAT.cpp}
\subsection{MinimumMeanCycle*} % test by TIOJ 1934
\lstinputlisting{2_Graph/MinimumMeanCycle.cpp}
Expand Down

0 comments on commit 575e298

Please sign in to comment.