diff --git a/src/search/landmarks/landmark_heuristic.cc b/src/search/landmarks/landmark_heuristic.cc index 5031c29d1e..9cfb134b6c 100644 --- a/src/search/landmarks/landmark_heuristic.cc +++ b/src/search/landmarks/landmark_heuristic.cc @@ -35,13 +35,12 @@ void LandmarkHeuristic::initialize(const plugins::Options &opts) { However, there is currently no good way to do this, so we use this incomplete, slightly less safe test. */ - // TODO: update comment and cerr message if (task != tasks::g_root_task && dynamic_cast(task.get()) == nullptr && dynamic_cast(task.get()) == nullptr) { cerr << "The landmark heuristics currently only support " << "task transformations that modify the operator costs " - "or add negated axioms.See issues 845 and 686 " + "or add negated axioms. See issues 845 and 686 " "for details." << endl; utils::exit_with(utils::ExitCode::SEARCH_UNSUPPORTED); } diff --git a/src/search/tasks/negated_axioms_task.cc b/src/search/tasks/negated_axioms_task.cc index da0989d0f9..3ae288b5fd 100644 --- a/src/search/tasks/negated_axioms_task.cc +++ b/src/search/tasks/negated_axioms_task.cc @@ -13,25 +13,6 @@ using namespace std; using utils::ExitCode; -/* - This task transformation adds explicit axioms for how the default value - of derived variables can be achieved. In general this is done as follows: - Given derived variable v with n axioms v <- c_1, ..., v <- c_n, add axioms - that together represent ¬v <- ¬c_1 ^ ... ^ ¬c_n. - - Notes: - - THE TRANSFORMATION CAN BE SLOW! The rule ¬v <- ¬c_1 ^ ... ^ ¬c_n must - be split up into axioms whose conditions are simple conjunctions. Since - all c_i are also simple conjunctions, this amounts to converting a CNF - to a DNF. - - The tranformation is not exact. For derived variables v that have cyclic - dependencies, the general approach is incorrect. We instead trivially - overapproximate such cases with the axiom ¬v <- T. - - The search ignores axioms that set the derived variable to their default - value. The task transformation is thus only meant for heuristics that need - to know how to achieve the default value. - */ - namespace tasks { NegatedAxiomsTask::NegatedAxiomsTask( const shared_ptr &parent, @@ -125,23 +106,25 @@ NegatedAxiomsTask::NegatedAxiomsTask( /* Collect for which derived variables it is relevant to know how they - can become false. - In general a derived variable v is needed negatively if + can obtain their default value. + In general a derived variable v is "needed negatively" (that is, in + its default value) if (a) v appears negatively in the goal or an operator condition (b) v appears positively in the body of an axiom for a variable v' that is needed negatively (c) v appears negatively in the body of an axiom for a variable v' that is needed positively. - We will however not consider case (b) if v' is in an scc with size>1. - This is because for such v' we overapproximate the axioms for ¬v by - the trivial v' <- T, meaning v is actually not needed for these rules. - */ + We will however not consider case (b) if we already know that the + axioms for the default value of v' will be trivially overapproximated + with an empty body (in this case, the default value of v' does not + depend on anything). +*/ unordered_set NegatedAxiomsTask::collect_needed_negatively( const vector> &positive_dependencies, const vector> &negative_dependencies, const vector *> &var_to_scc) { // Stores which derived variables are needed positively or negatively. - set> needed; + utils::HashSet> needed; TaskProxy task_proxy(*parent); @@ -248,7 +231,7 @@ void NegatedAxiomsTask::add_negated_axioms_for_var( // We can see multiplying out the cnf as collecting all hitting sets. set current; - set current_vars; + unordered_set current_vars; set> hitting_sets; collect_non_dominated_hitting_sets_recursively( conditions_as_cnf, 0, current, current_vars, hitting_sets); @@ -262,11 +245,11 @@ void NegatedAxiomsTask::add_negated_axioms_for_var( void NegatedAxiomsTask::collect_non_dominated_hitting_sets_recursively( const vector> &conditions_as_cnf, size_t index, - set &hitting_set, set &hitting_set_vars, + set &hitting_set, unordered_set &hitting_set_vars, set> &results) { if (index == conditions_as_cnf.size()) { /* - Check whether the hitting set denoted in hitting set is dominated. + Check whether the hitting set denoted in hitting_set is dominated. If we find a fact f in hitting set such that no conjunction in the cnf is covered by *only* f, then we could remove f and the resulting set would still be a hitting set that dominates the @@ -291,8 +274,8 @@ void NegatedAxiomsTask::collect_non_dominated_hitting_sets_recursively( const set &conditions = conditions_as_cnf[index]; for (const FactPair &elem : conditions) { /* - The current condition is covered with the current hitting set - elements, we continue with the next condition. + If the current condition is covered with the current hitting + set elements, we continue with the next condition. */ if (hitting_set.find(elem) != hitting_set.end()) { collect_non_dominated_hitting_sets_recursively( diff --git a/src/search/tasks/negated_axioms_task.h b/src/search/tasks/negated_axioms_task.h index 45e225319f..5ea461761a 100644 --- a/src/search/tasks/negated_axioms_task.h +++ b/src/search/tasks/negated_axioms_task.h @@ -9,6 +9,29 @@ namespace plugins { class Options; } +/* + This task transformation adds explicit axioms for how the default value + of derived variables can be achieved. In general this is done as follows: + Given derived variable v with n axioms v <- c_1, ..., v <- c_n, add axioms + that together represent ¬v <- ¬c_1 ^ ... ^ ¬c_n. + + Notes: + - THE TRANSFORMATION CAN BE SLOW! The rule ¬v <- ¬c_1 ^ ... ^ ¬c_n must + be split up into axioms whose conditions are simple conjunctions. Since + all c_i are also simple conjunctions, this amounts to converting a CNF + to a DNF. + - To address the potential exponential blowup, we provide an option + to instead add trivial default values axioms, i.e. axioms that assign + the default value and have an empty body. This guarantees short runtime + but loses information. + - The transformation is not exact. For derived variables v that have cyclic + dependencies, the general approach is incorrect. We instead trivially + overapproximate such cases with an axiom with an empty body. + - The search ignores axioms that set the derived variable to their default + value. The task transformation is thus only meant for heuristics that need + to know how to achieve the default value. + */ + namespace tasks { struct NegatedAxiom { FactPair head; @@ -31,7 +54,8 @@ class NegatedAxiomsTask : public DelegatingTask { FactPair head, std::vector &axiom_ids); void collect_non_dominated_hitting_sets_recursively( const std::vector> &conditions_as_cnf, size_t index, - std::set &hitting_set, std::set &hitting_set_vars, + std::set &hitting_set, + std::unordered_set &hitting_set_vars, std::set> &results); public: explicit NegatedAxiomsTask(