This page describes various merge scoring functions. A scoring function, given a list of merge candidates and a factored transition system, computes a score for each candidate based on this information and potentially some chosen options. Minimal scores are considered best. Scoring functions are currently only used within the score based filtering merge selector.

DFP scoring

This scoring function computes the 'DFP' score as 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:

dfp()

Note: To obtain the configurations called DFP-B-50K described in the paper, use the following configuration of the merge-and-shrink heuristic and adapt the tie-breaking criteria of total_order as desired:

merge_and_shrink(merge_strategy=merge_stateless(merge_selector=score_based_filtering(scoring_functions=[goal_relevance,dfp,total_order(atomic_ts_order=reverse_level,product_ts_order=new_to_old,atomic_before_product=true)])),shrink_strategy=shrink_bisimulation(greedy=false),label_reduction=exact(before_shrinking=true,before_merging=false),max_states=50000,threshold_before_merge=1)

Goal relevance scoring

This scoring function assigns a merge candidate a value of 0 iff at least one of the two transition systems of the merge candidate is goal relevant in the sense that there is an abstract non-goal state. All other candidates get a score of positive infinity.

goal_relevance()

MIASM

This scoring function favors merging transition systems such that in their product, there are many dead states, which can then be pruned without sacrificing information. In particular, the score it assigns to a product is the ratio of alive states to the total number of states. To compute this score, this class thus computes the product of all pairs of transition systems, potentially copying and shrinking the transition systems before if otherwise their product would exceed the specified size limits. A stateless merge strategy using this scoring function is called dyn-MIASM (nowadays also called sbMIASM for score-based MIASM) and is described in the following paper:

sf_miasm(shrink_strategy, max_states=-1, max_states_before_merge=-1, threshold_before_merge=-1, use_caching=true)

Note: To obtain the configurations called dyn-MIASM described in the paper, use the following configuration of the merge-and-shrink heuristic and adapt the tie-breaking criteria of total_order as desired:

merge_and_shrink(merge_strategy=merge_stateless(merge_selector=score_based_filtering(scoring_functions=[sf_miasm(shrink_strategy=shrink_bisimulation(greedy=false),max_states=50000,threshold_before_merge=1),total_order(atomic_ts_order=reverse_level,product_ts_order=new_to_old,atomic_before_product=true)])),shrink_strategy=shrink_bisimulation(greedy=false),label_reduction=exact(before_shrinking=true,before_merging=false),max_states=50000,threshold_before_merge=1)

Note: Unless you know what you are doing, we recommend using the same options related to shrinking for sf_miasm as for merge_and_shrink, i.e. the options shrink_strategy, max_states, and threshold_before_merge should be set identically. Furthermore, as this scoring function maximizes the amount of possible pruning, merge-and-shrink should be configured to use full pruning, i.e. prune_unreachable_states=true and prune_irrelevant_states=true (the default).

Single random

This scoring function assigns exactly one merge candidate a score of 0, chosen randomly, and infinity to all others.

single_random(random_seed=-1)

Total order

This scoring function computes a total order on the merge candidates, based on the specified options. The score for each merge candidate correponds to its position in the order. This scoring function is mainly intended as tie-breaking, and has been introduced in the following paper:

Furthermore, using the atomic_ts_order option, this scoring function, if used alone in a score based filtering merge selector, can be used to emulate the corresponding (precomputed) linear merge strategies reverse level/level (independently of the other options).

total_order(atomic_ts_order=reverse_level, product_ts_order=new_to_old, atomic_before_product=false, random_seed=-1)

FastDownward: Doc/MergeScoringFunction (last edited 2024-11-19 13:35:32 by XmlRpcBot)