Computer programs tournament

[Ed Trice]

As we have been over many times of this forum - Chinook team used heuristics in constructing the proof tree making their method unsound. The absolute minimum requirement for solving checkers is that a sound method is used. So no Chinook has in no way solved checkers.

Another aspect is that they don't have all the reachable nodes in their proof tree so if Chinook was to play a game there would be positions after the opening and before they reach the endgame databases where they would have to use a regular search. Therefore it is very likely they would lose a game.

I disagree with both of these remarks.

1. The Chinook team removed the last shadow of doubt when they corrected the Graph History Interaction problem, commonly referred to as "GHI." This is described at the bottom of page 471 in the One Jump Ahead: Computer Perfection at Checkers (OJA:CP@C) book. Basically, it deals with transpositions being labeled as draws if they were previously evaluated, so the newly-recurring positions do not spawn more positions, thereby bloating the game tree. It occurs very infrequently, but it was enough to cast a shadow of doubt over any results that might be announced wherein GHI possibilities could have arisen. The solution: write code that handled GHI. Schaeffer hired Akihiro Kishimoto, who won a "best paper prize" in 2002 for his pioneering work in dealing with GHI in parallel searching programs. Teaming up with Martin Muller, they were both tasked with solving the GHI problem in its entirety. They succeeded. See page 473 for confirmation of this.

2. Chinook can search and reach previously solved nodes, and due to captures being forced, these Proof Tree Nodes are inescapable. Murray Cash did something similar with Nemesis; namely, he created "Middlegame Landings" that resided in RAM. These landings were proven draws he encountered during his opening book generation process as it ran across a network of 14 workstations. With enough middlegame positions loaded into a hash table, Nemesis did not have to worry about any "holes" in its opening book. Where possible, it would divert the play into a previously drawn landing. Chinook does this on a GALACTIC scale. There is no way you or anyone else can convince me otherwise. It is well documented, and the Schaeffer claim to have solved checkers drew the attention of the leading minds in the artificial intelligence community. They rigorously tested his proof, and it was certified as being correct.

[Ed Trice]

Privet, Ed !

Hello there Alex.

Chinook can at least draw

True for GAYP

The first opening Schaeffer set out to tackle was the White Doctor. The last opening he solved was the Black Widow. Read pages 495 and 496 of One Jump Ahead: Computer Perfection at Checkers.

and will always win once an opponent makes a losing move.

Not true. This is not a part of scientific proof. Chinook team only claimed that program never makes a losing move in GAYP games. This is the lowest level of solving checkers.

The proof tree was generated using 10,000,000 searches of which 3,300,000 made it into the tree. Each search examined 1,000,000 separate positions that were backed up by the 10-piece databases. The solver could search 30 ply, the proof tree was expanded to 154 ply, and I recently discovered the longest win in checkers which is now 291 ply. There are longer wins than my discovery, because it is only in an 8-piece position, and not 10 pieces. That means, all total, Chinook examined every position to at least a depth of 475 ply, which is 238 moves for the winner, and 237 moves for the loser.

You can't convince me that it cannot win a won position with 475+ ply of information at its disposal. It might take a very long time to win in a difficult position, but it will still win.

[MostFamousDane]

I disagree with both of these remarks.

1. The Chinook team removed the last shadow of doubt when they corrected the Graph History Interaction problem, commonly referred to as "GHI."

Well I guess my post proves otherwise . The articles I have read through are extreme thin on details especially regarding the soundness of their search. Let say theoretically you setup a program like kingsrow and let it think for millions of years on the start position and it returns a value - then you have not soundly solved checkers. A standard search is filled with with techniques that improve the performance of the search unsoundly. In a standard playing/analysing context it makes sense because it enables the search to go deeper. In a solving context this doesn't make sense. An example is using zobrist keys. To use search in a solving context you owe to go through each technique you use and argue for the soundness of each technique and the soundness of the complete solution. I have not seen them do this. Their papers just focus on their solver and then say they used Chinook to search.

They posted on their homepage that they had increased the search because they weren't searching far enough ie they are cutting of lines when the look bad enough (probably +2 or +3 pieces). I posted some fortress position earlier to prove that this is not valid.

Someone wrote to them about the issues (I forgot who) and their answer was something along the line of "oh we can never be completely certain since there can be hardware faults etc". This is what they write in their paper on the subject :

"Are the results correct?

Early
on in the computation, we realized that there
were many potential sources of errors, including
algorithm bugs and data transmission errors.
Great care has been taken to eliminate any pos-
sibility of error by verifying all computation
results and doing consistency checks. As well,
some of the computations have been indepen-
dently verified (SOM text).
Even if an error has crept into the calcula-
tions, it likely does not change the final result.
Assume a position that is 40 ply away from the
start is incorrect. The probability that this er-
roneous result can propagate up 40 ply and
change the value for the game of checkers is
vanishingly small"

I am interpreting their stance as they know that their method is not completely sound and since the possible wrong evaluations here and there is not likely to change the evaluation of the start position. Ie they have sortof proved that the starting position is a draw not all their evaluations are necessarily correct.

2. Chinook can search and reach previously solved nodes, and due to captures being forced, these Proof Tree Nodes are inescapable. Murray Cash did something similar with Nemesis; namely, he created "Middlegame Landings" that resided in RAM. These landings were proven draws he encountered during his opening book generation process as it ran across a network of 14 workstations. With enough middlegame positions loaded into a hash table, Nemesis did not have to worry about any "holes" in its opening book. Where possible, it would divert the play into a previously drawn landing. Chinook does this on a GALACTIC scale.

Ah you don't understand my point here is some more text from their article:

"The stored proof tree is only 10*7
positions.
Saving the entire proof tree, from the start of the
game so that every line ends in an endgame
database position, would require many tens of
terabytes, resources that were not available.
Instead, only the top of the proof tree, the
information maintained by the manager, is stored
on disk. When a user queries the proof, if the end
of a line of play in the proof is reached, then the
solver is used to continue the line into the
databases. This substantially reduces the storage
needs, at the cost of recomputing (roughly 2 min
per search)."

The time obviously varies depending on which position is reached so even if the proof was sound - under time constraint they would not necessarily be able to pick the right move.

There is no way you or anyone else can convince me otherwise.

It is well documented, and the Schaeffer claim to have solved checkers drew the attention of the leading minds in the artificial intelligence community. They rigorously tested his proof, and it was certified as being correct.

Well I have not seen any publications that seriously tried to verify this and most importantly I have not seen the complete source code anywhere!!!.

Also you are saying argumentation doesn't matter - you just blindly trust authority ? I think we are having a culture difference here!!

[Ed Trice]

The articles I have read through are extreme thin on details especially regarding the soundness of their search.

I've read every paper on checkers Schaeffer has published. He cited some of my own published papers in more than one of his papers.

I would be delighted to see the list of papers you think are "thin on details." Please list them in your reply.

Let say theoretically you setup a program like kingsrow and let it think for millions of years on the start position and it returns a value - then you have not soundly solved checkers.

Wow, do you even know who you are in communication with? Of course I know this.

A standard search is filled with with techniques that improve the performance of the search unsoundly.

Name every technique that is unsound in your reply.

I posted some fortress position earlier to prove that this is not valid.

And I can post one position with 8 pieces total on the board that you cannot tell me how to win with best play for both sides. This has no bearing on the Chinook proof.

"Are the results correct?

Early
on in the computation, we realized that there
were many potential sources of errors, including
algorithm bugs and data transmission errors.
Great care has been taken to eliminate any pos-
sibility of error by verifying all computation
results and doing consistency checks. As well,
some of the computations have been indepen-
dently verified...

That was their admission, which is not anything close to the capitulation you stated:

As we have been over many times of this forum - Chinook team used heuristics in constructing the proof tree making their method unsound. The absolute minimum requirement for solving checkers is that a sound method is used. So no Chinook has in no way solved checkers.

Your statement is blatantly incorrect.

Would you like Dr. Schaeffer's email address? Don't you think you should tell him why he is wrong?

Saving the entire proof tree, from the start of the
game so that every line ends in an endgame
database position, would require many tens of
terabytes, resources that were not available.
Instead, only the top of the proof tree, the
information maintained by the manager, is stored
on disk. When a user queries the proof, if the end
of a line of play in the proof is reached, then the
solver is used to continue the line into the
databases. This substantially reduces the storage
needs, at the cost of recomputing (roughly 2 min
per search)."

That's exactly what I said as well. It searches until it encounters a previously solved landing. Which is all that it needs to do to solve checkers. You statement here is in perfect agreement with me, which just means you don't understand what you are referring to.

Also you are saying argumentation doesn't matter - you just blindly trust authority ?

You just blindly disagree with the result, and you don't have a decent grasp on what was required for him to make the claim. If his proof was determined to have been flawed, it would have been a career-ending moment. That's why he took every precaution, verified and re-verified and then independently had his results verified.

Or can the "MostFamousDane" just say "No you didn't" to anything anyone has ever published?

[Alex_Moiseyev]

You just blindly disagree with the result

On my end I totally agree and 150% accept result of scientific research and proof - "GAYP is drawn game"

In reality people knew this fact more than 100 years ago and we can say that checkers (GAYP) were solved at the end of 19th century. This is about true because they started 2-moves restriction play around this time. I think first mixed match (GAYP + 2 moves games) was played in 1896 ... correct ?

AM

[George Hay]

Hi Sune, it was Richard Pask who wrote to Dr. Schaeffer, and this is the quote from Ricahrd Pask's post:

Hello everyone!

As a matter of fact, I sent Dr Schaeffer the fortress position for Chinook to persuse about 15 or so years ago. (I still have his reply.) He agreed that it was beyond its search horizon.

by Richard Pask
Thu Sep 13, 2012 2:16 am

Forum: General Discussion
Topic: Why Checkers is NOT easier than Chess

The topic link is: viewtopic.php?f=1&t=3052

Interesting discussion on "checkers solved" or not, as checkers challenges the mind in more ways than one!

--George Hay

[MostFamousDane]

The articles I have read through are extreme thin on details especially regarding the soundness of their search.

I've read every paper on checkers Schaeffer has published. He cited some of my own published papers in more than one of his papers.

I would be delighted to see the list of papers you think are "thin on details." Please list them in your reply.

If you go back in this thread you will see two links to the articles available on the Chinook website.

Let say theoretically you setup a program like kingsrow and let it think for millions of years on the start position and it returns a value - then you have not soundly solved checkers.

Wow, do you even know who you are in communication with? Of course I know this.

Well if you do realize that as a starting point searching is not valid in a proof context then I just can't understand why you think it is OK to use it in this context without further argumentation. If you can find this argumentation in their article feel free to post it.

A standard search is filled with with techniques that improve the performance of the search unsoundly.

Name every technique that is unsound in your reply.

I gave you two examples earlier: futility pruning and zobrist keys there might be more.

I posted some fortress position earlier to prove that this is not valid.

And I can post one position with 8 pieces total on the board that you cannot tell me how to win with best play for both sides. This has no bearing on the Chinook proof.

Of course it has - it is an illustration of why you can't futility prune if your goal is to solve checkers.

"Are the results correct?

Early
on in the computation, we realized that there
were many potential sources of errors, including
algorithm bugs and data transmission errors.
Great care has been taken to eliminate any pos-
sibility of error by verifying all computation
results and doing consistency checks. As well,
some of the computations have been indepen-
dently verified...

That was their admission, which is not anything close to the capitulation you stated:

As we have been over many times of this forum - Chinook team used heuristics in constructing the proof tree making their method unsound. The absolute minimum requirement for solving checkers is that a sound method is used. So no Chinook has in no way solved checkers.

Your statement is blatantly incorrect.

Would you like Dr. Schaeffer's email address? Don't you think you should tell him why he is wrong?

No thank you - I find his behavior in this absolutely appalling and have no desire to communicate with him - I seriously doubt anything productive would come from this. We have had this debate many times on this forum I know he is aware of this and he has had amble opportunity to react to the criticism. Also he is not wrong about the soundness of his proof METHOD since he has not to my knowledge argued for its soundness anywhere.

Saving the entire proof tree, from the start of the
game so that every line ends in an endgame
database position, would require many tens of
terabytes, resources that were not available.
Instead, only the top of the proof tree, the
information maintained by the manager, is stored
on disk. When a user queries the proof, if the end
of a line of play in the proof is reached, then the
solver is used to continue the line into the
databases. This substantially reduces the storage
needs, at the cost of recomputing (roughly 2 min
per search)."

That's exactly what I said as well. It searches until it encounters a previously solved landing. Which is all that it needs to do to solve checkers. You statement here is in perfect agreement with me, which just means you don't understand what you are referring to.

You do realize that in checkers pieces don't get put back on the board - positions (typically with 12 pieces) at the BOTTOM are cut off. It was stated earlier that if Chinook was playing in the tournament it would not lose any game. The above statement has no consequence for the validity of the proof but it has consequences for Chinook to actually be able to produce a draw under time constraints.

Also you are saying argumentation doesn't matter - you just blindly trust authority ?

You just blindly disagree with the result, and you don't have a decent grasp on what was required for him to make the claim. If his proof was determined to have been flawed, it would have been a career-ending moment. That's why he took every precaution, verified and re-verified and then independently had his results verified.

Or can the "MostFamousDane" just say "No you didn't" to anything anyone has ever published?

No but lets say somebody claims to have invented a perpetual motion machine I am going to be skeptical.

[George Hay]

Ed Trice, I appreciate your references to One Jump Ahead, revised edition. I did look up the pages you mentioned and it makes for interesting reading. Dr. Schaeffer used algebraic notation with square a1 on the white side, with black moving first. Dr. Schaeffer's explanation of only 13 openings needed on page 485 seemed a bit convoluted to me, perhaps due to three-move openings being used instead of two-move openings. My layman's understanding of weekly solving checkers with only thirteen (two-move) openings would be to first open with black with a strong move, say 11-15, and then reply with the seven possible moves of white. Then repeat the process with a strong opening move for white, say 22-18, to all of blacks seven opening moves. That would be 7+7=14, but since 11-15, 22-18 shows up in each sequence of seven, then it is 14-1=13, or only 13 two-move openings needed to start weekly solving checkers!

--George Hay

[megamau]

Dear Ed, Sune, Alex,

We are speaking of a fairly uncontroversial topic, no need to get too heated.

and will always win once an opponent makes a losing move.

Not true. This is not a part of scientific proof. Chinook team only claimed that program never makes a losing move in GAYP games. This is the lowest level of solving checkers.

Alex is right on this one. They weakly solved the game, meaning that Chinook will never lose the game with either color from the starting position, but may not win if the opponent makes a losing move.
Of course it will still win most of the time, but it is not "proven". Otherwise it would have had to strongly solve checkers.

On my end I totally agree and 150% accept result of scientific research and proof - "GAYP is drawn game"
In reality people knew this fact more than 100 years ago and we can say that checkers (GAYP) were solved at the end of 19th century. This is about true because they started 2-moves restriction play around this time. I think first mixed match (GAYP + 2 moves games) was played in 1896 ... correct ?

Player suspected/conjectured that GAYP is drawn, but they didn't know for a fact. This is the main point of Schaeffer Proof.

No but lets say somebody claims to have invented a perpetual motion machine I am going to be skeptical.
Of course it has - it is an illustration of why you can't futility prune if your goal is to solve checkers.
As a matter of fact, I sent Dr Schaeffer the fortress position for Chinook to persuse about 15 or so years ago. (I still have his reply.) He agreed that it was beyond its search horizon.

The fact that checkers is a draw seem hardly similar to a perpetual motion machine. As said above it has been actually suspected for more than 100 years.

Regarding the futility pruning / zobrist key and other issues with the proof manager, the key thing is that the proof manager is heuristic.
You don't need to be exact/sound when deciding which line to analyze; you need to be exact/sound when proving the value of the position at the end of the line.
Let's make an example at the very start of the game. It could be that 10-15 is also a draw, but much more difficult to prove than 09-13.
The proof manager uses heuristics to decide on which move the effort of the solver will be concentrated (09-13). Then the solver need to be "sound" to prove that 09-13 is a draw. The 10-15 move had never been analyzed with "sound" methods, only discarded heuristically but it doesn't matter.

Regarding the fortress position by Pask: the fact that Chinook can not see it, does not invalidate the proof. If the fortress position is never reached in the proof-tree from the initial position, the solution is irrelevant for weakly solving. For all we know Chinook may not be able to draw the 2vs1 in the corner, but it doesn't matter if it can provably never reach this ending.

[George Hay]

You just blindly disagree with the result

On my end I totally agree and 150% accept result of scientific research and proof - "GAYP is drawn game"

In reality people knew this fact more than 100 years ago and we can say that checkers (GAYP) were solved at the end of 19th century. This is about true because they started 2-moves restriction play around this time. I think first mixed match (GAYP + 2 moves games) was played in 1896 ... correct ?

AM

Mr. Alex, I appreciate your clarifying and consistent remarks on Chinook through the years.... As for restrictions used in World Championship Match checkers, it is indeed an incomplete and scattered history. The first WCM's were pure GAYP, but later what is listed as old GAYP WCM's was by contract with some combination of GAYP, modified one-move restriction, and/or drawing openings from a hat! I read different explanations of the restrictions used in the 1894 WCM J. Ferrie vs J. Willie ((13-6-69). The 1894 match is in More Memorable Matches by Jim Loy, but without commentary on the restrictions used. If the 1894 match is all two-move, it is not in sets of two games! The Checker Games Of Richard Jordan by Jim Loy has the first standard two-game alternating set two-move WCM in 1896, R. Jordan vs J. Ferrie (4-3-33). The 1896 games themselves are all played in sets of two of a two-move opening.

--George Hay

[Ed Trice]

If you go back in this thread you will see two links to the articles available on the Chinook website.

I will not do that. Reply directly. I want no room for misinterpretation.

Well if you do realize that as a starting point searching is not valid in a proof context then I just can't understand why you think it is OK to use it in this context without further argumentation. If you can find this argumentation in their article feel free to post it.

You are missing the point. I am fully aware that a single search for an infinite amount of time is nowhere near what is required to issue a statement of proof. The Chinook team conducted 10,000,000 separate searches. Of these 10,000,000 searches, about 1/3rd resulted in data that was integrated into the proof tree. Each of these individual searches examined no fewer than 10,000,000 positions (I left a zero off of my first post, it was 10^7 not 10^6) which were searched with a 10-piece database loaded into RAM.

10,000,000 searches times 10,000,000 positions searched each time with a 10-piece database at the back end is what was needed to prove checkers is a draw from the starting position.

A standard search is filled with with techniques that improve the performance of the search unsoundly.

Name every technique that is unsound in your reply.

I gave you two examples earlier: futility pruning and zobrist keys there might be more.

Futility pruning is not the same thing as what the Chinook team was doing with conspiracy number searches, and certain has no bearing on their data obtained after the Graph History Interaction problem was resolved.
The fact that you list "Zobrist keys" tells me you 100% have no clue what you are talking about. That is a hash table function wherein collision resolution is possible, and it is used more for games like chess than anything else.
You don't need Zobrist hashing for checkers, and, in fact, there are much better ways to hash checkers positions.

You also said "a standard search is filled with unsound techniques," yet you furnished only 2 examples, neither of which are directly applicable to the Chinook project.

You have grossly exaggerated your point, and your point was flawed anyway.

Your next post regarding "fortress positions" makes no sense to me, so I will leave it alone.

Would you like Dr. Schaeffer's email address? Don't you think you should tell him why he is wrong?

No thank you - I find his behavior in this absolutely appalling and have no desire to communicate with him - I seriously doubt anything productive would come from this. We have had this debate many times on this forum I know he is aware of this and he has had amble opportunity to react to the criticism. Also he is not wrong about the soundness of his proof METHOD since he has not to my knowledge argued for its soundness anywhere.

What is the color of the sky in your world? Because you certainly do not live in mine.

I won't argue with you anymore, because it is not fair to fight a battle of wits with an unarmed person, such as yourself.

[Ed Trice]

Alex is right on this one. They weakly solved the game, meaning that Chinook will never lose the game with either color from the starting position, but may not win if the opponent makes a losing move.
Of course it will still win most of the time, but it is not "proven". Otherwise it would have had to strongly solve checkers.

As the only person presently on planet earth that has published strong solutions for the game of checkers, I can say with 100% certainty that you are wrong on this one.

A strong solution is the "perfect play" from start to finish where one side has a win. It is a win in the fewest number of moves possible, when pitted against the strongest resistance. See WCC Platinum III for strong solutions through 7 pieces.

"Weakly solving" checkers only means being able to forecast the game theoretical result from the starting position, which is a draw, no surprise to anyone.

Chinook can win every won position, though not with the precision of a strong solution. The reason is: Chinook only declares a win once it has an inescapable path to the database win/proof tree win. Unlike humans, Chinook does not make claims it cannot back up.

[MostFamousDane]

What is the color of the sky in your world? Because you certainly do not live in mine.

I won't argue with you anymore, because it is not fair to fight a battle of wits with an unarmed person, such as yourself.

That is a shame surely you must have more insults to sling.

[megamau]

Alex is right on this one. They weakly solved the game, meaning that Chinook will never lose the game with either color from the starting position, but may not win if the opponent makes a losing move.
Of course it will still win most of the time, but it is not "proven". Otherwise it would have had to strongly solve checkers.

As the only person presently on planet earth that has published strong solutions for the game of checkers, I can say with 100% certainty that you are wrong on this one.
A strong solution is the "perfect play" from start to finish where one side has a win. It is a win in the fewest number of moves possible, when pitted against the strongest resistance. See WCC Platinum III for strong solutions through 7 pieces.
"Weakly solving" checkers only means being able to forecast the game theoretical result from the starting position, which is a draw, no surprise to anyone.Chinook can win every won position, though not with the precision of a strong solution. The reason is: Chinook only declares a win once it has an inescapable path to the database win/proof tree win. Unlike humans, Chinook does not make claims it cannot back up.

I hope there is no "semantic" misunderstanding, but the claim that "Chinook can win every won position" is not proven.
It may be true, but it is not proven; for what we know, even Kingsrow and Cake could be able to win every won position, but nobody has proven that.
If a program could win every won position and draw every drawn position, it would have strongly solved checkers.

I quote from the article "Solving Checkers", which you can find at http://disi.unitn.it/~montreso/asd/docs/checkers.pdf
Underline is mine

Perfection implies solving a game: determining the final result (game-theoretic value) when neither player
makes a mistake. There are three levels of solving a game (6). For the lowest level, ultra-weakly solved, the perfect-play result is known but not a strategy for achieving that
value (e.g., Hex is a first-player win, but for large board sizes the winning strategy is not known (7)). For weakly solved games, both the result and a strategy for achieving it
from the start of the game are known (e.g., Go Moku is a first-player win and a program can demonstrate the win (6)). Strongly solved games have the result computed for
all possible positions that can arise in the game (e.g., Awari (8)).

This paper announces that checkers has been weakly solved. From the starting position (Fig. 1A), we have a
computational proof that checkers is a draw. The proof consists of an explicit strategy that never loses – the
program can achieve at least a draw against any opponent, playing either the black or white pieces. That checkers is a
draw is not a surprise; grandmaster players have conjectured this for decades.

[Ed Trice]

I hope there is no "semantic" misunderstanding, but the claim that "Chinook can win every won position" is not proven.
It may be true, but it is not proven; for what we know, even Kingsrow and Cake could be able to win every won position, but nobody has proven that.
If a program could win every won position and draw every drawn position, it would have strongly solved checkers.

I think this will clear things up:

1. Ultra-weakly solved means being able to announce the theoretical value of the starting position. Chinook announces it as a draw.
2. Weakly solved means winning every winnable position, not losing from the starting position, and being able to hold a draw from any position that is a draw. This is what Chinook can do.
3. Strongly solved means "Win in X" can be announced from any position in which there is such a win, and there is no solution shorter than X, nor is there a defense that allows the game to go on to move X+1 or more. Only 1 program in the world can do this, and it can only do this for 7 pieces or fewer. This is WCC Platinum III, which I am the co-author. I will soon have 8-pieces strongly solved.

Edit: I think I see the issue. We have been using slightly different versions of these terms.