1 files changed, 72 insertions, 27 deletions

diff --git a/05-advanced_algorithms_and_complexity/04-np-completeness/01-circuit_design/circuit_design.cpp b/05-advanced_algorithms_and_complexity/04-np-completeness/01-circuit_design/circuit_design.cpp
index afc1a9f..2768e93 100644
--- a/05-advanced_algorithms_and_complexity/04-np-completeness/01-circuit_design/circuit_design.cpp
+++ b/05-advanced_algorithms_and_complexity/04-np-completeness/01-circuit_design/circuit_design.cpp
@@ -6,45 +6,90 @@ struct Clause {
     int secondVar;
 };
 
+struct Vertex {
+    int index;
+    int lowLink;
+    bool onStack;
+};
+
 struct TwoSatisfiability {
     int numVars;
+    int x;
     vector<Clause> clauses;
+    stack<int> st;
+    vector<Vertex> vertices;
+    vector<vector<int> > adj;
 
     TwoSatisfiability(int n, int m) :
         numVars(n),
-        clauses(m)
-    {  }
+        clauses(m),
+        x(0),
+        vertices(n * 2, {-1, -1, false}),
+        adj(n * 2, vector<int>())
+    {
+    }
 
-    bool isSatisfiable(vector<int>& result) {
-        // This solution tries all possible 2^n variable assignments.
-        // It is too slow to pass the problem.
-        // Implement a more efficient algorithm here.
-        for (int mask = 0; mask < (1 << numVars); ++mask) {
-            for (int i = 0; i < numVars; ++i) {
-                result[i] = (mask >> i) & 1;
+    // bool tarjan(int &x, int i, vector<int> &result) {
+    bool tarjan(int i, vector<int> &result) {
+        Vertex &v = vertices[i];
+        v.index = x;
+        v.lowLink = x;
+        v.onStack = true;
+        st.push(i);
+        x++;
+        for (int a : adj[i]) {
+            Vertex &w = vertices[a];
+            if (w.index == -1) {
+                if (!tarjan(a, result)) return false;
+                v.lowLink = min(v.lowLink, w.lowLink);
+            } else if (w.onStack) {
+                v.lowLink = min(v.lowLink, w.index);
             }
-
-            bool formulaIsSatisfied = true;
-
-            for (const Clause& clause: clauses) {
-                bool clauseIsSatisfied = false;
-                if (result[abs(clause.firstVar) - 1] == (clause.firstVar < 0)) {
-                    clauseIsSatisfied = true;
-                }
-                if (result[abs(clause.secondVar) - 1] == (clause.secondVar < 0)) {
-                    clauseIsSatisfied = true;
+        }
+        // is a SCC root node
+        if (v.lowLink == v.index) {
+            for (;;) {
+                int i = st.top();
+                int iv = inv(i);
+                if (vertices[iv].index == v.index) return false;
+                st.pop();
+                if (i < numVars) {
+                    if (result[i] == -1)
+                        result[i] = 1;
+                } else {
+                    if (result[iv] == -1)
+                        result[iv] = 0;
                 }
-                if (!clauseIsSatisfied) {
-                    formulaIsSatisfied = false;
+                vertices[i].onStack = false;
+                if (vertices[i].index == v.index) {
                     break;
                 }
             }
+        }
+        return true;
+    }
 
-            if (formulaIsSatisfied) {
-                return true;
+    inline int idx(int v) { return (v > 0 ? (v - 1) : (numVars - v - 1)); }
+    inline int inv(int i) { return i + ((i < numVars) ? numVars : -numVars); }
+
+    bool isSatisfiable(vector<int>& result) {
+
+        // construct the implication graph        (l1 l2) -> !l1 ->l2 !l2->l1
+        for(Clause clause : clauses) {
+            adj[idx(-clause.firstVar)].push_back(idx(clause.secondVar));
+            adj[idx(-clause.secondVar)].push_back(idx(clause.firstVar));
+        }
+
+        // find SCC's of graph
+        // int x = 0;
+        for (int i = 0; i < vertices.size(); i++) {
+            Vertex &v = vertices[i];
+            if (v.index == -1)  {
+                if (!tarjan(i, result)) return false;
             }
         }
-        return false;
+
+        return true;
     }
 };
 
@@ -58,14 +103,14 @@ int main() {
         cin >> twoSat.clauses[i].firstVar >> twoSat.clauses[i].secondVar;
     }
 
-    vector<int> result(n);
+    vector<int> result(n, -1);
     if (twoSat.isSatisfiable(result)) {
         cout << "SATISFIABLE" << endl;
         for (int i = 1; i <= n; ++i) {
             if (result[i-1]) {
-                cout << -i;
-            } else {
                 cout << i;
+            } else {
+                cout << -i;
             }
             if (i < n) {
                 cout << " ";