From 07a1c4f87dcccbfe2ca4fbbc100a07c9be801502 Mon Sep 17 00:00:00 2001
From: pjungeblut <paul.jungeblut@gmail.com>
Date: Thu, 30 Oct 2014 19:26:30 +0100
Subject: SCCS added, seperated from 2-SAT

---
 sonstiges/.2sat.cpp.kate-swp | Bin 0 -> 325 bytes
 sonstiges/2sat.cpp           |  63 -------------------------------------------
 sonstiges/sonstiges.tex      |   7 ++++-
 3 files changed, 6 insertions(+), 64 deletions(-)
 create mode 100644 sonstiges/.2sat.cpp.kate-swp
 delete mode 100644 sonstiges/2sat.cpp

(limited to 'sonstiges')

diff --git a/sonstiges/.2sat.cpp.kate-swp b/sonstiges/.2sat.cpp.kate-swp
new file mode 100644
index 0000000..b688b2e
Binary files /dev/null and b/sonstiges/.2sat.cpp.kate-swp differ
diff --git a/sonstiges/2sat.cpp b/sonstiges/2sat.cpp
deleted file mode 100644
index 627e484..0000000
--- a/sonstiges/2sat.cpp
+++ /dev/null
@@ -1,63 +0,0 @@
-vector< vector<int> > adjlist; //adjazenzliste
-vector<int> sccs; //speichert die gefundenen SCCs
-vector<bool> visited; //welcher Knoten ist schon besucht worden (in der DFS)
-vector<bool> inStack; //ist Knoten gerade im Stack
-vector<int> d; //discovery time
-vector<int> low; //wie weit hoch geht's im Tiefensuchbaum
-int counter; //Zaehler fuer discovery time
-stack<int> st; //der Stack
-int sccCounter; //Zaehler fuer SCCs
-
-//Tiefensuche, die starke Zusammenhangskomponenten findet
-void visit(int v) {
-	visited[v] = true;
-	d[v] = counter;
-	low[v] = counter;
-	counter++;
-	st.push(v);
-	inStack[v] = true;
-	
-	for (int i = 0; i < (int)adjlist[v].size(); i++) {
-		int w = adjlist[v][i];
-		
-		if (!visited[w]) {
-			visit(w);
-			low[v] = min(low[v], low[w]);
-		} else if (inStack[w]) {
-			low[v] = min(low[v], low[w]);
-		}
-	}
-	
-	if (low[v] == d[v]) {
-		int next;
-		do {
-			next = st.top();
-			st.pop();
-			sccs[next] = sccCounter;
-			inStack[next] = false;
-		} while (next != v);
-		
-		sccCounter++;
-	}
-}
-
-void solve() {
-	//adjlist initialisieren
-	//(a || b) wird zu (!a => b) und (!b => a)
-	
-	visited.clear(); visited.assign(adjlist.size(), false);
-	inStack.clear(); inStack.assign(adjlist.size(), false);
-	d.clear(); d.assign(adjlist.size(), false);
-	low.clear(); low.assign(adjlist.size(), false);
-	sccs.clear(); sccs.resize(adjlist.size());
-	
-	counter = 0;
-	sccCounter = 0;
-	for (i = 0; i < (int)adjlist.size(); i++) {
-		if (!visited[i]) {
-			visit(i);
-			sccCounter++;
-		}
-	}
-	// genau dann loesbar, wenn keine Variable in gleicher SCC wie Negation ist
-}
\ No newline at end of file
diff --git a/sonstiges/sonstiges.tex b/sonstiges/sonstiges.tex
index 0befff3..09ea14c 100644
--- a/sonstiges/sonstiges.tex
+++ b/sonstiges/sonstiges.tex
@@ -1,4 +1,9 @@
 \section{Sonstiges}
 
 \subsection{2-SAT}
-\lstinputlisting{sonstiges/2sat.cpp}
\ No newline at end of file
+\begin{enumerate}
+	\item Bedingungen in 2-CNF formulieren.
+	\item Implikationsgraph bauen, $\left(a \vee b\right)$ wird zu $\neg a \Rightarrow b$ und $\neg b \Rightarrow a$.
+	\item Finde die starken Zusammenhangskomponenten.
+	\item Genau dann lösbar, wenn keine Variable mit ihrer Negation in einer SCC liegt.
+\end{enumerate}
\ No newline at end of file
-- 
cgit v1.2.3