maxsat encoding

include/feature_generation/features.hpp

@@ -7,7 +7,7 @@
 #include "../planning/domain.hpp"
 #include "../planning/state.hpp"
 #include "neighbour_container.hpp"
-#include "pruning.hpp"
+#include "pruning/pruning_options.hpp"
 
 #include <map>
 #include <memory>

include/feature_generation/pruning/maxsat.hpp

@@ -0,0 +1,37 @@
+#ifndef FEATURE_GENERATION_PRUNING_MAXSAT_HPP
+#define FEATURE_GENERATION_PRUNING_MAXSAT_HPP
+
+#include <string>
+#include <vector>
+
+namespace feature_generation {
+  struct MaxSatClause {
+    std::vector<int> variables;
+    std::vector<bool> negated;
+    int weight;
+    bool hard;
+
+    MaxSatClause(const std::vector<int> &variables,
+                 const std::vector<bool> &negated,
+                 const int weight,
+                 const bool hard);
+
+    int size() const { return variables.size(); }
+  };
+
+  class MaxSatProblem {
+    std::vector<int> variables;
+    std::vector<MaxSatClause> clauses;
+
+   public:
+    MaxSatProblem(const std::vector<MaxSatClause> &clauses);
+
+    int get_n_variables() const { return variables.size(); }
+    int get_n_clauses() const { return clauses.size(); }
+
+    // https://maxsat-evaluations.github.io/2022/rules.html#input
+    std::string to_string();
+  };
+}  // namespace feature_generation
+
+#endif  // FEATURE_GENERATION_PRUNING_MAXSAT_HPP

include/feature_generation/pruning.hpp → include/feature_generation/pruning/pruning_options.hpp

@@ -1,5 +1,5 @@
-#ifndef FEATURE_GENERATION_PRUNING_HPP
-#define FEATURE_GENERATION_PRUNING_HPP
+#ifndef FEATURE_GENERATION_PRUNING_PRUNING_OPTIONS_HPP
+#define FEATURE_GENERATION_PRUNING_PRUNING_OPTIONS_HPP
 
 #include <string>
 #include <vector>
@@ -15,4 +15,4 @@ namespace feature_generation {
   };
 }  // namespace feature_generation
 
-#endif  // FEATURE_GENERATION_PRUNING_HPP
+#endif  // FEATURE_GENERATION_PRUNING_PRUNING_OPTIONS_HPP

src/feature_generation/features.cpp

@@ -1,6 +1,7 @@
 #include "../../include/feature_generation/features.hpp"
 
 #include "../../include/feature_generation/dependency_graph.hpp"
+#include "../../include/feature_generation/pruning/maxsat.hpp"
 #include "../../include/graph/graph_generator_factory.hpp"
 #include "../../include/utils/nlohmann/json.hpp"
 
@@ -391,8 +392,48 @@ namespace feature_generation {
 
     // 3. maxsat
     std::cout << "Solving MaxSAT optimisation." << std::endl;
-    std::cout << "TODO" << std::endl;
-    // TODO
+    // get groups
+    std::map<int, std::vector<int>> group_to_features;
+    std::vector<int> variables;
+    for (int colour = 0; colour < n_features; colour++) {
+      int group = feature_group.at(colour);
+      if (group != DISTINCT) {
+        if (group_to_features.count(group) == 0) {
+          group_to_features[group] = std::vector<int>();
+        }
+        group_to_features[group].push_back(colour);
+        variables.push_back(colour);
+      }
+    }
+
+    // encode
+    std::vector<MaxSatClause> clauses;
+
+    // variable=T indicates feature to be thrown out
+    // equivalently, ~variable=T indicates feature to be kept
+    for (const int variable : variables) {
+      clauses.push_back(MaxSatClause({variable}, {false}, 1, false));
+    }
+
+    // a thrown out variable forces children to be thrown out
+    // i.e., variable => child_1 & ... & child_n which is equivalent to
+    // (~variable | child_1) & ... & (~variable | child_n)
+    for (const int variable : variables) {
+      for (const int child : fdg.get_fw_edges(variable)) {
+        clauses.push_back(MaxSatClause({variable, child}, {true, false}, 0, true));
+      }
+    }
+
+    // keep one feature from each equivalence group
+    for (const auto &[group, features] : group_to_features) {
+      std::vector<bool> negated(features.size(), true);
+      clauses.push_back(MaxSatClause(features, negated, 0, true));
+    }
+
+    MaxSatProblem max_sat_problem = MaxSatProblem(clauses);
+    std::cout << max_sat_problem.to_string() << std::endl;
+
+    std::cout << "TODO solve the problem" << std::endl;
 
     std::cout << "Equivalent features minimised!" << std::endl;
   }

src/feature_generation/pruning/maxsat.cpp

@@ -0,0 +1,48 @@
+#include "../../../include/feature_generation/pruning/maxsat.hpp"
+
+#include <iostream>
+
+namespace feature_generation {
+  MaxSatClause::MaxSatClause(const std::vector<int> &variables,
+                             const std::vector<bool> &negated,
+                             const int weight,
+                             const bool hard)
+      : variables(variables), negated(negated), weight(weight), hard(hard) {
+    if (hard && weight != 0) {
+      std::cout << "error: hard MaxSAT clauses should have 0 weight!" << std::endl;
+      exit(-1);
+    } else if (!hard && weight < 1) {
+      std::cout << "error: soft MaxSAT clauses should have weight >= 1!" << std::endl;
+      exit(-1);
+    }
+    if (variables.size() != negated.size()) {
+      std::cout << "error: variables and negated in MaxSatClause should have the same size!" << std::endl;
+      exit(-1);
+    }
+  }
+
+  MaxSatProblem::MaxSatProblem(const std::vector<MaxSatClause> &clauses) : clauses(clauses) {
+    // preprocess
+  }
+
+  std::string MaxSatProblem::to_string() {
+    std::string ret = "";
+    for (const MaxSatClause &clause : clauses) {
+      std::string clause_string = "";
+      if (clause.hard) {
+        clause_string += "h ";
+      } else {
+        clause_string += std::to_string(clause.weight) + " ";
+      }
+      for (int i = 0; i < clause.size(); i++) {
+        if (clause.negated[i]) {
+          clause_string += "-";
+        }
+        clause_string += std::to_string(clause.variables[i]) + " ";
+      }
+      clause_string += "0";
+      ret += clause_string + "\n";
+    }
+    return ret;
+  }
+}  // namespace feature_generation

src/feature_generation/pruning.cpp → src/feature_generation/pruning/pruning_options.cpp

@@ -1,4 +1,4 @@
-#include "../../include/feature_generation/pruning.hpp"
+#include "../../../include/feature_generation/pruning/pruning_options.hpp"
 
 namespace feature_generation {
   const std::string PruningOptions::NONE = "none";