Why do engines lack mate solving?

[Ras]

then captures with MVA-LVV

MVV-LVA of course.

[yurikvelo]

Either I fail to understand the output, or Stockfish really needs more than 50 plies depth in order to reliably detect a mate in 15

there is no upper limit to reliably prove DTM=15 as minimum.
Even at D=100 there will be a lot zillions of lines with less than D=15 searched.
It is possible to miss DTM=10 at D=100, if that line was early pruned

With branching factor of all SF methods (alpha-beta pruning, NMR, LMR, EG-heuristics etc) ~1.6 (in EG positions) you need 1.6^50 = 16 BN to reach D=50

With brancing factor ~20 for all legal moves (in EG positions) you need 20^15 = 3.2 * 10^19 just to reach D=15

DTM=15 (30 plies) require 10^39 brute force complexity!

With 16BN positions searched, SF reaches typical D=50, while full bruteforce will reach only D=8 (mate in 4)

[hgm]

then captures with MVA-LVV

MVV-LVA of course.

The point is that this is an ordering optimized for getting high material eval. If you are optimizing the prospects for mate or escape, rather than material, it could be very counter-poductive. The 'value' referred to in MVV-LVA should refer to the threat they pose to the King of the number of checking squares they defend, rather than the piece type.

My guess is that it would be really helpful to have a heuristic evaluation that estimates how easy it is to checkmate, rather than to win in an end-game, or just evaluating every non-mate as 0. With the latter techniques like IID would be no help at all, as any move would look the same as long as the mate is not yet within the horizon.

With some evaluation to provide guidance you could get the most promising move from a shallow pilot search, and search that first.

[Ras]

ok, so far, I get very nice results with the approach of first only examining check-giving moves for the side to deliver mate, and in case of failure to find mate, push out the start depth for "checking moves alone" move by move. So, an iteration. For mate in 1-8, that is OK.

I even dug out a mate in 8 with a quiet move (neither check nor capture) in the 3rd move that my embedded target system solves within nice 5:07 minutes:
FEN "r3r3/1ppp1ppk/1bn4p/1B2N3/3P4/2P4P/QP3PP1/6K1 w - -"

I also have taken a look into PN-search, but the showstopper for any further consideration was that the tree has to be in memory.

However, there is another aspect rising. While the search time for finding a mate is really fine, the re-search for double solutions obviously doesn't profit from my speedup approach because it cannot find a mate (there is none). So that boils down to the mate searcher doing the alpha-beta-minimax with all moves considered until the full depth. With the result being "no mate found", of course.

With the position given above, the target system would need about 2:20 hours (calculated by how much time the x86 based development version needs).

I'm a bit out of ideas how to deal with that problem. No "find it quickly" strategy can help when there is nothing to find and the point is to actually prove this. For proving the existence of something, you "just" have to find it by whatever clever method. But for proving absence, you have to try out everything and see that exhaustive search fail, so this is a much harder task.

BUT, here comes the funny thing: someone with a Mephisto Nigel Short (6502 CPU) tried out the mate in 7 by Nimzowitsch, and the machine solves that within 37 seconds (where my system needs less than a second, after the improvement). But when doing the search for a second solution, the Nigel Short almost immediately tells that there is none. Just how is this possible, short of being a probabilistic answer instead of a proof?

Did I overlook something, and disproving mate is really even easier than proving it?

[Evert]

ok, so far, I get very nice results with the approach of first only examining check-giving moves for the side to deliver mate, and in case of failure to find mate, push out the start depth for "checking moves alone" move by move. So, an iteration. For mate in 1-8, that is OK.

I even dug out a mate in 8 with a quiet move (neither check nor capture) in the 3rd move that my embedded target system solves within nice 5:07 minutes:
FEN "r3r3/1ppp1ppk/1bn4p/1B2N3/3P4/2P4P/QP3PP1/6K1 w - -"

I also have taken a look into PN-search, but the showstopper for any further consideration was that the tree has to be in memory.

However, there is another aspect rising. While the search time for finding a mate is really fine, the re-search for double solutions obviously doesn't profit from my speedup approach because it cannot find a mate (there is none). So that boils down to the mate searcher doing the alpha-beta-minimax with all moves considered until the full depth. With the result being "no mate found", of course.

With the position given above, the target system would need about 2:20 hours (calculated by how much time the x86 based development version needs).

I'm a bit out of ideas how to deal with that problem. No "find it quickly" strategy can help when there is nothing to find and the point is to actually prove this. For proving the existence of something, you "just" have to find it by whatever clever method. But for proving absence, you have to try out everything and see that exhaustive search fail, so this is a much harder task.

BUT, here comes the funny thing: someone with a Mephisto Nigel Short (6502 CPU) tried out the mate in 7 by Nimzowitsch, and the machine solves that within 37 seconds (where my system needs less than a second, after the improvement). But when doing the search for a second solution, the Nigel Short almost immediately tells that there is none. Just how is this possible, short of being a probabilistic answer instead of a proof?

Did I overlook something, and disproving mate is really even easier than proving it?

I haven't given this a great deal of thought, but I would think that you can speed things up considerably by a suitable choice of aspiration window. If you're looking for a mate-in-N, then you can set alpha to +mate-N and beta to +mate (say) and most moves should be cut quickly.

I don't know how well that works in practice, but I gave it a try for the position you posted with Jazz. Without doing anything, it doesn't find the mate before depth 20 after 36 seconds (when I stopped the search; it had found the correct first move and the score was climbing steadily with each iteration). If I set the aspiration window for a mate score, it finds the solution at depth 7 in under a second:

Code: Select all

  7 +159.86   0.65    226115 1. Bd3 Kg8 2. Qxf7 Kh8 3. Qg6 Kg8 4. Qh7 Kf8 5. Qh8 Ke7 6. Qxg7 Ke6 7. Qf7 Kd6 8. Qxd7 

[Ras]

If I set the aspiration window for a mate score, it finds the solution at depth 7 in under a second:

Nah, the issue isn't finding the mate, that's the easy part. The issue is blocking the already found solving move in the root position and then proving that there isn't an alternative mate anymore within the required distance.

[Arpad Rusz]

Stockfish often doesn't find mates in two moves even at depth 127. I guess, that is not a normal behavior for a top engine...

[Evert]

If I set the aspiration window for a mate score, it finds the solution at depth 7 in under a second:

Nah, the issue isn't finding the mate, that's the easy part. The issue is blocking the already found solving move in the root position and then proving that there isn't an alternative mate anymore within the required distance.

How is that an issue?
Similar to multi-pv, you just skip the move you already found and search normally, with the aspiration window set appropriately. If you do this correctly, you should find alternatives ok (if they exist).

I don't think there is a search strategy that is equally efficient in all positions though; there will always be some you cannot find (easily).

[Evert]

Stockfish often doesn't find mates in two moves even at depth 127. I guess, that is not a normal behavior for a top engine...

Only if it loses or fails to win games because of that. Otherwise it makes no difference, it just looks stupid.
Remember: Stockfish is optimised for winning games, not for analysis or problem solving.

[Ras]

How is that an issue?

While the mate in 8 posted above is found within 5 minutes on the target platform (good), the re-search for the alternative (that doesn't exist) takes 2:20 hours, that is the issue.