From 5ab8a5088b729a9953b8dff1b2a985dc8fb2098b Mon Sep 17 00:00:00 2001
From: mzuenni <michi.zuendorf@gmail.com>
Date: Mon, 27 Jun 2022 17:19:28 +0200
Subject: updated tcr

---
 graph/2sat.cpp | 60 +++++++++++++++-------------------------------------------
 1 file changed, 15 insertions(+), 45 deletions(-)

(limited to 'graph/2sat.cpp')

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;
 	}
 
-- 
cgit v1.2.3