From 59bea75c7c785e9012b0f3d677b9afbf93818fb4 Mon Sep 17 00:00:00 2001 From: Gloria Mundi Date: Sun, 8 Jun 2025 23:30:29 +0200 Subject: make SCC a struct, and minor 2SAT changes --- content/graph/2sat.cpp | 26 +++++++++++++------------- content/graph/scc.cpp | 45 ++++++++++++++++++++++----------------------- test/graph/2sat.cpp | 10 +++------- test/graph/2sat.cpp.awk | 6 ------ test/graph/scc.cpp | 24 ++++++++++++------------ 5 files changed, 50 insertions(+), 61 deletions(-) delete mode 100644 test/graph/2sat.cpp.awk diff --git a/content/graph/2sat.cpp b/content/graph/2sat.cpp index b9cfd1c..d4c8b7b 100644 --- a/content/graph/2sat.cpp +++ b/content/graph/2sat.cpp @@ -1,28 +1,28 @@ -constexpr int var(int i) {return i << 1;} // use this! -struct sat2 { - int n; // + scc variablen +constexpr int var(int i) { return i << 1; } // use this! +struct SAT2 { + int n; + vector> adj; vector sol; - sat2(int vars) : n(vars*2), adj(n) {} + SAT2(int vars) : n(vars*2), adj(n) {} void addImpl(int a, int b) { adj[a].push_back(b); adj[1^b].push_back(1^a); } void addEquiv(int a, int b) { addImpl(a, b); addImpl(b, a); } - void addOr(int a, int b) { addImpl(1^a, b);} - void addXor(int a, int b) { addOr(a, b); addOr(1^a, 1^b); } - void addTrue(int a) { addImpl(1^a, a);} - void addFalse(int a) { addTrue(1^a);} + void addOr(int a, int b) { addImpl(1^a, b); } + void addXor(int a, int b) { addEquiv(a, 1^b); } + void addTrue(int a) { addImpl(1^a, a); } + void addFalse(int a) { addTrue(1^a); } void addAnd(int a, int b) { addTrue(a); addTrue(b); } void addNand(int a, int b) { addOr(1^a, 1^b); } bool solve() { - scc(); //scc code von oben + SCC scc(adj); // SCC @\sourceref{graph/scc.cpp}@ sol.assign(n, -1); - for (int i = 0; i < n; i += 2) { - if (idx[i] == idx[i + 1]) return false; - sol[i] = idx[i] < idx[i + 1]; - sol[i + 1] = !sol[i]; + for (int i = 0; i < n; i++) { + if (scc.idx[i] == scc.idx[1^i]) return false; + sol[i] = scc.idx[i] < scc.idx[1^i]; } return true; } diff --git a/content/graph/scc.cpp b/content/graph/scc.cpp index 9f8f850..a9e10c1 100644 --- a/content/graph/scc.cpp +++ b/content/graph/scc.cpp @@ -1,26 +1,25 @@ -vector> adj; -vector low, idx, s; // idx enthält Index der SCC pro Knoten -vector> sccs; // Liste der Knoten pro SCC +struct SCC { + vector idx; // idx enthält Index der SCC pro Knoten + vector> sccs; // Liste der Knoten pro SCC -void visit(int v) { - int old = low[v] = ssize(s); - s.push_back(v); + SCC(const vector> &adj): idx(ssize(adj), -1) { + vector low(ssize(adj), -1); + vector s; + auto dfs = [&](auto &&self, int v) -> void { + int old = low[v] = ssize(s); + s.push_back(v); - for (auto u : adj[v]) { - if (low[u] < 0) visit(u); - if (idx[u] < 0) low[v] = min(low[v], low[u]); - } + for (auto u : adj[v]) { + if (low[u] < 0) self(self, u); + if (idx[u] < 0) low[v] = min(low[v], low[u]); + } - if (old == low[v]) { - sccs.emplace_back(begin(s) + old, end(s)); - for (int u: sccs.back()) idx[u] = ssize(sccs)-1; - s.resize(old); -}} - -void scc() { - low.assign(ssize(adj), -1); - idx.assign(ssize(adj), -1); - sccs.clear(); - for (int i = 0; i < ssize(adj); i++) { - if (low[i] < 0) visit(i); -}} + if (old == low[v]) { + sccs.emplace_back(begin(s) + old, end(s)); + for (int u: sccs.back()) idx[u] = ssize(sccs)-1; + s.resize(old); + }}; + for (int i = 0; i < ssize(adj); i++) { + if (low[i] < 0) dfs(dfs, i); + }} +}; diff --git a/test/graph/2sat.cpp b/test/graph/2sat.cpp index cf37131..e969364 100644 --- a/test/graph/2sat.cpp +++ b/test/graph/2sat.cpp @@ -25,7 +25,7 @@ struct RandomClause { return false; } - void add(sat2& sat) const { + void add(SAT2& sat) const { int va = a; int vb = b; if (type == 0) sat.addImpl(va, vb); @@ -80,9 +80,8 @@ void stress_test() { vector clauses; for (int i = 0; i < m; i++) clauses.emplace_back(n); - sat2 sat(n); + SAT2 sat(n); for (auto& c : clauses) c.add(sat); - adj = sat.adj; bool got = sat.solve(); bool expected = naive(n, clauses); @@ -113,11 +112,8 @@ void performance_test() { vector clauses; for (int i = 0; i < M; i++) clauses.emplace_back(N); t.start(); - sat2 sat(N); + SAT2 sat(N); for (auto& c : clauses) c.add(sat); - t.stop(); - adj = sat.adj; - t.start(); hash_t hash = sat.solve(); t.stop(); if (t.time > 500) cerr << "too slow: " << t.time << FAIL; diff --git a/test/graph/2sat.cpp.awk b/test/graph/2sat.cpp.awk deleted file mode 100644 index d0215d8..0000000 --- a/test/graph/2sat.cpp.awk +++ /dev/null @@ -1,6 +0,0 @@ -/scc variablen/ { - print; - print "\tvector> adj;"; - next -} -{ print } diff --git a/test/graph/scc.cpp b/test/graph/scc.cpp index 46ad201..bc52d7e 100644 --- a/test/graph/scc.cpp +++ b/test/graph/scc.cpp @@ -9,11 +9,11 @@ void stress_test() { Graph g(n); g.erdosRenyi(m); - adj.assign(n, {}); - g.forEdges([](int a, int b){ + vector> adj(n); + g.forEdges([&](int a, int b){ adj[a].push_back(b); }); - scc(); + SCC scc(adj); auto reach = [&](int a) -> vector { vector seen(n); @@ -29,9 +29,9 @@ void stress_test() { }; vector seen(n); - for (int i = 0; i < ssize(sccs); i++) { - for (int v: sccs[i]) { - if (idx[v] != i) cerr << v << " is in scc " << i << ", but idx[" << v << "] = " << idx[v] << FAIL; + for (int i = 0; i < ssize(scc.sccs); i++) { + for (int v: scc.sccs[i]) { + if (scc.idx[v] != i) cerr << v << " is in scc " << i << ", but idx[" << v << "] = " << scc.idx[v] << FAIL; seen[v]++; } } @@ -40,9 +40,9 @@ void stress_test() { if (seen[a] != 1) cerr << a << " occurs " << seen[a] << " times in sccs" << FAIL; vector reacha = reach(a); for (int b = 0; b < n; b++) { - if (idx[a] == idx[b]) { + if (scc.idx[a] == scc.idx[b]) { if (!reacha[b]) cerr << a << " and " << b << " should be in different SCCs" << FAIL; - } else if (idx[a] < idx[b]) { + } else if (scc.idx[a] < scc.idx[b]) { if (reacha[b]) cerr << a << " should come before " << b << " in topological order" << FAIL; } } @@ -58,16 +58,16 @@ void performance_test() { timer t; Graph g(N); g.erdosRenyi(M); - adj.assign(N, {}); - g.forEdges([](int a, int b){ + vector> adj(N); + g.forEdges([&](int a, int b){ adj[a].push_back(b); }); t.start(); - scc(); + SCC scc(adj); t.stop(); hash_t hash = 0; - for (int x : idx) hash += x; + for (int x : scc.idx) hash += x; if (t.time > 500) cerr << "too slow: " << t.time << FAIL; cerr << "tested performance: " << t.time << "ms (hash: " << hash << ")" << endl; } -- cgit v1.2.3