Differences between revisions 14 and 15
Revision 14 as of 2016-08-19 10:23:34
Size: 4896
Editor: XmlRpcBot
Comment:
Revision 15 as of 2016-08-19 10:43:42
Size: 4894
Editor: XmlRpcBot
Comment:
Deletions are marked like this. Additions are marked like this.
Line 53: Line 53:
 * ''merge_tree'' (Merge Tree): The precomputed merge tree  * ''merge_tree'' (MergeTree): The precomputed merge tree
Line 61: Line 61:
 * ''merge_selector'' (Merge Selector): The merge selector to be used.  * ''merge_selector'' (MergeSelector): The merge selector to be used.

This page describes the various merge strategies supported by the planner.

Merge strategy DFP

This merge strategy implements the algorithm originally described in the paper "Directed model checking with distance-preserving abstractions" by Draeger, Finkbeiner and Podelski (SPIN 2006), adapted to planning in the following paper:

Using this command line option is deprecated, please use the equivalent call: merge_strategy=merge_stateless(merge_selector=score_based_filtering(scoring_functions=[goal_relevance,dfp,total_order(<order_option>))]))if specifying tie-breaking order criteria or: merge_strategy=merge_stateless(merge_selector=score_based_filtering(scoring_functions=[goal_relevance,dfp,single_random()]))if using full random tie-breaking.

merge_dfp(atomic_ts_order=reverse_level, product_ts_order=new_to_old, atomic_before_product=false, random_seed=-1, randomized_order=false)
  • atomic_ts_order ({reverse_level, level, random}): The order in which atomic transition systems are considered when considering pairs of potential merges.

    • reverse_level: the variable order of Fast Downward

    • level: opposite of reverse_level

    • random: a randomized order

  • product_ts_order ({old_to_new, new_to_old, random}): The order in which product transition systems are considered when considering pairs of potential merges.

    • old_to_new: consider composite transition systems from most recent to oldest, that is in decreasing index order

    • new_to_old: opposite of old_to_new

    • random: a randomized order

  • atomic_before_product (bool): Consider atomic transition systems before composite ones iff true.

  • random_seed (int [-1, infinity]): Set to -1 (default) to use the global random number generator. Set to any other value to use a local random number generator with the given seed.

  • randomized_order (bool): If true, use a 'globally' randomized order, i.e. all transition systems are considered in an arbitrary order. This renders all other ordering options void.

Linear merge strategies

These merge strategies implement several linear merge orders, which are described in the paper:

Using this command line option is deprecated, please use the equivalent call: merge_strategy=merge_precomputed(merge_tree=linear(<variable_order>))

merge_linear(random_seed=-1, update_option=use_random, variable_order=CG_GOAL_LEVEL)
  • random_seed (int [-1, infinity]): Set to -1 (default) to use the global random number generator. Set to any other value to use a local random number generator with the given seed.

  • update_option ({use_first, use_second, use_random}): When the merge tree is used within another merge strategy, howshould it be updated when a merge different to a merge from the tree is performed: choose among use_first, use_second, and use_random to choose which node of the tree should survive and represent the new merged index. Specify use_first (use_second) to let the node represententing the index that would have been merged earlier (later) survive. use_random chooses a random node.

  • variable_order ({CG_GOAL_LEVEL, CG_GOAL_RANDOM, GOAL_CG_LEVEL, RANDOM, LEVEL, REVERSE_LEVEL}): the order in which atomic transition systems are merged

Precomputed merge strategy

This merge strategy has a precomputed merge tree. Note that this merge strategy does not take into account the current state of the factored transition system. This also means that this merge strategy relies on the factored transition system being synchronized with this merge tree, i.e. all merges are performed exactly as given by the merge tree.

merge_precomputed(merge_tree)
  • merge_tree (MergeTree): The precomputed merge tree

Stateless merge strategy

This merge strategy has a merge selector, which computes the next merge only depending on the current state of the factored transition system, not requireing any additional information.

merge_stateless(merge_selector)

FastDownward: Doc/MergeStrategy (last edited 2024-01-11 22:26:37 by XmlRpcBot)