Upper bound on proof tree size

Discussion of chess software programming and technical issues.

Moderators: hgm, Rebel, chrisw

Angrim
Posts: 97
Joined: Mon Jun 25, 2012 10:16 pm
Location: Forks, WA
Full name: Ben Nye

Re: Upper bound on proof tree size

Post by Angrim »

Sorry, but that one is not in my list. I currently only do 8x8 variants, with the most work done in suicide, atomic, and crazyhouse. Not co-incidentally these are ones played on FICS.
If you already have an engine that can play that variant, it shouldn't be too hard to add some form of pn^2 search to it. And that sort of puzzle is pretty much ideal for proof number search, unless you are looking for the shortest mate. proof number search goes for most-forcing rather than shortest.
Zenmastur
Posts: 919
Joined: Sat May 31, 2014 8:28 am

Re: Upper bound on proof tree size

Post by Zenmastur »

zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG). If you want to present an argument that some other structure is a better choice feel free. I'm not anticipating any problems when using this structure.

I'm not convinced that the sqrt(number of possible descendants) is the best estimate that can be found. But, until I find something better I plan on using both methods plus some empirical data to smooth the transition space between them to determine the approximate space needed to store a proof tree.

Regards,

Zen
Only 2 defining forces have ever offered to die for you.....Jesus Christ and the American Soldier. One died for your soul, the other for your freedom.
Zenmastur
Posts: 919
Joined: Sat May 31, 2014 8:28 am

Re: Upper bound on proof tree size

Post by Zenmastur »

Ben,

Is source or an exe available for your program?

I know that I don't like giving-up code I have written so I'll understand if the answer is no.

Thanks,

Zen
Only 2 defining forces have ever offered to die for you.....Jesus Christ and the American Soldier. One died for your soul, the other for your freedom.
zullil
Posts: 6442
Joined: Tue Jan 09, 2007 12:31 am
Location: PA USA
Full name: Louis Zulli

Re: Upper bound on proof tree size

Post by zullil »

Zenmastur wrote:
zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG).
OK, so you're considering two nodes in the tree (that I've been envisioning) to be the same if they represent the same position. This makes sense (for efficiency), but the object you obtain is indeed a DAG, which to me is certainly not a "tree".

So I've been speaking of cherries and you of plums---closely related but not the same.

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

A minimal proof-DAG for this seems to have 20 nodes, while a minimal proof-tree has 26. For example, the move-sequences b5--f5--b6--g5 and b5--g5--b6--f5 lead to distinct nodes in the tree but the same node in the DAG.

OK, now many of your earlier posts make more sense to me.
Angrim
Posts: 97
Joined: Mon Jun 25, 2012 10:16 pm
Location: Forks, WA
Full name: Ben Nye

Re: Ben

Post by Angrim »

1. I can save a proof tree either in my private book format for my engine to use, which is not readily readable by anything else, or as a simple list of lines of text which consist of a list of moves. I use the second format for archival in case I make some change to my book format, and also for exchanging proofs with other people working on the same variants as I am.
2. I have a cgi program that lets me look up positions in the book using a web browser, and gives a list of moves with their values. Fairly similar to the one here(http://catalin.francu.com/nilatac/book.php) that is for suicide chess.
3. depends on the variant, there are no tablebases for crazyhouse for instance. For chess, suicide chess, and atomic chess I have and use the 5 piece tables.
4. C
5. No. Which probably makes the rest of the questions irrelevant
6. 1 core, when I last did serious work on my search a 2 core machine was rather expensive, so it was not a priority. I might get around to adding SMP support in the next few years, but 6 piece egtb are certainly higher priority, and there are still some improvements to search that should give more reward for the amount of headache.
7 either, I have compiled it on 64bit linux, and lightly tested it, but my main development machine is still 32bit.
8. linux, and should work on any unix system, but I haven't bothered to port it to windows. Should be easy to do if I had a reason though, mostly just the code to check for input would need changed.
Zenmastur wrote: 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
Uri Blass
Posts: 10282
Joined: Thu Mar 09, 2006 12:37 am
Location: Tel-Aviv Israel

Re: Upper bound on proof tree size

Post by Uri Blass »

zullil wrote:
Zenmastur wrote:
zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG).
OK, so you're considering two nodes in the tree (that I've been envisioning) to be the same if they represent the same position. This makes sense (for efficiency), but the object you obtain is indeed a DAG, which to me is certainly not a "tree".

So I've been speaking of cherries and you of plums---closely related but not the same.

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

A minimal proof-DAG for this seems to have 20 nodes, while a minimal proof-tree has 26. For example, the move-sequences b5--f5--b6--g5 and b5--g5--b6--f5 lead to distinct nodes in the tree but the same node in the DAG.

OK, now many of your earlier posts make more sense to me.
You can add also black pawns at e6 and d6 and I need the same number of nodes to see the mate that is clearly less than 20 nodes.

Uri
zullil
Posts: 6442
Joined: Tue Jan 09, 2007 12:31 am
Location: PA USA
Full name: Louis Zulli

Re: Upper bound on proof tree size

Post by zullil »

Uri Blass wrote:
zullil wrote:
Zenmastur wrote:
zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG).
OK, so you're considering two nodes in the tree (that I've been envisioning) to be the same if they represent the same position. This makes sense (for efficiency), but the object you obtain is indeed a DAG, which to me is certainly not a "tree".

So I've been speaking of cherries and you of plums---closely related but not the same.

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

A minimal proof-DAG for this seems to have 20 nodes, while a minimal proof-tree has 26. For example, the move-sequences b5--f5--b6--g5 and b5--g5--b6--f5 lead to distinct nodes in the tree but the same node in the DAG.

OK, now many of your earlier posts make more sense to me.
You can add also black pawns at e6 and d6 and I need the same number of nodes to see the mate that is clearly less than 20 nodes.

Uri
I don't understand your statement.
Uri Blass
Posts: 10282
Joined: Thu Mar 09, 2006 12:37 am
Location: Tel-Aviv Israel

Re: Upper bound on proof tree size

Post by Uri Blass »

zullil wrote:
Uri Blass wrote:
zullil wrote:
Zenmastur wrote:
zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG).
OK, so you're considering two nodes in the tree (that I've been envisioning) to be the same if they represent the same position. This makes sense (for efficiency), but the object you obtain is indeed a DAG, which to me is certainly not a "tree".

So I've been speaking of cherries and you of plums---closely related but not the same.

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

A minimal proof-DAG for this seems to have 20 nodes, while a minimal proof-tree has 26. For example, the move-sequences b5--f5--b6--g5 and b5--g5--b6--f5 lead to distinct nodes in the tree but the same node in the DAG.

OK, now many of your earlier posts make more sense to me.
You can add also black pawns at e6 and d6 and I need the same number of nodes to see the mate that is clearly less than 20 nodes.

Uri
I don't understand your statement.
My statement is that I do not need to look at 20 different chess positions to be sure that there is a mate in 3 even if I add 2 black pawns at d6 and e6.
zullil
Posts: 6442
Joined: Tue Jan 09, 2007 12:31 am
Location: PA USA
Full name: Louis Zulli

Re: Upper bound on proof tree size

Post by zullil »

Uri Blass wrote:
zullil wrote:
Uri Blass wrote:
zullil wrote:
Zenmastur wrote:
zullil wrote:
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 :D).
Louis,

As far as I have been able to determine the best structure to store a proof-tree of a mate is a Directed Acyclic Graph (DAG).
OK, so you're considering two nodes in the tree (that I've been envisioning) to be the same if they represent the same position. This makes sense (for efficiency), but the object you obtain is indeed a DAG, which to me is certainly not a "tree".

So I've been speaking of cherries and you of plums---closely related but not the same.

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

A minimal proof-DAG for this seems to have 20 nodes, while a minimal proof-tree has 26. For example, the move-sequences b5--f5--b6--g5 and b5--g5--b6--f5 lead to distinct nodes in the tree but the same node in the DAG.

OK, now many of your earlier posts make more sense to me.
You can add also black pawns at e6 and d6 and I need the same number of nodes to see the mate that is clearly less than 20 nodes.

Uri
I don't understand your statement.
My statement is that I do not need to look at 20 different chess positions to be sure that there is a mate in 3 even if I add 2 black pawns at d6 and e6.
I'm giving the number of nodes in a specific DAG related to the position. I'm not saying how many nodes you need to look at---whatever that means.

I agree that even with black pawns on d6 and e6 the number of checkmate positions is less than 20.
Zenmastur
Posts: 919
Joined: Sat May 31, 2014 8:28 am

Re: Upper bound on proof tree size

Post by Zenmastur »

A better estimate of the maximum number of nodes in a proof-tree (a DAG by any other name would smell as sweet) appears to be:

MAX_Nodes = 2 * sqrt( Number_of_possible_descendants ) / sqrt( b - 1 )

Where: b is the branching factor if known. If b is unknown then any reasonable estimate can be used without a huge effect on the results. If the number of possible descendants is greater than b ^ ( 2 * n - 1 ) then b ^ ( 2 * n - 1 ) should be used instead of the number of descendants. "n" in this case refers to the number of moves in the mate if it is known or can be WAGed. If the number of moves in the mate are unknown there may actually be a way to estimate it in some circumstances. Still working on that part of it though.

These are my thoughts on the matter ... so far!

Any questions?

I probably DON'T have the answer.

BUT...

...The first part could probably be proved as an upper bound (instead of just an estimate) if you are more practiced in your math skills than I.

Regards,

Zen
Only 2 defining forces have ever offered to die for you.....Jesus Christ and the American Soldier. One died for your soul, the other for your freedom.