Algorithms : complete 05-advanced_algorithms_and_complexity 03-np-completness

1 files changed, 59 insertions, 7 deletions

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;
     }
 };