Improved plan reconstruction by constraining the preimage to the clos…

…ed states. Minor refactoring of transition relations and improved some functions.

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<SymVariables> 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

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 <queue>
 
 namespace symbolic {
@@ -50,6 +52,8 @@ class SymSolutionRegistry {
     std::shared_ptr<PlanSelector> plan_data_base;
     std::shared_ptr<SymTransitionRelations> 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();
+    }
 };
 }
 

src/search/symbolic/search_engines/symbolic_search.cc

@@ -30,7 +30,6 @@ SymbolicSearch::SymbolicSearch(const plugins::Options &opts)
       plan_data_base(opts.get<shared_ptr<PlanSelector>>("plan_selection")),
       solution_registry(make_shared<SymSolutionRegistry>()),
       simple(opts.get<bool>("simple")),
-      single_solution(opts.get<bool>("single_solution")),
       silent(opts.get<bool>("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<int>(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<bool>("silent", "silent mode that avoids writing the cost bounds", "false");
     feature.add_option<bool>("simple", "simple/loopless plan construction", "false");
-    feature.add_option<bool>("single_solution", "search for a single solution", "true");
 }
 }

src/search/symbolic/search_engines/symbolic_search.h

@@ -52,7 +52,6 @@ class SymbolicSearch : public SearchAlgorithm {
     std::shared_ptr<PlanSelector> plan_data_base;
     std::shared_ptr<SymSolutionRegistry> solution_registry; // Solution registry
     bool simple;
-    bool single_solution;
 
     bool silent;
 

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) {

src/search/symbolic/sym_transition_relations.cc

@@ -69,7 +69,7 @@ void SymTransitionRelations::create_single_trs(const shared_ptr<AbstractTask> &t
     // For Conjunctive Transiton Relations in presence of CEs
     shared_ptr<extra_tasks::EffectAggregatedTask> 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<extra_tasks::EffectAggregatedTask>(task);
     }
 
@@ -82,11 +82,6 @@ void SymTransitionRelations::create_single_trs(const shared_ptr<AbstractTask> &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();

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();
     }

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<extra_tasks::EffectAggregatedTask> &task,
@@ -67,107 +61,67 @@ 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<int, int> vars_last_occurance;
+    unordered_map<int, int> vars_bw_last_occurance;
 
-    vector<vector<unsigned int>> trs_supports;
-    for (const auto &tr : transitions) {
-        auto tr_support = tr.get_tr_BDD().SupportIndices();
-        vector<unsigned int> 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<pair<int, vector<unsigned int>>> 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<int> 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<vector<unsigned int>> 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<unsigned int> 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<unsigned int> 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<DisjunctiveTransitionRelation> 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<BDD>(transitions.size(), sym_vars->oneBDD());
+    exists_bw_vars = vector<BDD>(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 {
     BDD res = from;
     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();
     }
 }
 

src/search/symbolic/transition_relations/conjunctive_transition_relation.h

@@ -34,8 +34,7 @@ class ConjunctiveTransitionRelation : public TransitionRelation {
     std::vector<BDD> 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;