Unsolvability reporting

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.

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,

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

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<SearchNode> 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;

src/search/search_algorithms/eager_search.h

@@ -29,6 +29,21 @@ class EagerSearch : public SearchAlgorithm {
 
     std::shared_ptr<PruningMethod> 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();

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

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;
 

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