Upper bound on proof tree size

[Angrim]

If you are interested in mate solvers in general, you really should read up on it. pn-search and it's variants are designed for finding
proofs, and in many positions are much better at it than conventional searchers.
https://chessprogramming.wikispaces.com ... ber+search

As for your questions:
nodes: I haven't kept track, but some have been over a trillion nodes.
depth: Again, haven't kept track of the longest ever, but in more forcing positions I've seen it get over 140 ply. These super-long lines tend to include a lot of pointless checks.
time: I've had some positions take as long as 2 weeks, I tend to get bored and terminate the search if it takes more than that.
resumability: I have a UPS, so no, it doesn't support restarts.
chess: Yes, standard chess is one of the variants that my engine supports. I use it as a baseline that I modify when adding a new
variant to my collection. I have done very little with the chess engine itself
speed: speed in my computer(few years old Athlon) is around 2-3m nps for chess. perft 6 takes around 10 seconds.

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

[Zenmastur]

I wish you luck.

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

I think I have found a step in the right direction.

A search space of 10^18 still seems impossibly large. If 10^6 positions were solved per second, 100,000 years of computing would be required to enumerate all the positions. What makes the problem of finding the game-theoretic value of checkers feasible is the idea of a proof tree. When analyzing a position that is a win, one need only consider one winning move; the alternatives moves are either inferior or redundant. When considering a position that is a loss or a draw, all alternatives must be considered (since you have to prove you cannot do better). In the best case a game that is provably winning the search only has to explore roughly the square root of the search space: a single move at winning positions and all moves at losing positions. This means that a proof of the game-theoretic value of checkers might require a search of as few as 10^9 positions. Of course, knowing which 10^9 positions out of 10^18 is the hard part.

I'm wondering if either of the authors post here or on other boards. It would be nice to get a little more information about these thoughts. Although they don't mention the number of nodes in a proof tree if the proof can be found by searching 10^9 nodes in checkers it seems that the proof tree couldn't have more nodes in it than that.

If their supposition is true, it has several useful implications. One of these is the calculation is not based on the depth of the mate or the branching factor of the various positions in the proof tree. This simplifies the analysis greatly. For many positions the estimate will still be "loose" but this is considerably better than the other method. It means that no proof tree in chess can have greater than 10^21.5 nodes in it. (This statement assumes Shannon's estimate for the total number of positions possible in chess is correct.) So any proof tree of a mate would have this upper bound regardless of length of mate or branching factor.

This number, 10^21.5 is based on the total number of positions that are reachable from the standard chess starting position. It can be shown that for any position in which pawns have been moved or any number of pieces or pawns have been captured that the number of positions that can be reached is significantly reduced. For example, approximately 2.41E+36 position can be reached from this position, which is 15 plies into the game:

[D]rnbqkb1r/pp3ppp/4p3/8/3PP3/8/P4PPP/1RBQKBNR b Kkq - 0 8

So the maximum size of proof tree starting at this position would have at most 1.55E+18 nodes in it if this idea is correct. This position which has the same material content:

[D] 2bqr1k1/r4p2/p3p2B/npb3P1/2p4p/P1N1PB2/1P2QPP1/2R1K2R b K - 0 22
would have different numbers, namely ~1.88E+34 reachable positions and a maximum proof tree size of ~1.37E+17 nodes. The difference in these numbers is a result of the second position having a more advanced (meaning degraded) pawn structure.

This may not look like its much of an improvement, and for these positions it isn't. But as more pawns advance and more pieces are removed from the board the number of reachable positions are significantly reduced and the square root of this number will become a usable bound in many but not all cases.

In a case were there is a long mate but not too much material this will give a much better estimate than the formula you gave. In a case where the mate isn't too long but there is a lot of material on the board the iterative formulae may give a better estimate. In the mate in 549 moves taken from the Lomonosov table bases this method is a huge improvement. There are, if my math is correct, less than 1.4E+13 positions possible given the material available. This implies that a proof-tree of this mate will contain ~3,744,857 or fewer nodes. This is a huge number of orders of magnitude less than the other formula gives.

It's not much but it's a step in the right direction and all I had to do was a little reading. A little more research seems to be in order.

I guess one way to test this theory is to check it against the table bases. If none of the poof trees included in or that can be constructed from the table bases exceeds the square root of the total number of positions possible with the given material then this would lend some support that this idea is correct. It won't prove it obviously, but if any of the proof trees are significantly larger than the square root of the total number of positions possible this would be sufficient to show the idea is flawed if no smaller proof tree can be found.

An alternate way to test it is to use a program such as Ben's to generate a proof tree for the position from the Lomonsov table bases (or other positions from smaller table bases). If the number of nodes in the proof tree is less than or equal to 3,744,857 then this would seem to be good evidence that the idea is a good one. If the number of nodes in the proof tree is greater than 3,744,857 then one would need to check to see if a smaller proof-tree can be found. If no smaller tree can be found I think it would be safe to discard the idea in its current form.

I don't know about getting access to the Lomonosov table bases. It seems improbable that this could be done over the internet but someone that has more direct access to them may be able to do the tests.

Of course there are probably some positions from the 5 or 6 man table bases that have long mates that would be easier and quicker to test. These would make a good first start towards a determination of the validity of this idea.

So Ben,

What do you think about trying your program on a few positions taken from the 5 and 6 man table bases? Preferably the longest one they contain. And possibly working your way up to the longest 7-man mate?

Regards,

Zen

[Zenmastur]

If you are interested in mate solvers in general, you really should read up on it. pn-search and it's variants are designed for finding
proofs, and in many positions are much better at it than conventional searchers.
https://chessprogramming.wikispaces.com ... ber+search

As for your questions:
nodes: I haven't kept track, but some have been over a trillion nodes.
depth: Again, haven't kept track of the longest ever, but in more forcing positions I've seen it get over 140 ply. These super-long lines tend to include a lot of pointless checks.
time: I've had some positions take as long as 2 weeks, I tend to get bored and terminate the search if it takes more than that.
resumability: I have a UPS, so no, it doesn't support restarts.
chess: Yes, standard chess is one of the variants that my engine supports. I use it as a baseline that I modify when adding a new
variant to my collection. I have done very little with the chess engine itself
speed: speed in my computer(few years old Athlon) is around 2-3m nps for chess. perft 6 takes around 10 seconds.

Well, I read the linked page, and see that it's a specific type of conspiracy number search which I have read a few papers on, albeit many years ago. So, I down loaded Louis Allis's "Searching for Solutions in Games and Artificial Intelligence" which will take me a while to read. If you know of any other papers that would be of interest or complement that paper and aren't too hard to come by let me know.

From what you have said about your program it seems to have many of the capabilities that I would be interested in, in this type of program. It also seems to have good speed. The only exception would be the ability to stop and start the program as desired. So, I guess a few more questions are in order.

1.) How is the proof tree stored (format of the data). i.e. .pgn, .fen, .bin file etc.
2.) Can it display the data so you can walk through the lines on a board or output a pgn for this purpose?
3.) Does it make use of table bases? If so which ones?
4.) What language is it written in?
5.) Is the source code available or executables?
6.) # of cores supported
7.) Is it 64 or 32 bit?
8.) What OS's can it be set up for.

Thanks again.

Regards,

Forrest

[hgm]

nodes: I haven't kept track, but some have been over a trillion nodes.
depth: Again, haven't kept track of the longest ever, but in more forcing positions I've seen it get over 140 ply. These super-long lines tend to include a lot of pointless checks.
time: I've had some positions take as long as 2 weeks, I tend to get bored and terminate the search if it takes more than that.
resumability: I have a UPS, so no, it doesn't support restarts.
chess: Yes, standard chess is one of the variants that my engine supports. I use it as a baseline that I modify when adding a new
variant to my collection. I have done very little with the chess engine itself
speed: speed in my computer(few years old Athlon) is around 2-3m nps for chess. perft 6 takes around 10 seconds.

I suppose it is too much to hope for that your program ever could do Chu Shogi? I have spent the past few months solving historic mate ('tsume') problems, preserved from the Edo period (around 1700). These problems were published without solutions, and are often so difficult (despite the fact that one of the rules of 'tsume' is that every move has to be a check) that no sulutions are known to date.

I used a normal engine to work on these problems, but this at times seems to be very inefficient. The iterative deepening initially goes for material, which is not completely silly, because needlessly giving up all your powerful pieces will hurt your possibility to checkmate. But often the solution starts with enormous sacrifices to peel out the King from its fortress, so that the program has a completely wrong PV until the last iteration, where it finds the mate (and which then takes forever).

E.g. this is one of the mates I could not solve even with several days of thinking:



Guiding the early moves of the search process by hand I could prove there is a tsume mate in 16, but I did not prove this is the fastest mate.

The solutions of these problems are of fundamental importance, because they often reflect back on the rules, in particular to ambiguities in the rule descriptions of that era. Problems are often constructed to exploit a rule detail that is insignificant in normal play (comparable to under-promotion in Chess).

[Zenmastur]

I suppose it is too much to hope for that your program ever could do Chu Shogi? I have spent the past few months solving historic mate ('tsume') problems, preserved from the Edo period (around 1700). These problems were published without solutions, and are often so difficult (despite the fact that one of the rules of 'tsume' is that every move has to be a check) that no sulutions are known to date.

I used a normal engine to work on these problems, but this at times seems to be very inefficient. The iterative deepening initially goes for material, which is not completely silly, because needlessly giving up all your powerful pieces will hurt your possibility to checkmate. But often the solution starts with enormous sacrifices to peel out the King from its fortress, so that the program has a completely wrong PV until the last iteration, where it finds the mate (and which then takes forever).

E.g. this is one of the mates I could not solve even with several days of thinking:



Guiding the early moves of the search process by hand I could prove there is a tsume mate in 16, but I did not prove this is the fastest mate.

The solutions of these problems are of fundamental importance, because they often reflect back on the rules, in particular to ambiguities in the rule descriptions of that era. Problems are often constructed to exploit a rule detail that is insignificant in normal play (comparable to under-promotion in Chess).

hmmm...

Looks interesting...

Where can I find the game rules. I not too interested in getting completely sidetracked by other problems like this, but I do like to try different things as they can teach you new and different approaches to old problems or give you new perspectives. I believe this is important since the proper perception of the problem will be the deciding factor in its solution.

Wouldn't it be nice if this game was already in his play list?

Regards,

Zen

[zullil]

I wish you luck.

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

I think I have found a step in the right direction.

A search space of 10^18 still seems impossibly large. If 10^6 positions were solved per second, 100,000 years of computing would be required to enumerate all the positions. What makes the problem of finding the game-theoretic value of checkers feasible is the idea of a proof tree. When analyzing a position that is a win, one need only consider one winning move; the alternatives moves are either inferior or redundant. When considering a position that is a loss or a draw, all alternatives must be considered (since you have to prove you cannot do better). In the best case a game that is provably winning the search only has to explore roughly the square root of the search space: a single move at winning positions and all moves at losing positions. This means that a proof of the game-theoretic value of checkers might require a search of as few as 10^9 positions. Of course, knowing which 10^9 positions out of 10^18 is the hard part.

Zen

I think you've simply discovered a statement of the well-known fact that, with perfect move ordering, an alpha-beta search reduces the size of the search tree from b^d to about sqrt(b^d).

Actually, isn't the content of this already visible in the formula I posted? I certainly used the fact that only one winning move is required.

My formula says that a proof-tree for mate-in-n needs O(b^(n-1)) nodes. Since mate-in-n would require a min-max search to depth 2n-1, I've reduced the search space from b^(2n-1) to something of order b^(n-1).

[hgm]

I have a page on Chu Shogi on my website (based on the piece representations I used in the diagram above, where the shapes are mnemonics for the moves), which contains a compact list of pieces and their moves: http://hgm.nubati.net/chu/

The pages that describes the rules of all XBoard-supported variants give a more compact rule description, but it uses XBoard's pictographical representation of the pieces: http://hgm.nubati.net/rules/Chu.html

And of course it can also be found in the Wikipedia: https://en.wikipedia.org/wiki/Chu_shogi

[Zenmastur]

I think you've simply discovered a statement of the well-known fact that, with perfect move ordering, an alpha-beta search reduces the size of the search tree from b^d to about sqrt(b^d).

Actually, isn't the content of this already visible in the formula I posted? I certainly used the fact that only one winning move is required.

My formula says that a proof-tree for mate-in-n needs O(b^(n-1)) nodes. Since mate-in-n would require a min-max search to depth 2n-1, I've reduced the search space from b^(2n-1) to something of order b^(n-1).

The fact is O(b^(n-1)) doesn't produce a reasonable bound for the number of positions that can be reached from a given position. In many cases it wildly overestimates this number. Since no proof-tree may contain more positions in it than are reachable from the starting position it follows directly that O(b^(n-1)) won't produce a reasonable bound for the number of nodes in a proof tree.

The difference lies in the fact that Schaeffer and Lake use the square root of a "known good" bound. i.e. There are methods that calculate a better estimate of the number of position that are reachable from a given position than O(b^(n-1)). In effect what they are saying is that because we know that a well ordered search will have about sqrt(b^d) nodes in it, as you pointed out, and we have a better bound than b^d for the number of possible nodes reachable, lets call it "x", then a better solution is sqrt("x").

The example that I used to demonstrate this was the 549 move mate taken from the Lomonosov table bases. It has an average branching factor of ~19 (I still haven't counted the number at each black move yet). So O(19^(549-1)) gives O(5.7E+700) this number is clearly many orders of magnitude larger than sqrt(1.4E+13) where 1.4E+13 is a rough estimate that I made of the number of positions that can be reached from the starting position. Since both of these methods are estimating the same quantity and the estimates are about as far apart as one could imagine, it's should be intuitively obvious to a casual observer that the two methods are different. If you are going to claim that the idea's are the same then you need to reconcile these wildly different results.

Regards,

Zen

[zullil]

I think you've simply discovered a statement of the well-known fact that, with perfect move ordering, an alpha-beta search reduces the size of the search tree from b^d to about sqrt(b^d).

Actually, isn't the content of this already visible in the formula I posted? I certainly used the fact that only one winning move is required.

My formula says that a proof-tree for mate-in-n needs O(b^(n-1)) nodes. Since mate-in-n would require a min-max search to depth 2n-1, I've reduced the search space from b^(2n-1) to something of order b^(n-1).

The fact is O(b^(n-1)) doesn't produce a reasonable bound for the number of positions that can be reached from a given position. In many cases it wildly overestimates this number. Since no proof-tree may contain more positions in it than are reachable from the starting position it follows directly that O(b^(n-1)) won't produce a reasonable bound for the number of nodes in a proof tree.

The difference lies in the fact that Schaeffer and Lake use the square root of a "known good" bound. i.e. There are methods that calculate a better estimate of the number of position that are reachable from a given position than O(b^(n-1)). In effect what they are saying is that because we know that a well ordered search will have about sqrt(b^d) nodes in it, as you pointed out, and we have a better bound than b^d for the number of possible nodes reachable, lets call it "x", then a better solution is sqrt("x").

The example that I used to demonstrate this was the 549 move mate taken from the Lomonosov table bases. It has an average branching factor of ~19 (I still haven't counted the number at each black move yet). So O(19^(549-1)) gives O(5.7E+700) this number is clearly many orders of magnitude larger than sqrt(1.4E+13) where 1.4E+13 is a rough estimate that I made of the number of positions that can be reached from the starting position. Since both of these methods are estimating the same quantity and the estimates are about as far apart as one could imagine, it's should be intuitively obvious to a casual observer that the two methods are different. If you are going to claim that the idea's are the same then you need to reconcile these wildly different results.

Regards,

Zen

Your original post asked about "nodes" in a "proof-tree". Perhaps I don't understand what a proof-tree is.

[D]k7/P7/K4ppp/8/1P6/8/8/8 w - - 0 1

I can prove that this is mate-in-3 by presenting a tree with 26 nodes (this includes a root node representing the position itself). I don't see how any proof-tree for this position could have fewer nodes than this. Of course, some of these nodes represent the same position, but they are still distinct nodes (or it ain't a tree ).

[zullil]

Can anyone point me to a paper that deals with proof-tree sizes. I'm looking for an upper bound for the number of nodes in proof-trees. The tighter the better.

I've spent some time on the problem and it seems that a good bound might be 2*b^(n/2) where b is the branching factor and n is the number of moves in the mate but I have no proof for it.

Regards,

Forrest

To prove that the side-to-go has mate in at most n, it suffices to give one move for the side-to-go, and then for each reply by the opposing side, it suffices to prove that the side-to-go has mate in at most n-1. Assuming that there are at most b moves in any position, this leads to the recursive formula V[n] = 1 + b + b * V[n-1] = 1 + b * (1 + V[n-1]). Here V[n] denotes the number of nodes in a mate-in-at-most-n proof tree, with V[1] = 1.

From the recursion:

Code: Select all

V[1] = 1
V[2] = 1 + 2b
V[3] = 1 + 2b + 2b^2
V[4] = 1 + 2b + 2b^2 + 2b^3

so

V[n] = 1 + 2b + 2b^2 + 2b^3 + ... + 2b^(n-1).

(Take this with a grain of salt, since

(a) I'm not sure this is what you're asking about, and

(b) I thought about this for only five minutes or so.)

With a root node representing the position itself, we get

Code: Select all

V[n] = 2 + 2b + 2b^2 + 2b^3 + ... + 2b^(n-1)

       = 2 (1 + b + b^2 + ... + b^(n-1))

       = 2 (b^n - 1) / (b - 1)