Algorithms : complete 05-advanced_algorithms_and_complexity 03-np-completness

3 files changed, 143 insertions, 21 deletions

diff --git a/05-advanced_algorithms_and_complexity/03-np-completness/01-gsm_network/gsm_network.cpp b/05-advanced_algorithms_and_complexity/03-np-completness/01-gsm_network/gsm_network.cpp
index 5eafa18..ff53c87 100644
--- a/05-advanced_algorithms_and_complexity/03-np-completness/01-gsm_network/gsm_network.cpp
+++ b/05-advanced_algorithms_and_complexity/03-np-completness/01-gsm_network/gsm_network.cpp
@@ -18,14 +18,39 @@ struct ConvertGSMNetworkProblemToSat {
         edges(m)
     {  }
 
+    static inline int var(int vertex, int color) { return vertex * 3 + color; }
+
     void printEquisatisfiableSatFormula() {
-        // This solution prints a simple satisfiable formula
-        // and passes about half of the tests.
-        // Change this function to solve the problem.
-        cout << "3 2" << endl;
-        cout << "1 2 0" << endl;
-        cout << "-1 -2 0" << endl;
-        cout << "1 -2 0" << endl;
+        vector<vector<int>> clauses;
+
+        // 1 color per vertex
+        for (int i = 0; i < numVertices; i++) {
+            // at least one var must be true
+            clauses.push_back({var(i, 1), var(i, 2), var(i, 3)}); // R || G || B
+            // both can't be true
+            clauses.push_back({-var(i, 1), -var(i, 2)});          // !R || !G
+            clauses.push_back({-var(i, 1), -var(i, 3)});          // !R || !B
+            clauses.push_back({-var(i, 2), -var(i, 3)});          // !B || !G
+        }
+
+        // 2 colors per edge
+        for (Edge e : edges) {
+            int from = e.from - 1;
+            int to = e.to - 1;
+            // both can't be true
+            clauses.push_back({-var(from, 1), -var(to, 1)});  // !R || !R
+            clauses.push_back({-var(from, 2), -var(to, 2)});  // !G || !G
+            clauses.push_back({-var(from, 3), -var(to, 3)});  // !B || !B
+        }
+
+        cout << clauses.size() << " " << numVertices * 3 << endl;
+        for (vector<int>& c : clauses) {
+            for (int v : c) {
+                cout << v << " ";
+             }
+             cout << "0" << endl;
+        }
+        cout << endl;
     }
 };
 
diff --git a/05-advanced_algorithms_and_complexity/03-np-completness/02-cleaning_apartment/cleaning_apartment.cpp b/05-advanced_algorithms_and_complexity/03-np-completness/02-cleaning_apartment/cleaning_apartment.cpp
index 5690be7..a205158 100644
--- a/05-advanced_algorithms_and_complexity/03-np-completness/02-cleaning_apartment/cleaning_apartment.cpp
+++ b/05-advanced_algorithms_and_complexity/03-np-completness/02-cleaning_apartment/cleaning_apartment.cpp
@@ -15,14 +15,66 @@ struct ConvertHampathToSat {
         edges(m)
     {  }
 
+    // matrix of vertices * vertices (+1 because 0 is reserved)
+    static inline int var(int v1, int v2, int n) { return 1 + v1 * n + v2; }
+
     void printEquisatisfiableSatFormula() {
-        // This solution prints a simple satisfiable formula
-        // and passes about half of the tests.
-        // Change this function to solve the problem.
-        cout << "3 2" << endl;
-        cout << "1 2 0" << endl;
-        cout << "-1 -2 0" << endl;
-        cout << "1 -2 0" << endl;
+        vector<vector<int>> clauses;
+        vector<int> cstrs;
+
+        for (int i = 0; i < numVertices; i++) {
+            // the vertex belongs to the path, matrix rows
+            cstrs.clear();
+            for (int j = 0; j < numVertices; j++)
+                cstrs.push_back(var(i, j, numVertices));      // (Xi0 || Xi1 || Xi2 ...)
+            clauses.push_back(cstrs);
+
+            // the vertex appears just once in the path
+            for (int j = 0; j < numVertices; j++) {
+                for (int k = j + 1; k < numVertices; k++)
+                    clauses.push_back({-var(i, j, numVertices), -var(i, k, numVertices)});  // ( !Xij && !Xik )
+            }
+
+            // each position in the path has a vertex, matrix cols
+            cstrs.clear();
+            for (int j = 0; j < numVertices; j++)
+                cstrs.push_back(var(j, i, numVertices));      // (X0i || X1i || X2i ...)
+            clauses.push_back(cstrs);
+
+            // each position has only 1 vertex
+            for (int j = 0; j < numVertices; j++) {
+                for (int k = j + 1; k < numVertices; k++)
+                    clauses.push_back({-var(j, i, numVertices), -var(k, i, numVertices)});  // ( !Xji && !Xki )
+            }
+
+            // if there is no ij edje, there is no Xik Xj(k+1) or Xjk Xi(k+1)
+            for (int j = i + 1; j < numVertices; j++) {
+                // would be much faster with an adjacent matrix
+                bool found = false;
+                for (Edge e : edges) {
+                    if ((e.from == i+1 && e.to == j+1) || (e.from == j+1 && e.to == i+1)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    // no v-w edge
+                    for (int k = 0; k < (numVertices - 1); k++) {
+                        clauses.push_back({-var(i, k, numVertices), -var(j, k + 1, numVertices)});  // ( !Xik && !Xj(k+1)
+                        clauses.push_back({-var(j, k, numVertices), -var(i, k + 1, numVertices)});  // ( !Xjk && !Xi(k+1)
+                    }
+                }
+            }
+        }
+
+        cout << clauses.size() << " " << numVertices * numVertices << endl;
+        for (vector<int>& c : clauses) {
+            for (int v : c) {
+                cout << v << " ";
+             }
+             cout << "0" << endl;
+        }
+        cout << endl;
     }
 };
 
diff --git a/05-advanced_algorithms_and_complexity/03-np-completness/03-budget_allocation/budget_allocation.cpp b/05-advanced_algorithms_and_complexity/03-np-completness/03-budget_allocation/budget_allocation.cpp
index d2bfc51..c97937b 100644
--- a/05-advanced_algorithms_and_complexity/03-np-completness/03-budget_allocation/budget_allocation.cpp
+++ b/05-advanced_algorithms_and_complexity/03-np-completness/03-budget_allocation/budget_allocation.cpp
@@ -12,13 +12,58 @@ struct ConvertILPToSat {
     {}
 
     void printEquisatisfiableSatFormula() {
-        // This solution prints a simple satisfiable formula
-        // and passes about half of the tests.
-        // Change this function to solve the problem.
-        cout << "3 2" << endl;
-        cout << "1 2 0" << endl;
-        cout << "-1 -2 0" << endl;
-        cout << "1 -2 0" << endl;
+        int vars = A[0].size();
+        int eqs = A.size();
+        vector<vector<int>> clauses;
+
+        // 5x1 + 2x2 + 3x3 ≤ 6
+        // vector that are no solutions :  (1,1,1)=10, (1,1,0)=7, (1,0,1)=8
+        // corresponding clauses (!x || !y || !z), (!x || !y || z), (!x || y || !z)
+        vector<int> coefficients(vars, -1);
+        for (int i = 0; i < eqs; i++) {
+
+            vector<int> equ = A[i];
+
+            // collect non 0 coefficients
+            coefficients.clear();
+            for (int j = 0; j < vars; j++) {
+                if (equ[j] != 0)  coefficients.push_back(j);
+            }
+
+            vector<int> clause;
+            // for each bit combinaison
+            for (int j = 0; j < (1<<coefficients.size()); j++) {
+
+                // sum the coefficients using the bit map
+                int v = 0;
+                clause.clear();
+                for (int k = 0; k < coefficients.size(); k++) {
+                    bool b = ((j & (1<<k)) > 0);
+                    int w = coefficients[k];
+                    if (b) v += equ[w];
+                    w += 1;
+                    clause.push_back(b ? -w: w);
+                }
+
+                if (v > b[i]) {
+                  clauses.push_back(clause);
+                }
+            }
+        }
+
+        int n = clauses.size();
+        if (n == 0) {
+            cout << "1 1\n1 -1 0"<< endl;
+        } else {
+            cout << clauses.size() << " " << vars << endl;
+            for (vector<int>& c : clauses) {
+                for (int v : c) {
+                    cout << v << " ";
+                }
+                cout << "0" << endl;
+            }
+            cout << endl;
+        }
     }
 };