diff --git a/include/feature_generation/features.hpp b/include/feature_generation/features.hpp index 8231bb4..8bec94e 100644 --- a/include/feature_generation/features.hpp +++ b/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 #include diff --git a/include/feature_generation/pruning/maxsat.hpp b/include/feature_generation/pruning/maxsat.hpp new file mode 100644 index 0000000..55e9f71 --- /dev/null +++ b/include/feature_generation/pruning/maxsat.hpp @@ -0,0 +1,37 @@ +#ifndef FEATURE_GENERATION_PRUNING_MAXSAT_HPP +#define FEATURE_GENERATION_PRUNING_MAXSAT_HPP + +#include +#include + +namespace feature_generation { + struct MaxSatClause { + std::vector variables; + std::vector negated; + int weight; + bool hard; + + MaxSatClause(const std::vector &variables, + const std::vector &negated, + const int weight, + const bool hard); + + int size() const { return variables.size(); } + }; + + class MaxSatProblem { + std::vector variables; + std::vector clauses; + + public: + MaxSatProblem(const std::vector &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 diff --git a/include/feature_generation/pruning.hpp b/include/feature_generation/pruning/pruning_options.hpp similarity index 65% rename from include/feature_generation/pruning.hpp rename to include/feature_generation/pruning/pruning_options.hpp index fa31c45..fe5f4a6 100644 --- a/include/feature_generation/pruning.hpp +++ b/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 #include @@ -15,4 +15,4 @@ namespace feature_generation { }; } // namespace feature_generation -#endif // FEATURE_GENERATION_PRUNING_HPP +#endif // FEATURE_GENERATION_PRUNING_PRUNING_OPTIONS_HPP diff --git a/src/feature_generation/features.cpp b/src/feature_generation/features.cpp index 83f0461..65f6783 100644 --- a/src/feature_generation/features.cpp +++ b/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> group_to_features; + std::vector 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(); + } + group_to_features[group].push_back(colour); + variables.push_back(colour); + } + } + + // encode + std::vector 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 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; } diff --git a/src/feature_generation/pruning/maxsat.cpp b/src/feature_generation/pruning/maxsat.cpp new file mode 100644 index 0000000..371da3d --- /dev/null +++ b/src/feature_generation/pruning/maxsat.cpp @@ -0,0 +1,48 @@ +#include "../../../include/feature_generation/pruning/maxsat.hpp" + +#include + +namespace feature_generation { + MaxSatClause::MaxSatClause(const std::vector &variables, + const std::vector &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 &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 diff --git a/src/feature_generation/pruning.cpp b/src/feature_generation/pruning/pruning_options.cpp similarity index 84% rename from src/feature_generation/pruning.cpp rename to src/feature_generation/pruning/pruning_options.cpp index 0825084..0e5cc98 100644 --- a/src/feature_generation/pruning.cpp +++ b/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";