diff --git a/UNSOLVABILITY.md b/UNSOLVABILITY.md new file mode 100644 index 0000000000..3ec84c4498 --- /dev/null +++ b/UNSOLVABILITY.md @@ -0,0 +1,153 @@ +# Reporting unsolvability + +This document describes how Fast Downward detects and reports that a planning +task has **no solution**, what information the planner gives you in each case, +and what changed in the `unsolvability-reporting` branch. + +Unsolvability can be discovered in two places: + +1. **The translator** (`src/translate/`), during preprocessing, before any + search runs. +2. **The search component** (`src/search/`), either while building a heuristic + or while exploring the state space. + +Both layers communicate the outcome through the planner's **exit code**. + +## Exit codes + +| Code | Name | Message | Meaning | +|------|------|---------|---------| +| 10 | `TRANSLATE_UNSOLVABLE` | *(translator prints a reason, see below)* | The translator proved unsolvability during preprocessing. | +| 11 | `SEARCH_UNSOLVABLE` | `Task is provably unsolvable.` | The search proved that no plan exists (within the current cost bound, if one is set). | +| 12 | `SEARCH_UNSOLVED_INCOMPLETE` | `Search stopped without finding a solution.` | No plan was found, but unsolvability could **not** be proven (the algorithm is incomplete, gave up, or pruned states unsoundly). | + +The full list of exit codes lives in `driver/returncodes.py`. + +> **What changed:** previously, exit codes 10 and 11 were almost never emitted +> for a task that "just" turned out to be unsolvable. The translator always +> wrote a trivially-unsolvable task and exited `0`; standard search (A\*, lazy +> search, …) reported `12` even after *exhaustively* proving unsolvability. +> Now the translator exits `10`, and an exhaustive search reports `11` whenever +> the proof is sound (see [Soundness](#soundness-when-is-exhaustion-a-proof)). + +## Translator reasons (exit code 10) + +When the translator detects unsolvability it prints a one-line reason, emits a +trivially-unsolvable SAS task (so the search component still behaves as before +if it is run on the file directly), and exits with `TRANSLATE_UNSOLVABLE` (10). +All four cases funnel through `unsolvable_sas_task()` in +`src/translate/main.py`. + +| Reason | When it triggers | Reported detail | +|--------|------------------|-----------------| +| **No relaxed solution** | The goal is unreachable even in the delete relaxation (the strongest "easy" reachability check). | **Lists the positive goal atoms that are not relaxed reachable** (and are not already true in the initial state). | +| **Goal violates a mutex** | Two goal facts can never hold simultaneously according to the discovered mutex groups. | **Names the pair of mutually exclusive goal atoms.** | +| **Trivially false goal** | The instantiated goal collapses to "impossible" because of static facts (e.g. a negated static atom that always holds). See issue1055. | Clarifying message describing the static-false goal. | +| **Simplified to trivially false goal** | While filtering unreachable propositions, the goal becomes contradictory (`simplify.Impossible`). | Message identifying the simplification step. | + +> **What changed:** all four reasons existed before, but they were printed as +> bare strings ("No relaxed solution", "Goal violates a mutex", …) and the +> translator exited `0`. The branch (a) propagates the dedicated exit code +> `10`, and (b) enriches the first two reasons with the concrete offending +> atoms. The detail is computed read-only and never affects the translation. + +Example output: + +``` +No relaxed solution: the following goal atoms are not reachable even in the +delete relaxation: Atom q()! Generating unsolvable task... +``` + +``` +Goal violates a mutex: the goal atoms Atom at(b) and Atom at(c) are mutually +exclusive! Generating unsolvable task... +``` + +## Search reasons + +The search component can report unsolvability in two fundamentally different +ways. + +### 1. Unsolvability proven while building a heuristic + +Several heuristics analyse (an abstraction of) the task before search begins +and can already prove that no plan exists: + +* **Pattern database CEGAR** (`pdbs/cegar.cc`) calls + `exit_with(SEARCH_UNSOLVABLE)` directly when a pattern's projection is + unsolvable. +* **Merge-and-shrink** (`merge_and_shrink/merge_and_shrink_heuristic.cc`) + extracts an *unsolvable factor* and uses it as the heuristic; it then returns + `DEAD_END` for the initial state. +* **Cartesian abstractions** (`cartesian_abstractions/cegar.cc`) report + "Abstract task is unsolvable" and the resulting heuristic is infinite on the + initial state. +* Any **admissible heuristic** (`lmcut`, `hmax`, PDBs, landmark heuristics, + merge-and-shrink, Cartesian, …) that returns `DEAD_END` / infinity for the + initial state effectively proves unsolvability, because for these heuristics + dead ends are *reliable*. + +In the heuristic-returns-dead-end cases, the search opens no states, exhausts +the (empty) open list immediately, and now reports `SEARCH_UNSOLVABLE` (11). + +### 2. Unsolvability proven by exhausting the state space + +`eager_search` and `lazy_search` log + +``` +Completely explored state space -- no solution! +``` + +when the open list runs empty. If the exploration was complete, this **is** a +proof of unsolvability. The search now returns the new `UNSOLVABLE` search +status (see `enum SearchStatus` in `src/search/search_algorithm.h`), which +`planner.cc` maps to exit code `11`. + +### Enforced hill climbing + +`ehc` is incomplete, so it generally reports `SEARCH_UNSOLVED_INCOMPLETE` (12) +when it gives up. The one exception (pre-existing) is when the **initial state +is a dead end** and the evaluator's dead ends are reliable, in which case it +already reported `SEARCH_UNSOLVABLE`. + +## Soundness: when is exhaustion a proof? + +Exhausting the open list only proves unsolvability if no reachable state was +discarded unsoundly. The relevant subtlety is **dead-end pruning**: + +* Open lists distinguish `is_dead_end()` (used for pruning) from + `is_reliable_dead_end()`. A dead end is *reliable* only if the evaluator + guarantees the state truly cannot reach the goal. +* Relaxation-based heuristics report **unreliable** dead ends when the task has + axioms or conditional effects (see `HMHeuristic::dead_ends_are_reliable`, + `RelaxationHeuristic::dead_ends_are_reliable`, etc.). Pruning such a state may + remove a genuine path to the goal, so an "empty" open list no longer proves + unsolvability. + +To stay sound, `eager_search` and `lazy_search` track a flag +`exhaustion_proves_unsolvability` (initialised to `true`). Whenever a state is +pruned for which `is_dead_end()` holds but `is_reliable_dead_end()` does not, +the flag is cleared. On exhaustion: + +* `exhaustion_proves_unsolvability == true` → return `UNSOLVABLE` → exit `11`. +* `exhaustion_proves_unsolvability == false` → return `FAILED` → exit `12`. + +Cost-bound pruning (`g + cost(op) >= bound`) does **not** invalidate the proof: +exit code `11` means "provably unsolvable with the given bound". Completeness- +preserving operator pruning (e.g. stubborn sets / partial-order reduction) is +also fine, because it preserves at least one path to every reachable goal. + +This is why, for example, `astar(hm())` on a *solvable* task that contains +axioms still reports `12` (the unreliable dead ends make exhaustion +inconclusive) rather than wrongly claiming unsolvability. + +## Quick reference: how to read the result + +* **Exit 10** — the task is unsolvable for a structural reason found before + search; read the translator line for *which* goal atoms / mutex are to blame. +* **Exit 11** — the search proved unsolvability (heuristic dead end on the + initial state, or a complete exhaustive search). Trustworthy as a proof + (modulo the cost bound). +* **Exit 12** — no plan found, but **not** a proof. The configuration is + incomplete or relied on unreliable pruning; try a complete, admissible + configuration (e.g. `astar(blind())`) to get a definitive `11`/solution. diff --git a/src/search/planner.cc b/src/search/planner.cc index 2f5addf422..43e7e176cc 100644 --- a/src/search/planner.cc +++ b/src/search/planner.cc @@ -53,9 +53,14 @@ int main(int argc, const char **argv) { utils::g_log << "Search time: " << search_timer << endl; utils::g_log << "Total time: " << utils::g_timer << endl; - ExitCode exitcode = search_algorithm->found_solution() - ? ExitCode::SUCCESS - : ExitCode::SEARCH_UNSOLVED_INCOMPLETE; + ExitCode exitcode; + if (search_algorithm->found_solution()) { + exitcode = ExitCode::SUCCESS; + } else if (search_algorithm->get_status() == UNSOLVABLE) { + exitcode = ExitCode::SEARCH_UNSOLVABLE; + } else { + exitcode = ExitCode::SEARCH_UNSOLVED_INCOMPLETE; + } exit_with(exitcode); } catch (const utils::ExitException &e) { /* To ensure that all destructors are called before the program exits, diff --git a/src/search/search_algorithm.h b/src/search/search_algorithm.h index 9ed2d571c3..e561b2029c 100644 --- a/src/search/search_algorithm.h +++ b/src/search/search_algorithm.h @@ -28,10 +28,18 @@ namespace successor_generator { class SuccessorGenerator; } +/* + Search status values returned by step() and stored in the search algorithm. + FAILED means the search stopped without a solution but cannot rule out that + one exists (e.g. it gave up or pruned states based on unreliable dead-end + detection). UNSOLVABLE means the search proved that no solution exists (within + the current cost bound, if any). +*/ enum SearchStatus { IN_PROGRESS, TIMEOUT, FAILED, + UNSOLVABLE, SOLVED }; diff --git a/src/search/search_algorithms/eager_search.cc b/src/search/search_algorithms/eager_search.cc index 99be531179..7148481334 100644 --- a/src/search/search_algorithms/eager_search.cc +++ b/src/search/search_algorithms/eager_search.cc @@ -92,6 +92,7 @@ void EagerSearch::initialize() { if (open_list->is_dead_end(eval_context)) { log << "Initial state is a dead end." << endl; + note_dead_end_pruning(eval_context); } else { if (search_progress.check_progress(eval_context)) statistics.print_checkpoint_line(0); @@ -107,6 +108,11 @@ void EagerSearch::initialize() { pruning_method->initialize(task); } +void EagerSearch::note_dead_end_pruning(EvaluationContext &eval_context) { + if (!open_list->is_reliable_dead_end(eval_context)) + exhaustion_proves_unsolvability = false; +} + void EagerSearch::print_statistics() const { statistics.print_detailed_statistics(); search_space.print_statistics(); @@ -118,7 +124,7 @@ SearchStatus EagerSearch::step() { if (!node.has_value()) { assert(open_list->empty()); log << "Completely explored state space -- no solution!" << endl; - return FAILED; + return exhaustion_proves_unsolvability ? UNSOLVABLE : FAILED; } return expand(node.value()); @@ -163,6 +169,7 @@ optional EagerSearch::get_next_node_to_expand() { int new_h = eval_context.get_evaluator_value_or_infinity( lazy_evaluator.get()); if (open_list->is_dead_end(eval_context)) { + note_dead_end_pruning(eval_context); node.mark_as_dead_end(); statistics.inc_dead_ends(); continue; @@ -257,6 +264,7 @@ void EagerSearch::generate_successors(const SearchNode &node) { statistics.inc_evaluated_states(); if (open_list->is_dead_end(succ_eval_context)) { + note_dead_end_pruning(succ_eval_context); succ_node.mark_as_dead_end(); statistics.inc_dead_ends(); continue; diff --git a/src/search/search_algorithms/eager_search.h b/src/search/search_algorithms/eager_search.h index 9d3da156ad..92cd89ad32 100644 --- a/src/search/search_algorithms/eager_search.h +++ b/src/search/search_algorithms/eager_search.h @@ -29,6 +29,21 @@ class EagerSearch : public SearchAlgorithm { std::shared_ptr pruning_method; + /* + True as long as exhausting the open list would prove the task unsolvable. + We set this to false once we prune a state as a dead end based on + unreliable dead-end detection, because then completely exploring the + reachable state space no longer rules out that a solution exists. + */ + bool exhaustion_proves_unsolvability = true; + + /* + Call this whenever we prune a state for which open_list->is_dead_end() + holds. If the dead end is not reliable, exhausting the state space no + longer proves unsolvability. + */ + void note_dead_end_pruning(EvaluationContext &eval_context); + void start_f_value_statistics(EvaluationContext &eval_context); void update_f_value_statistics(EvaluationContext &eval_context); void reward_progress(); diff --git a/src/search/search_algorithms/lazy_search.cc b/src/search/search_algorithms/lazy_search.cc index dd5afac207..005f5f5597 100644 --- a/src/search/search_algorithms/lazy_search.cc +++ b/src/search/search_algorithms/lazy_search.cc @@ -122,7 +122,7 @@ void LazySearch::generate_successors() { SearchStatus LazySearch::fetch_next_state() { if (open_list->empty()) { log << "Completely explored state space -- no solution!" << endl; - return FAILED; + return exhaustion_proves_unsolvability ? UNSOLVABLE : FAILED; } EdgeOpenListEntry next = open_list->remove_min(); @@ -216,6 +216,8 @@ SearchStatus LazySearch::step() { generate_successors(); statistics.inc_expanded(); } else { + if (!open_list->is_reliable_dead_end(current_eval_context)) + exhaustion_proves_unsolvability = false; node.mark_as_dead_end(); statistics.inc_dead_ends(); } diff --git a/src/search/search_algorithms/lazy_search.h b/src/search/search_algorithms/lazy_search.h index ae0dbcba04..8841e604d8 100644 --- a/src/search/search_algorithms/lazy_search.h +++ b/src/search/search_algorithms/lazy_search.h @@ -38,6 +38,13 @@ class LazySearch : public SearchAlgorithm { int current_real_g; EvaluationContext current_eval_context; + /* + True as long as exhausting the open list would prove the task unsolvable. + Set to false once we prune a state as a dead end based on unreliable + dead-end detection (see EagerSearch for details). + */ + bool exhaustion_proves_unsolvability = true; + virtual void initialize() override; virtual SearchStatus step() override; diff --git a/src/translate/__main__.py b/src/translate/__main__.py index 92802a6413..c127d9c7c4 100644 --- a/src/translate/__main__.py +++ b/src/translate/__main__.py @@ -34,7 +34,9 @@ def handle_sigxcpu(signum, stackframe): # Reserve about 10 MB of emergency memory. # https://stackoverflow.com/questions/19469608/ emergency_memory = b"x" * 10**7 - main() + # main() returns TRANSLATE_UNSOLVABLE if the task is unsolvable and + # None otherwise (in which case we exit with code 0). + sys.exit(main()) except MemoryError: del emergency_memory print() diff --git a/src/translate/main.py b/src/translate/main.py index d047353677..fe175986c3 100755 --- a/src/translate/main.py +++ b/src/translate/main.py @@ -30,6 +30,10 @@ def python_version_supported(): from translate import variable_order from translate.options import get_options +## For a full list of exit codes, please see driver/returncodes.py. Here, we +## only list the code returned by main() when the task is unsolvable. +TRANSLATE_UNSOLVABLE = 10 + # TODO: The translator may generate trivial derived variables which are always # true, for example if there ia a derived predicate in the input that only # depends on (non-derived) variables which are detected as always true. @@ -472,7 +476,13 @@ def translate_task( if goal_dict_list is None: # "None" is a signal that the goal is unreachable because it # violates a mutex. - return unsolvable_sas_task("Goal violates a mutex") + conflict = describe_goal_mutex_violation(goals, mutex_dict) + if conflict: + reason = ("Goal violates a mutex: the goal atoms %s are mutually " + "exclusive" % conflict) + else: + reason = "Goal violates a mutex" + return unsolvable_sas_task(reason) assert len(goal_dict_list) == 1, "Negative goal not supported" ## we could substitute the negative goal literal in @@ -529,7 +539,50 @@ def solvable_sas_task(msg): def unsolvable_sas_task(msg): print("%s! Generating unsolvable task..." % msg) - return trivial_task(solvable=False) + task = trivial_task(solvable=False) + task.unsolvable = True + task.unsolvable_reason = msg + return task + + +def describe_unreachable_goal_atoms(task, reachable_atoms): + """Return the positive goal atoms that can never become true: they are + neither relaxed reachable nor true in the initial state. + + reachable_atoms is the set of relaxed-reachable fluent facts. We read the + goal directly from the (normalized) task because an unreachable positive + goal atom causes the instantiated goal to collapse to None. + """ + goal = task.goal + if isinstance(goal, pddl.Conjunction): + goal_parts = goal.parts + elif isinstance(goal, pddl.Literal): + goal_parts = [goal] + else: + return [] + init_facts = {fact for fact in task.init if isinstance(fact, pddl.Atom)} + return [part for part in goal_parts + if isinstance(part, pddl.Atom) + and part not in reachable_atoms + and part not in init_facts] + + +def describe_goal_mutex_violation(goal_list, mutex_dict): + """Return a description of a pair of goal atoms that are mutually + exclusive, or None if no such pair of positive goal atoms is found. + + This mirrors the positive-fact check in translate_strips_conditions_aux + but only for reporting purposes, so it never affects the translation. + """ + assigned = {} # mutex variable -> (value, goal atom assigning it) + for fact in goal_list: + if fact.negated: + continue + for var, val in mutex_dict.get(fact, []): + if var in assigned and assigned[var][0] != val: + return "%s and %s" % (assigned[var][1], fact) + assigned[var] = (val, fact) + return None def pddl_to_sas(task): with timers.timing("Instantiating", block=True): @@ -537,9 +590,19 @@ def pddl_to_sas(task): reachable_action_params) = instantiate.explore(task) if not relaxed_reachable: - return unsolvable_sas_task("No relaxed solution") + unreached = describe_unreachable_goal_atoms(task, atoms) + if unreached: + reason = ("No relaxed solution: the following goal atoms are not " + "reachable even in the delete relaxation: " + + ", ".join(str(atom) for atom in unreached)) + else: + reason = ("No relaxed solution: the goal is not reachable even in " + "the delete relaxation") + return unsolvable_sas_task(reason) elif goal_list is None: - return unsolvable_sas_task("Trivially false goal") + return unsolvable_sas_task( + "Trivially false goal: the goal contains a fact that is " + "statically false (e.g. a negated static atom that always holds)") negative_in_goal = set() for item in goal_list: @@ -712,3 +775,27 @@ def main(): with open(get_options().sas_file, "w") as output_file: sas_task.output(output_file) print("Done! %s" % timer) + + if get_options().diagnostics_json: + write_diagnostics_json(sas_task, get_options().diagnostics_json) + + if sas_task.unsolvable: + return TRANSLATE_UNSOLVABLE + + +def write_diagnostics_json(sas_task, path): + import json + record = { + "status": "unsolvable" if sas_task.unsolvable else "ok", + "reason": sas_task.unsolvable_reason, + "statistics": { + "variables": len(sas_task.variables.ranges), + "facts": sum(sas_task.variables.ranges), + "goal_facts": len(sas_task.goal.pairs), + "operators": len(sas_task.operators), + "axioms": len(sas_task.axioms), + "mutex_groups": len(sas_task.mutexes), + }, + } + with open(path, "w") as f: + json.dump(record, f) diff --git a/src/translate/options.py b/src/translate/options.py index 1943b60a1f..f8c671c5e3 100644 --- a/src/translate/options.py +++ b/src/translate/options.py @@ -81,6 +81,10 @@ def get_arg_parser(): argparser.add_argument( "--dump-task", action="store_true", help="dump human-readable SAS+ representation of the task") + argparser.add_argument( + "--diagnostics-json", default=None, + help="write a machine-readable JSON diagnostics record (solvability " + "status, unsolvability reason, and translation statistics) to this path") argparser.add_argument( "--layer-strategy", default="min", choices=["min", "max"], help="How to assign layers to derived variables. 'min' attempts to put as " diff --git a/src/translate/sas_tasks.py b/src/translate/sas_tasks.py index 748f9703a4..f1833bffec 100644 --- a/src/translate/sas_tasks.py +++ b/src/translate/sas_tasks.py @@ -36,6 +36,14 @@ def __init__(self, self.axioms = sorted(axioms, key=lambda axiom: ( axiom.condition, axiom.effect)) self.metric = metric + # Set to True by the translator when it has detected that the task is + # unsolvable. The (trivially unsolvable) task is still emitted so that + # the search component works as before, but the translator additionally + # exits with the TRANSLATE_UNSOLVABLE exit code. + self.unsolvable = False + # The reason produced by unsolvable_sas_task() (e.g. which goal atoms + # are unreachable), surfaced in the --diagnostics-json record. + self.unsolvable_reason = None if DEBUG: self.validate()