What exactly does "weakly" and "strongly" solved games mean

[klx]

This is quite a long post.

Wow this is an amazing answer, I think you managed to answer in full every single question I posed. Thank you so much, and I hope this post can be useful for others as well. You should update the wikipedia page

You are right, I had missed tha part of the proof tree. Or rather, I had read about it, but not understood its significance in weakly solving the game.

I think part of this was that I assumed that with or without a proof tree, as long as the search ends in a WDL database, we could not guarantee a terminating search so it's not solved anyway. As per your post above, your take is that at least in Checkers, running search on top of WDL, we should be able to make progress, so it is indeed solved. This makes sense.

Now I am curious about this proof tree, can we also create it from an alpha-beta search? And what's the most efficient way of doing this.

[Rein Halbersma]

Checkers is probably reasonably benign, (comapred to Chess), because most moves are irreversible (perhaps all moves?). When you don't have to deal with infinitely long branches, you can safely do a depth-first search that only considers a node a leaf when it hits the EGT. Or falls victim to the equivalent of mate-distance pruning.

Checkers (8x8 board) and draughts (10x10 board, different capture rules) with promoted pieces have reversible moves, just like chess endgames. There are also longest wins spanning hundreds of ply.

[Rein Halbersma]

According to Victor Allis:
ultra-weakly solved
For the initial position(s), the game-theoretic value has been determined.

weakly solved
For the initial position(s), a strategy has been determined to obtain at least the game-theoretic value of the game, for both players, under reasonable resources.

strongly solved
For all legal positions, a strategy has been determined to obtain the game-theoretic value of the position, for both players, under reasonable resources.

One could also define "ultra-strongly solved" as having an optimal length strategy. This would correspond to having DTM/DTZ type tablebases rather than WLD tablebases.

[hgm]

OTOH, 'ultra-strongly solved' of a game with WDL outcome would be the same as 'strongly solved' for a game where the distance-to-win metric is part of the game rules, so that 'slower' wins count as a different (inferior) game result.