[Retros] Generating proof games by computer

[Francois Labelle]

Michel Caillaud wrote:


> so I think he can program similarly the longest SPG with 2

> pieces moving? if not, tell us Francois, so the chase can begin!


I don't think that I can do this one. With two sides playing instead of 
one, the complexity is roughly squared. In this particular case it's 
probably worse.

To see why here's a primer on how to generate record proof games with a 
particular theme (say Lazy-Spectators) on a computer:

OPTION 1

Generate all games which can potentially lead to a diagram that can be 
achieved by a theme game. It doesn't suffice to generate only theme games 
because we need to make sure that a themed PG isn't cooked by a non-themed 
solution.

For option 1 I'm limited by the number of distinct positions I can 
consider at any given ply (~3e9 positions).

For R153 in Problemesis I was helped by the fact that Black doesn't move 
and most White pieces are jammed. The number of positions to consider at 
any given ply is bounded by 2^13*49*48/2/2 = 4,816,896, where 2^13 counts 
possible subsets of black pieces, 49*48/2 white knights positions, and 
divided by two because of ply parity. (There is no need to let the rooks 
move.) My computer actually found 3,421,876 positions at move 24. A few 
million positions is what I consider a problem of "medium" complexity for 
a computer.

For Lazy-Spectators, we know that the final position will be an at-home 
position with possibly 2 exceptions. But intermediate positions of 
potential cooks have no such restriction, they can be pretty much 
anything, so option 1 isn't practical.

OPTION 2

Generate only themed proof games with one solution directly, by checking 
partial games individually for a unique solution with a proof game solver 
as the enumeration progresses.

I only played a little with this idea. It's mostly limited by the running 
time. If it takes up to 1 day to check a typical PG with the theme, and 
the computer needs to call natch/popeye for thousands of positions... you 
can see the problem. So for this to work the theme must be easily 
checkable by computer.

A COMPROMISE

Instead of shooting for the theoretical maximum I can always take a guess 
and search for only one particular type of solution that should be good 
enough to compete with humans, and is restricted enough to be computable. 
Sort of another level in computer-aided composition: above using proof 
game solvers to test ideas, but not quite pressing a button and resolving 
the question completely.

CONCLUSION

Proof game composition is still dominated by humans. For example I looked 
at the Messigny 2004 and Champagne 2004 retro composing tourneys, and 
didn't see a way to compose these kinds of proof games by computer. This 
is in strong contrast with "playing chess" where computers dominate. So 
Michel, don't be pessimistic, with chess problems you chose the right 
field!

 	Francois