Upper bound on proof tree size

[zullil]

For any position P that is mate in N, define M[P] as the minimum number of nodes in any proof tree for that fact. I think what you meant to ask is what is the maximum value of M[P] among all positions P that are mate in N.

Yes, max over minimal proof trees. Thanks for clarifying.

[zullil]

When N becomes large the maximum number of nodes in a proof tree is more problematic. The current bound (if that's what you want to call it) is useless. Example a mate in 549 (taken from the 7-man Lomonosov table bases) isn't possible if the current upper bound is to be believed. Even with a branching factor of 2 or less the size of the proof tree would be orders of magnitude larger than the total number of positions in chess. Black's branching factor in line of play is as high as the mid-thirties and probably averages around 15-20. If we use the formula given in other posts the number of nodes in this tree would be ~ 1.0E+701. There are only approximately 1.0E+43 possible positions in chess. No proof tree may contain all possible chess positions. So clearly this upper bound is completely worthless!

I conclude that there exists a better upper bound. i.e. something that is around 2*b^(n/2)or there abouts. The problem is finding it's exact form and then proving it. Even if no proof is found having a good estimate vice a bound for such a f

Yes, we all agree that the least (ie, best) upper bound is much lower than than the (useless ) upper bound provided by my formula. And yes, we understand that some replies by the opponent will lead to much smaller proof trees than will other replies. But unless you include additional assumptions, you cannot obtain a better formula. To prove a better upper bound, you'd have do an exhaustive search over mate-in-n positions.

What is the least upper bound for mate-in-2 positions? Suppose we only consider positions for which:

(1) It's White's turn to play, and Black is not in check.
(2) No single move by White checkmates Black.
(3) There exist a unique move (the "key") for White that doesn't stalemate Black, and such that, for each reply by Black, White has a checkmate move.

What position satisfies these conditions and possesses the most replies by Black to White's key?

For example, this composition by Godfrey Heathcote appears in the Wikipedia entry for Chess_problem:

[D]6K1/pN2R1PQ/p7/r2k3r/N2n4/1P2p3/BB5p/2Rb2bq w - - 0 1

After the key of Rcc7, there are 28 replies by Black, each resulting in a mate in one by White. So a proof tree for this position needs 1 + 28 + 28 = 57 nodes.

How much above 57 is the most "complex" two-mover? What's the current record? Is the max known? Proved?

[Angrim]

I don't have a formula, if you store only "hard" lines, and not the refutations for all those mate in 1 positions, the resulting proof tree is generally small. I've stored proofs that took weeks to solve in a few megabytes, as text lists of moves, with no compression. My rule of thumb is that if a losing move can be proven to have lost in under 0.5 seconds, then I don't bother to store it. Going with that, you are unlikely to ever have a problem with disk space.

[Zenmastur]

Yes, we all agree that the least (ie, best) upper bound is much lower than than the (useless ) upper bound provided by my formula. And yes, we understand that some replies by the opponent will lead to much smaller proof trees than will other replies. But unless you include additional assumptions, you cannot obtain a better formula. ...

First, you seem to be admitting that not all black replies can be of equal value. I guess this is a start. While it may be possible for all black replies in a single position to be of equal value it seems impossible that ALL black moves in ALL positions originating from a single "key" position if the length of the series of moves is very long. The question is how to prove it.

I'm willing to include as many additional assumption, lemmas, or proofs as is required. I'm not sure why you believe that additional assumptions need to be made or what the nature of these assumptions might be.

I was thinking that we have sufficient information available to restrict the number of possible positions in chess that meet certain criterion by proofs that the pool of possible positions that meet these criterion becomes zero.

The only problem I see with this approach is no one that I'm aware of in the chess community, the computer chess community, or academia has laid sufficient foundation, in the way of proofs, to support such a proof.

Example, the four-color map theorem has been proven. It considers an infinite set of planer maps. If they would have tried to prove this theorem by a state space search, this is the approach you are suggesting we use to solve the current problem, it would be impossible of proof. The way the problem was actually solved was by showing that a small set of "key" maps were, in effect, equivalent to all other "possible" maps, and then solving the problem for the key maps. i.e. they took an infinite set and reduced it to a finite and tractable set and then solved the problem for this set. This was possible because a large group of individuals had worked to solve other problems (by proofs) in this field of study. In short, someone had laid a foundation that would support such a proof. Without this foundation it's very unlikely that this problem could have been solved, since the solvers would have had to solve all the subsidiary problems as well.

I don't see much of a foundation of this sort that would support such a proof in chess. Did I overlook it? Does it exist and in my haste I blindly passed it by?

To prove a better upper bound, you'd have do an exhaustive search over mate-in-n positions.

I don't believe that this statement follows, directly or indirectly, from your previous statements. I think it's a conjecture on your part and that the truth of the matter remains to be seen. If exhaustive search is the answer to all combinatorial state space problems we're in a world that will be forever a mystery to us.
Regards,

Zen

[zullil]

I wish you luck.

See if you can find the answer---with proof--- for N=2.

[Zenmastur]

I don't have a formula, if you store only "hard" lines, and not the refutations for all those mate in 1 positions, the resulting proof tree is generally small. I've stored proofs that took weeks to solve in a few megabytes, as text lists of moves, with no compression. My rule of thumb is that if a losing move can be proven to have lost in under 0.5 seconds, then I don't bother to store it. Going with that, you are unlikely to ever have a problem with disk space.

What program are you using to generate these proof trees? Is it a purpose built program or a more general one adapted for this purpose?

Regards,

Zen

[Zenmastur]

I wish you luck.

See if you can find the answer---with proof--- for N=2.

I'll, no doubt, need all the luck that I can get assuming there is such a thing.

If you are trying to point out that for N=2, a proof tree exists that is of the size of the upper bound that you gave, I will readily concede that this is possible.

I'm not ready to concede the more general case when N is large however.

I was hoping that someone else had already looked at this problem and found a better bound and I didn't want to re-invent the wheel but the lack of responses in this thread seems to indicate that no one else has found a better bound.

Regards,

Zen

[Angrim]

It's purpose built, using proof number search(with the pn^2 extension). I've been working on refuting openings in several chess variants. Some of them have similar branching factors to chess, so my results should be applicable.

What program are you using to generate these proof trees? Is it a purpose built program or a more general one adapted for this purpose?

Regards,

Zen

[Zenmastur]

It's purpose built, using proof number search(with the pn^2 extension). I've been working on refuting openings in several chess variants. Some of them have similar branching factors to chess, so my results should be applicable.

I'm not familiar with proof number searches and I know nothing of there extensions. Do they have some particular advantage that makes them suitable for generating proof trees?

Not to play 20 questions ... but close...

What's the largest proof tree by nodes that you have created?
The largest by depth of search?
The longest running time, cumulative time?
Can the searches be started and stopped at will or are they required to start and run to completion? i.e. does the engine create check points for restarts?
Can it play standard chess as is or would it need to be modified?
How fast is it in general? Perft?

Sorry, for all the questions, but I'm curious. I've been considering converting or adding code to crafty to do something similar. Plus I have a few ideas about pruning that I developed many years ago but never got around to implementing. From what I've read so far I haven't seen any similar idea's mentioned so maybe they're still new and untried. I just haven't decided that I want to spend that much time on it. Right now I'm just reading all the posts that I can and trying to bring myself back up to speed. Some things have changed a lot since I last wrote a chess program, while other things seem to have progressed very little.

Regards,

Zen

[hgm]

While it may be possible for all black replies in a single position to be of equal value it seems impossible that ALL black moves in ALL positions originating from a single "key" position if the length of the series of moves is very long.

[d]8/8/8/4K3/p7/P7/8/7k w

In positions like this there isn't very much black can do to hasten the mate...