I've started thinking about this in a bit more detail, but I suggest we move the
discussion to email while it's more in a brain-storming stage. The tracker
discussion for a resolved and only slightly related issue is perhaps not the
best place for this. :-) Silvan, I'll include you in the email because you're
nosy here; just let us know if you don't want to be part of the email conversation.

Omega(mn) as a lower bound for dynamic SSSP makes no sense because this is worse
than recomputing everything from scratch, which can be done in O(m + n log n)
and is of course a valid dynamic algorithm. There must be some additional
aspects to the model they use (how exactly queries and updates are interleaved
and how costs are counted) that make the problem harder than the problem we
consider here, which is *one* (small and localized) set of updates followed by
solving an SSSP.

Dynamics SSSPs (probably not under this name; I'd have to check the details)
have been studied in many papers by Sven Koenig's group, and they have achieved
very significant speed-ups over static algorithms.

A major point that makes me hopeful there is something to get here is that the
problem is *not* fully dynamic. I would model it with removal of edges only,
because refinement can only make shortest paths longer, never shorter. Think of
a refinement step as two separate operations [1]:

1. Clone the state you want to refine, copying all incoming and outgoing
transitions. That is, if the state you want to refine is v with predecessors
u_1, ..., u_n and successors w_1, ..., w_m, add a new state v' also with
predecessors u_1, ..., u_n and successors w_1, ..., w_m. If v has a self-loop,
create all four possible edges: v->v, v->v', v'->v, v'->v'.

2. Remove all edges that should not be present.

Note that the first transformation doesn't affect the goal distances. v' will
have the same goal distance as v, and no other goal distance changes. This is
because v and v' are completely interchangeable in all paths, so there is never
a need to use the new state v'.

So the only transformation that requires recomputations is the second one, which
is monotonic. The only states that can potentially have their heuristic value
changed are those whose recorded shortest paths (which can be stored by keeping
track of the shortest path tree, which is also useful for shortest path
extraction) are those nodes that are behind v in the shortest path tree, and I
would hope that by processing these in increasing h order (assuming non-zero
action costs; otherwise the best order is less clear), it is possible to do what
is essentially a Dijkstra search, but limited to states whose goal distance has
actually changed. But I haven't thought the details of this through.

[1] This assumes that the state you're refining is not a goal state. If it is,
and if it is refined into one state that is and one that isn't, there are some
additional complications. This can be avoided conceptually by using an
artificial goal state.

Keeping the heuristic values up to date and avoiding the search is certainly an
interesting idea. I searched the literature for this problem and think that the
following publication is the most relevant one:

On dynamic shortest paths problems
L. Roditty and U. Zwick
European Symposium on Algorithms, 2004, Springer

Below are three relevant excerpts. I included the first for nomenclature. Our
problem of keeping the goal distances up to date is a fully dynamic
single-source shortest path (SSSP) instance, since edges are both removed and
added. The second and third excerpts say that this kind of problem is hard,
i.e., runs in time Ω(mn), where m is the number of edges and n is the number of
nodes, which is probably prohibitively expensive for us. 

Introduction:
The objective of a dynamic shortest path algorithm is to efficiently process an
online sequence of update and query operations. Each update operation inserts or
deletes edges from an underlying dynamic graph. Each query operation asks for
the distance between two specified vertices in the current graph. A dynamic
algorithm is said to be fully dynamic if it can handle both insertions and
deletions. An incremental algorithm is an algorithm that can handle insertions,
but not deletions, and a decremental algorithm is an algorithm that can handle
deletions, but not insertions. Incremental and decremental algorithms are
sometimes referred to as being partially dynamic. An all-pairs shortest paths
(APSP) algorithm is an algorithm that can report distances between any two
vertices of the graph. A single-source shortest paths (SSSP) algorithm can only
report distances from a given source vertex.

Abstract:
[...] the incremental and decremental single-source shortest-paths problems, for
weighted directed or undirected graphs, are, in a strong sense, at least as hard
as the static all-pairs shortest-paths problem [...]

Bottom of page 582:
All known algorithms for the static APSP problems in weighted directed or
undirected graphs run in Ω(mn) time. A running time of O(mn + n² * log n) is
obtained by running Dijkstra's algorithm from each vertex.

Hmmm, I don't think so, but maybe my intuition for this is not good, as I don't
know the code very well.

Given how much time is spend performing A* search, I would try to avoid the
search for an optimal abstract solution altogether and instead keep the
heuristic values up to date in such a way that optimal abstract solutions can be
extracted without search. The main challenge then is how to keep the heuristic
values up to date, but for this incremental search algorithms exist that focus
on repairing only the values that may have changed. Maybe you're right and this
is not promising, but my intuition is that it should be possible to do this in
such a way that work is only needed for states whose heuristic values have just
improved, and that therefore the amortized overall work should be comparatively
low after a while when the heuristic values stop improving as quickly. (The
argument only really works in the absence of zero-cost actions, but I suppose
zero-cost actions make things much more expensive for A*-style algorithms, too.)

I agree that there might be other opportunities to improve the CEGAR code.
However, I think it will be hard to find a better version that doesn't use A*,
so it's likely that it will also benefit from the change at hand.

This is now merged.

The results look good. The only concern I have with this and some of the sister
issues is that I'm worried that this may be premature optimization: making local
performance improvements before it is clear that the overall data structures
used are the best choice. But the complication is not that large, so that's not
a major objection.

The new code is now documented and the results are in:

https://ai.dmi.unibas.ch/_tmp_files/seipp/issue883-v1-issue883-base-issue883-v1-compare.html

The abstraction computation becomes faster for all four tested variants. The
speedups are more pronounced for the original() versions since the
landmarks()+goals() versions don't take much time to compute anyway:
 
https://ai.dmi.unibas.ch/_tmp_files/seipp/issue883-v1-init_time-cegar-original-1M-issue883-base-issue883-v1.png
https://ai.dmi.unibas.ch/_tmp_files/seipp/issue883-v1-init_time-cegar-original-2M-issue883-base-issue883-v1.png
https://ai.dmi.unibas.ch/_tmp_files/seipp/issue883-v1-init_time-cegar-landmarks-goals-1M-issue883-base-issue883-v1.png
https://ai.dmi.unibas.ch/_tmp_files/seipp/issue883-v1-init_time-cegar-landmarks-goals-2M-issue883-base-issue883-v1.png

Coverage remains almost stable: the total coverage numbers differ only by +- 1
and no domain loses or gains more than 1 task using any of the four configurations.

What do you think?

I made a pull request for this at
https://bitbucket.org/jendrikseipp/downward/pull-requests/116 . 

The new code still needs documentation. Experiments are running.

After finding a trace, we currently update the h values of all abstract states
on the trace. This allows the internal A* algorithm to find the next trace
faster (in fact, if we didn't update the h values, we would be using uniform
cost search instead of A*).

I noticed that after an A* search is finished, we may have better lower bounds
on h* not only for the states on the trace, but for other states as well. If C*
is the cost of the trace and we take the current g values as assigned by A* when
it finds a shortest trace, then C*-g(s) is a lower bound on the goal distance of
abstract state s. This is the case since

g(s) >= g*(s) [1]

and

    f*(s) >= C*         (Optimality of A* with an admissible heuristic)
==> g*(s) + h*(s) >= C* (Definition of f values)
==> g(s) + h*(s) >= C*  (uses [1])
==> h*(s) >= C* - g(s)  (Arithmetic)

Together with our existing lower bound h*(s) >= h(s), i.e., the h values from
the last iteration, for each abstract state s we could set h(s) = max(h(s),
C*-g(s)).