diff --git a/src/search/symbolic/plan_reconstruction/sym_solution_registry.cc b/src/search/symbolic/plan_reconstruction/sym_solution_registry.cc index 167bee150..57a05b78e 100644 --- a/src/search/symbolic/plan_reconstruction/sym_solution_registry.cc +++ b/src/search/symbolic/plan_reconstruction/sym_solution_registry.cc @@ -114,9 +114,9 @@ void SymSolutionRegistry::expand_actions(const ReconstructionNode &node) { } for (auto tr : it->second) { - BDD succ = fwd ? tr->preimage(node.get_states()) : tr->image(node.get_states()); - BDD closed_states = cur_closed_list->get_closed_at(new_cost); + BDD succ = fwd ? tr->preimage(node.get_states(), closed_states) : tr->image(node.get_states()); + BDD intersection = succ * closed_states; int layer_id = 0; if (op_cost == 0) @@ -224,6 +224,9 @@ void SymSolutionRegistry::init(shared_ptr sym_vars, if (sym_transition_relations->has_unit_cost()) { queue = ReconstructionQueue(CompareReconstructionNodes(ReconstructionPriority::REMAINING_COST)); } + + reconstruction_timer.stop(); + reconstruction_timer.reset(); } void SymSolutionRegistry::register_solution(const SymSolutionCut &solution) { @@ -258,7 +261,9 @@ void SymSolutionRegistry::construct_cheaper_solutions(int bound) { if (plan_cost >= bound || found_all_plans()) break; + reconstruction_timer.resume(); reconstruct_plans(cuts); + reconstruction_timer.stop(); } // Erase handled keys diff --git a/src/search/symbolic/plan_reconstruction/sym_solution_registry.h b/src/search/symbolic/plan_reconstruction/sym_solution_registry.h index 1893f3460..7ce266794 100644 --- a/src/search/symbolic/plan_reconstruction/sym_solution_registry.h +++ b/src/search/symbolic/plan_reconstruction/sym_solution_registry.h @@ -14,6 +14,8 @@ #include "../../state_registry.h" #include "../../task_proxy.h" +#include "../../utils/timer.h" + #include namespace symbolic { @@ -50,6 +52,8 @@ class SymSolutionRegistry { std::shared_ptr plan_data_base; std::shared_ptr sym_transition_relations; + utils::Timer reconstruction_timer; + // We would like to use the prio queue implemented in FD but it requires // integer values as prio and we have a more complex comparision ReconstructionQueue queue; @@ -117,6 +121,10 @@ class SymSolutionRegistry { } return cheapest; } + + double get_reconstruction_time() const { + return reconstruction_timer(); + } }; } diff --git a/src/search/symbolic/search_engines/symbolic_search.cc b/src/search/symbolic/search_engines/symbolic_search.cc index 0928b33dd..29df6dc85 100644 --- a/src/search/symbolic/search_engines/symbolic_search.cc +++ b/src/search/symbolic/search_engines/symbolic_search.cc @@ -30,7 +30,6 @@ SymbolicSearch::SymbolicSearch(const plugins::Options &opts) plan_data_base(opts.get>("plan_selection")), solution_registry(make_shared()), simple(opts.get("simple")), - single_solution(opts.get("single_solution")), silent(opts.get("silent")) { cout << endl; vars->print_options(); @@ -54,6 +53,7 @@ void SymbolicSearch::initialize() { } if (simple) { + utils::g_log << "Plan Reconstruction: Simple (without loops)" << endl; // compute upper cost bound double num_states = 1; for (int var = 0; var < task->get_num_variables(); var++) { @@ -63,7 +63,6 @@ void SymbolicSearch::initialize() { (num_states - 1) * task_properties::get_max_operator_cost(task_proxy); - utils::g_log << "Plan Reconstruction: Simple (without loops)" << endl; upper_bound = static_cast(min((double)upper_bound, max_plan_cost + 1)); utils::g_log << "Maximal plan cost: " << upper_bound << endl; cout << endl; @@ -115,7 +114,7 @@ SearchStatus SymbolicSearch::step() { if (step_num > 0) { utils::g_log << ", dir: " << search->get_last_dir() << flush; } - utils::g_log << ", total time: " << utils::g_timer << ", " << flush; + utils::g_log << ", reconstruction time: " << solution_registry->get_reconstruction_time() << "s" << flush; utils::g_log << endl; } lower_bound_increased = false; @@ -175,6 +174,5 @@ void SymbolicSearch::add_options_to_feature(plugins::Feature &feature) { SymParameters::add_options_to_feature(feature); feature.add_option("silent", "silent mode that avoids writing the cost bounds", "false"); feature.add_option("simple", "simple/loopless plan construction", "false"); - feature.add_option("single_solution", "search for a single solution", "true"); } } diff --git a/src/search/symbolic/search_engines/symbolic_search.h b/src/search/symbolic/search_engines/symbolic_search.h index 16aee5e29..333936688 100644 --- a/src/search/symbolic/search_engines/symbolic_search.h +++ b/src/search/symbolic/search_engines/symbolic_search.h @@ -52,7 +52,6 @@ class SymbolicSearch : public SearchAlgorithm { std::shared_ptr plan_data_base; std::shared_ptr solution_registry; // Solution registry bool simple; - bool single_solution; bool silent; diff --git a/src/search/symbolic/search_engines/symbolic_uniform_cost_search.cc b/src/search/symbolic/search_engines/symbolic_uniform_cost_search.cc index e57418cdf..ed8eebc7b 100644 --- a/src/search/symbolic/search_engines/symbolic_uniform_cost_search.cc +++ b/src/search/symbolic/search_engines/symbolic_uniform_cost_search.cc @@ -58,7 +58,7 @@ void SymbolicUniformCostSearch::initialize() { bw_search ? bw_search->getClosedShared() : nullptr, sym_trs, plan_data_base, - single_solution, + true, simple); if (fw && bw) { @@ -71,7 +71,8 @@ void SymbolicUniformCostSearch::initialize() { SymbolicUniformCostSearch::SymbolicUniformCostSearch( const plugins::Options &opts, bool fw, bool bw, bool alternating) - : SymbolicSearch(opts), fw(fw), bw(bw), alternating(alternating) {} + : SymbolicSearch(opts), fw(fw), bw(bw), alternating(alternating) { +} void SymbolicUniformCostSearch::new_solution(const SymSolutionCut &sol) { if (!solution_registry->found_all_plans() && sol.get_f() < upper_bound) { diff --git a/src/search/symbolic/sym_transition_relations.cc b/src/search/symbolic/sym_transition_relations.cc index 89ea2bea3..890d6c7ce 100644 --- a/src/search/symbolic/sym_transition_relations.cc +++ b/src/search/symbolic/sym_transition_relations.cc @@ -69,7 +69,7 @@ void SymTransitionRelations::create_single_trs(const shared_ptr &t // For Conjunctive Transiton Relations in presence of CEs shared_ptr effect_aggregated_task = nullptr; TaskProxy task_proxy(*task); - if (task_properties::has_conditional_effects(task_proxy)) { + if (is_ce_transition_type_conjunctive(sym_params.ce_transition_type) && task_properties::has_conditional_effects(task_proxy)) { effect_aggregated_task = make_shared(task); } @@ -82,11 +82,6 @@ void SymTransitionRelations::create_single_trs(const shared_ptr &t individual_conj_transitions[cost].emplace_back(sym_vars, OperatorID(i), effect_aggregated_task, early_quantification); individual_conj_transitions[cost].back().init(); - // if (sym_params.mutex_type == MutexType::MUTEX_EDELETION) { - // individual_conj_transitions[cost].back().edeletion(sym_mutexes.notMutexBDDsByFluentFw, - // sym_mutexes.notMutexBDDsByFluentBw, - // sym_mutexes.exactlyOneBDDsByFluent); - // } } else { individual_disj_transitions[cost].emplace_back(sym_vars, OperatorID(i), task); individual_disj_transitions[cost].back().init(); diff --git a/src/search/symbolic/sym_variables.h b/src/search/symbolic/sym_variables.h index 91a2f4107..ada845419 100644 --- a/src/search/symbolic/sym_variables.h +++ b/src/search/symbolic/sym_variables.h @@ -140,6 +140,10 @@ class SymVariables { return getBDDVars(vars, bdd_index_eff); } + inline BDD levelBDD(int level) const { + return manager->bddVar(level); + } + inline BDD zeroBDD() const { return manager->bddZero(); } diff --git a/src/search/symbolic/transition_relations/conjunctive_transition_relation.cc b/src/search/symbolic/transition_relations/conjunctive_transition_relation.cc index 8adc8f4d3..3e82cd557 100644 --- a/src/search/symbolic/transition_relations/conjunctive_transition_relation.cc +++ b/src/search/symbolic/transition_relations/conjunctive_transition_relation.cc @@ -13,12 +13,6 @@ using namespace std; namespace symbolic { -static BDD get_exclusive_support(BDD f, BDD g) { - BDD common, only_f, only_g; - f.ClassifySupport(g, &common, &only_f, &only_g); - return only_f; -} - ConjunctiveTransitionRelation::ConjunctiveTransitionRelation(SymVariables *sym_vars, OperatorID op_id, const shared_ptr &task, @@ -67,100 +61,57 @@ void ConjunctiveTransitionRelation::init_exist_and_swap_vars() { exists_vars.back() = all_exists_vars; exists_bw_vars.back() = all_exists_bw_vars; + + if (early_quantification) { + set_early_exists_vars(); + } } -void ConjunctiveTransitionRelation::sort_transition_relations() { - auto support = all_exists_vars.SupportIndices(); +void ConjunctiveTransitionRelation::set_early_exists_vars() { + unordered_map vars_last_occurance; + unordered_map vars_bw_last_occurance; - vector> trs_supports; - for (const auto &tr : transitions) { - auto tr_support = tr.get_tr_BDD().SupportIndices(); - vector tr_exist_support; - set_intersection(tr_support.begin(), tr_support.end(), support.begin(), support.end(), back_inserter(tr_exist_support)); - trs_supports.push_back(tr_exist_support); + for (int bdd_var_level : all_exists_vars.SupportIndices()) { + vars_last_occurance[bdd_var_level] = -1; + } + for (int bdd_var_level : all_exists_bw_vars.SupportIndices()) { + vars_bw_last_occurance[bdd_var_level] = -1; } - assert(trs_supports.size() == transitions.size()); - - vector>> enumerated_trs_supports; - transform(trs_supports.begin(), trs_supports.end(), back_inserter(enumerated_trs_supports), - [i = size_t(0)](const auto &elem) mutable {return make_pair(i++, elem);}); - - vector new_tr_order; - - while (!enumerated_trs_supports.empty()) { - size_t best_id = 0; - size_t max_exclusive_vars = 0; - - // unioned support without tr i - vector> trs_others_supports(enumerated_trs_supports.size()); - for (size_t i = 0; i < enumerated_trs_supports.size(); ++i) { - for (size_t j = 0; j < enumerated_trs_supports.size(); ++j) { - if (i != j) { - vector new_set; - set_union(trs_others_supports[j].begin(), trs_others_supports[j].end(), - trs_supports[j].begin(), trs_supports[j].end(), back_inserter(new_set)); - trs_others_supports[j] = new_set; - } + + // Track the last occurrence of each variable in the transitions + for (size_t tr_id = 0; tr_id < transitions.size(); ++tr_id) { + const auto &tr = transitions[tr_id]; + for (int bdd_var_level : tr.get_tr_BDD().SupportIndices()) { + if (vars_last_occurance.count(bdd_var_level)) { + vars_last_occurance[bdd_var_level] = tr_id; } } - - for (size_t i = 0; i < enumerated_trs_supports.size(); ++i) { - const auto &cur_support = enumerated_trs_supports[i].second; - const auto &others_support = trs_others_supports[i]; - vector difference; - set_difference(cur_support.begin(), cur_support.end(), - others_support.begin(), others_support.end(), back_inserter(difference)); - if (difference.size() > max_exclusive_vars) { - max_exclusive_vars = difference.size(); - best_id = i; + for (int bdd_var_level : tr.get_tr_BDD().SupportIndices()) { + if (vars_bw_last_occurance.count(bdd_var_level)) { + vars_bw_last_occurance[bdd_var_level] = tr_id; } } - - new_tr_order.push_back(enumerated_trs_supports[best_id].first); - enumerated_trs_supports.erase(enumerated_trs_supports.begin() + best_id); } - vector new_transitions; - for (int index : new_tr_order) { - new_transitions.push_back(transitions[index]); - } - assert(transitions.size() == new_transitions.size()); - transitions = new_transitions; -} - -void ConjunctiveTransitionRelation::set_early_exists_and_swap_vars() { - // utils::g_log << "Support sizes: [ "; - BDD remaining_exits_vars = all_exists_vars; - BDD remaining_exits_bw_vars = all_exists_bw_vars; - - for (size_t tr1_id = 0; tr1_id < transitions.size(); ++tr1_id) { - BDD tr1_exist_vars = remaining_exits_vars; - BDD tr1_exist_bw_vars = remaining_exits_bw_vars; + // Initialize the BDD vectors with the one BDDs + exists_vars = vector(transitions.size(), sym_vars->oneBDD()); + exists_bw_vars = vector(transitions.size(), sym_vars->oneBDD()); - for (size_t tr2_id = tr1_id + 1; tr2_id < transitions.size(); ++tr2_id) { - tr1_exist_vars = get_exclusive_support(tr1_exist_vars, transitions[tr2_id].get_tr_BDD()); - tr1_exist_bw_vars = get_exclusive_support(tr1_exist_bw_vars, transitions[tr2_id].get_tr_BDD()); + // Add the exist variable to the last TR having the variable in the support + for (auto [bdd_var_level, tr_id] : vars_last_occurance) { + if (tr_id != -1) { + exists_vars[tr_id] *= sym_vars->levelBDD(bdd_var_level); + } else { + exists_vars[0] *= sym_vars->levelBDD(bdd_var_level); + } + } + for (auto [bdd_var_level, tr_id] : vars_bw_last_occurance) { + if (tr_id != -1) { + exists_bw_vars[tr_id] *= sym_vars->levelBDD(bdd_var_level); + } else { + exists_bw_vars[0] *= sym_vars->levelBDD(bdd_var_level); } - assert(tr1_exist_vars.IsCube()); - assert(tr1_exist_bw_vars.IsCube()); - - remaining_exits_vars = get_exclusive_support(remaining_exits_vars, tr1_exist_vars); - remaining_exits_bw_vars = get_exclusive_support(remaining_exits_bw_vars, tr1_exist_bw_vars); - - exists_vars[tr1_id] = tr1_exist_vars; - exists_bw_vars[tr1_id] = tr1_exist_bw_vars; - - // utils::g_log << tr1_exist_vars.nodeCount() << ":" << tr1_exist_bw_vars.nodeCount() << " "; } - // utils::g_log << "]" << endl; -} - -BDD ConjunctiveTransitionRelation::image(const BDD &from) const { - return image(from, 0U); -} - -BDD ConjunctiveTransitionRelation::preimage(const BDD &from) const { - return preimage(from, 0U); } BDD ConjunctiveTransitionRelation::image(const BDD &from, int max_nodes) const { @@ -168,6 +119,9 @@ BDD ConjunctiveTransitionRelation::image(const BDD &from, int max_nodes) const { for (size_t tr_id = 0; tr_id < transitions.size(); ++tr_id) { const auto &tr = transitions[tr_id]; res = res.AndAbstract(tr.get_tr_BDD(), exists_vars[tr_id], max_nodes); + if (res.IsZero()) { + return res; + } } // res = res.ExistAbstract(all_exists_vars); res = res.SwapVariables(all_swap_vars, all_swap_vars_p); @@ -180,16 +134,33 @@ BDD ConjunctiveTransitionRelation::preimage(const BDD &from, int max_nodes) cons for (size_t tr_id = 0; tr_id < transitions.size(); ++tr_id) { const auto &tr = transitions[tr_id]; res = res.AndAbstract(tr.get_tr_BDD(), exists_bw_vars[tr_id], max_nodes); + if (res.IsZero()) { + return res; + } } // res = res.ExistAbstract(all_exists_bw_vars); return res; } +BDD ConjunctiveTransitionRelation::preimage(const BDD &from, const BDD &constraint_to, int max_nodes) const { + BDD res = from; + res = res.SwapVariables(all_swap_vars, all_swap_vars_p); + res *= constraint_to; + for (size_t tr_id = 0; tr_id < transitions.size(); ++tr_id) { + const auto &tr = transitions[tr_id]; + res = res.AndAbstract(tr.get_tr_BDD(), exists_bw_vars[tr_id], max_nodes); + if (res.IsZero()) { + return res; + } + } + return res; +} + void ConjunctiveTransitionRelation::merge_transitions(int max_time, int max_nodes) { merge(sym_vars, transitions, conjunctive_tr_merge, max_time, max_nodes); init_exist_and_swap_vars(); if (early_quantification) { - set_early_exists_and_swap_vars(); + set_early_exists_vars(); } } diff --git a/src/search/symbolic/transition_relations/conjunctive_transition_relation.h b/src/search/symbolic/transition_relations/conjunctive_transition_relation.h index cd7666f4b..2710cac65 100644 --- a/src/search/symbolic/transition_relations/conjunctive_transition_relation.h +++ b/src/search/symbolic/transition_relations/conjunctive_transition_relation.h @@ -34,8 +34,7 @@ class ConjunctiveTransitionRelation : public TransitionRelation { std::vector all_swap_vars, all_swap_vars_p; // Swap variables from unprimed to primed void init_exist_and_swap_vars(); - void sort_transition_relations(); - void set_early_exists_and_swap_vars(); + void set_early_exists_vars(); public: ConjunctiveTransitionRelation(SymVariables *sym_vars, @@ -44,10 +43,9 @@ class ConjunctiveTransitionRelation : public TransitionRelation { bool early_quantification); void init(); - BDD image(const BDD &from) const override; - BDD preimage(const BDD &from) const override; - BDD image(const BDD &from, int max_nodes) const override; - BDD preimage(const BDD &from, int max_nodes) const override; + BDD image(const BDD &from, int max_nodes = 0U) const override; + BDD preimage(const BDD &from, int max_nodes = 0U) const override; + BDD preimage(const BDD &from, const BDD &constraint_to, int max_nodes = 0U) const override; virtual int nodeCount() const override; diff --git a/src/search/symbolic/transition_relations/disjunctive_transition_relation.cc b/src/search/symbolic/transition_relations/disjunctive_transition_relation.cc index 510e339df..70f9f50f1 100644 --- a/src/search/symbolic/transition_relations/disjunctive_transition_relation.cc +++ b/src/search/symbolic/transition_relations/disjunctive_transition_relation.cc @@ -109,14 +109,6 @@ void DisjunctiveTransitionRelation::add_condition(BDD cond) { tr_bdd *= cond; } -BDD DisjunctiveTransitionRelation::image(const BDD &from) const { - return image(from, 0U); -} - -BDD DisjunctiveTransitionRelation::preimage(const BDD &from) const { - return preimage(from, 0U); -} - BDD DisjunctiveTransitionRelation::image(const BDD &from, int maxNodes) const { BDD aux = from; BDD tmp = tr_bdd.AndAbstract(aux, exists_vars, maxNodes); @@ -130,6 +122,13 @@ BDD DisjunctiveTransitionRelation::preimage(const BDD &from, int maxNodes) const return res; } +BDD DisjunctiveTransitionRelation::preimage(const BDD &from, const BDD &constraint_to, int maxNodes) const { + BDD tmp = from.SwapVariables(swap_vars, swap_vars_p); + tmp *= constraint_to; + BDD res = tr_bdd.AndAbstract(tmp, exists_bw_vars, maxNodes); + return res; +} + int DisjunctiveTransitionRelation::nodeCount() const { return tr_bdd.nodeCount(); } diff --git a/src/search/symbolic/transition_relations/disjunctive_transition_relation.h b/src/search/symbolic/transition_relations/disjunctive_transition_relation.h index 3ad26c7df..09927406a 100644 --- a/src/search/symbolic/transition_relations/disjunctive_transition_relation.h +++ b/src/search/symbolic/transition_relations/disjunctive_transition_relation.h @@ -38,10 +38,9 @@ class DisjunctiveTransitionRelation : public TransitionRelation { void add_condition(BDD cond); - BDD image(const BDD &from) const override; - BDD preimage(const BDD &from) const override; - BDD image(const BDD &from, int max_nodes) const override; - BDD preimage(const BDD &from, int max_nodes) const override; + BDD image(const BDD &from, int max_nodes = 0U) const override; + BDD preimage(const BDD &from, int max_nodes = 0U) const override; + BDD preimage(const BDD &from, const BDD &constraint_to, int max_nodes = 0U) const override; virtual int nodeCount() const override; const OperatorID &get_unique_operator_id() const override; diff --git a/src/search/symbolic/transition_relations/transition_relation.h b/src/search/symbolic/transition_relations/transition_relation.h index 1cc2a2850..d92b1e411 100644 --- a/src/search/symbolic/transition_relations/transition_relation.h +++ b/src/search/symbolic/transition_relations/transition_relation.h @@ -15,10 +15,9 @@ class TransitionRelation { virtual ~TransitionRelation() = default; - virtual BDD image(const BDD &from) const = 0; - virtual BDD preimage(const BDD &from) const = 0; - virtual BDD image(const BDD &from, int maxNodes) const = 0; - virtual BDD preimage(const BDD &from, int maxNodes) const = 0; + virtual BDD image(const BDD &from, int maxNodes = 0U) const = 0; + virtual BDD preimage(const BDD &from, int maxNodes = 0U) const = 0; + virtual BDD preimage(const BDD &from, const BDD &constraint_to, int max_nodes = 0U) const = 0; // It's important to retain the name "nodeCount" as BDDs share the same functionality, // allowing us to utilize it within the templated merge functions. diff --git a/src/search/tasks/effect_aggregated_task.cc b/src/search/tasks/effect_aggregated_task.cc index 2dcb9124a..1f5b6fff1 100644 --- a/src/search/tasks/effect_aggregated_task.cc +++ b/src/search/tasks/effect_aggregated_task.cc @@ -57,7 +57,6 @@ EffectAggregatedTask::EffectAggregatedTask(const shared_ptr &paren local_to_parent_op_id.push_back(op_index); local_to_parent_eff_ids.push_back(effect); } - assert(local_to_parent_op_id.size() == local_to_parent_op_id.size()); } string EffectAggregatedTask::get_operator_cost_function(int index, bool is_axiom) const {