summaryrefslogtreecommitdiff
path: root/graph/2sat.cpp
diff options
context:
space:
mode:
authormzuenni <michi.zuendorf@gmail.com>2022-06-27 17:19:28 +0200
committermzuenni <michi.zuendorf@gmail.com>2022-06-27 17:19:28 +0200
commit5ab8a5088b729a9953b8dff1b2a985dc8fb2098b (patch)
treeed40d6936c0e9eee40ba62751cbf99ecddbaddc2 /graph/2sat.cpp
parentadabbad9c51cf7cd3874bfde8eac1fbcf84fec10 (diff)
updated tcr
Diffstat (limited to 'graph/2sat.cpp')
-rw-r--r--graph/2sat.cpp60
1 files changed, 15 insertions, 45 deletions
diff --git a/graph/2sat.cpp b/graph/2sat.cpp
index ab38b02..2ebb11a 100644
--- a/graph/2sat.cpp
+++ b/graph/2sat.cpp
@@ -1,58 +1,28 @@
struct sat2 {
- vector<vector<int>> adjlist, sccs;
- vector<bool> visited, inStack;
- int n, sccCounter, dfsCounter;
- vector<int> d, low, idx, sol;
- stack<int> s;
+ int n; // + scc variablen
+ vector<int> sol;
- sat2(int vars) : n(vars*2) { adjlist.resize(n); };
+ sat2(int vars) : n(vars*2), adjlist(vars*2) {};
- static int var(int i) { return i << 1; }
+ static int var(int i) {return i << 1;}
void addImpl(int v1, int v2) {
adjlist[v1].push_back(v2);
adjlist[1^v2].push_back(1^v1);
}
- void addEquiv(int v1, int v2) { addImpl(v1, v2); addImpl(v2, v1); }
- void addOr(int v1, int v2) { addImpl(1^v1, v2); }
- void addXor(int v1, int v2) { addOr(v1, v2); addOr(1^v1, 1^v2); }
- void addTrue(int v1) { addImpl(1^v1, v1); }
- void addFalse(int v1) { addTrue(1^v1); }
- void addAnd(int v1, int v2) { addTrue(v1); addTrue(v2); }
- void addNand(int v1, int v2) { addOr(1^v1, 1^v2); }
-
- void dfs(int v) {
- visited[v] = true;
- d[v] = low[v] = dfsCounter++;
- s.push(v); inStack[v] = true;
-
- for (auto w : adjlist[v]) {
- if (!visited[w]) {
- dfs(w);
- low[v] = min(low[v], low[w]);
- } else if (inStack[w]) low[v] = min(low[v], low[w]);
- }
-
- if (d[v] == low[v]) {
- sccs.push_back(vector<int>());
- int w;
- do {
- w = s.top(); s.pop(); inStack[w] = false;
- idx[w] = sccCounter;
- sccs[sccCounter].push_back(w);
- } while (w != v);
- sccCounter++;
- }}
+ void addEquiv(int v1, int v2) {addImpl(v1, v2); addImpl(v2, v1);}
+ void addOr(int v1, int v2) {addImpl(1^v1, v2);}
+ void addXor(int v1, int v2) {addOr(v1, v2); addOr(1^v1, 1^v2);}
+ void addTrue(int v1) {addImpl(1^v1, v1);}
+ void addFalse(int v1) {addTrue(1^v1);}
+ void addAnd(int v1, int v2) {addTrue(v1); addTrue(v2);}
+ void addNand(int v1, int v2) {addOr(1^v1, 1^v2);}
bool solvable() {
- visited.assign(n, false);
- inStack.assign(n, false);
- d.assign(n, -1);
- low.assign(n, -1);
- idx.assign(n, -1);
- sccCounter = dfsCounter = 0;
- for (int i = 0; i < n; i++) if (!visited[i]) dfs(i);
- for (int i = 0; i < n; i += 2) if (idx[i] == idx[i + 1]) return false;
+ scc(); //scc code von oben
+ for (int i = 0; i < n; i += 2) {
+ if (idx[i] == idx[i + 1]) return false;
+ }
return true;
}