diff options
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; + } } }; |