1 files changed, 52 insertions, 7 deletions
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;
+        }
     }
 };