[Computer-go] Paper “Complexity of Go” by Robson
Mario Xerxes Castelán Castro
J. M. Robson (1983) “The Complexity of Go”. Proceedings of the IFIP
Congress 1983 p. 413-417.
I could not find it online. There is no DOI anywhere to be found (I
searched Crossref and here:
https://dblp.uni-trier.de/db/conf/ifip/ifip83.html#Robson83 ) and the
conference proceedings are not in Library Genesis either.
Thanks in advance.
Andries E. Brouwer
This is
The Complexity of GO, report TR-CS-82-14, D.C.S., A.N.U.,
also in: IFIP World Computer Congress 1983, pp. 413-417.
A.N.U. = Australian National University
A scan of this report can be found in
https://www.lri.fr/~teytaud/robson/robsonResearchReports/goisexphard/
_______________________________________________
Computer-go mailing list
Compu...@computer-go.org
http://computer-go.org/mailman/listinfo/computer-go
Marcel Crasmaru
should be the other way around :)
--Marcel
On 18 June 2018 at 19:36, Marcel Crasmaru <cras...@gmail.com> wrote:
>> J. M. Robson (1983) “The Complexity of Go”. Proceedings of the IFIP Congress 1983 p. 413-417.
>
> If you are interested in how to prove that GO with kos and Japanese
> rules is EXP complete you can get the gist of it from a very early
> draft of my master thesis
> - I used Robson's idea of reduction from GO to an EXP hard problem
> using ladders instead of pipes (he used groups
> connected through long string of pieces, aka, "pipes")
>
> If you have related questions I am happy to answer them although John
> Tromp might have even better insights - ask him too.
>
> Best,
> Marcel
>
> On 18 June 2018 at 17:54, Mario Xerxes Castelán Castro
Mario Xerxes Castelán Castro
interested in formalizing results about the game of Go as my next
project. I have have a repository of computer-verified proofs here:
https://puszcza.gnu.org.ua/projects/hol-proofs/ Right now I am still
finishing a formalization of algorithms for handling dates in the
Gregorian calendar (the ordinary calendar).
Regards.
On 18/06/18 13:23, Marcel Crasmaru wrote:
> Hi Mario,
>> J. M. Robson (1983) “The Complexity of Go”. Proceedings of the IFIP Congress 1983 p. 413-417.
>
> If you are interested in how to prove that GO with kos and Japanese
> - I used Robson's idea with ladders instead of pipes (he had groups
>
>
> Best,
> Marcel
>
Mario Xerxes Castelán Castro
On 18/06/18 13:45, "Ingo Althöfer" wrote:
> Hello Mario,
> the authors of the following paper should be able to help you:
> https://hal.inria.fr/hal-01256660/file/gocomplexities_draft.pdf
>
> Regards, Ingo.
Marcel Crasmaru
https://drive.google.com/file/d/1tLCYr74UwVQsXAE2QrcwrGALIduH34b8/view?usp=sharing
--Marcel
uurtamo
Marcel Crasmaru
like problem on a Go board but I guess I've run into difficulties and
didn't finish it:
https://senseis.xmp.net/?Crasmarum%2FStrangeTsumego
However, it might help you understand how to convert Robson's problem
instances to equivalent Go positions.
--Marcel
On 18 June 2018 at 18:42, Mario Xerxes Castelán Castro
Álvaro Begué
me that ladders are PSPACE complete: https://tromp.github.io/lad.ps
Álvaro.
Marcel Crasmaru
Actually this is not obvious.
If you are able to replace the White Choice gadget shown at page V in
this paper: https://tromp.github.io/lad.ps with an equivalent Go
gadget that doesn't capture any stone then I believe you actually
prove that first-capture go is PSPACE complete.
--Marcel
uurtamo
John Tromp
>> FWIW, first-capture go (i.e. winner is first one to make a capture) should not be PSPACE-complete.
>
> Actually this is not obvious.
>
> If you are able to replace the White Choice gadget shown at page V in
> this paper: https://tromp.github.io/lad.ps with an equivalent Go
> gadget that doesn't capture any stone
In a ladder White is reduced to 1 liberty at every Black move, so the
only way to give White a choice is to provide an alternative to
playing that single liberty; which is necessarily a capture.
regards,
-John
John Tromp
> I don't think ko fights have anything to do with this. John Tromp told
> me that ladders are PSPACE complete: https://tromp.github.io/lad.ps
Ko fights are needed to take Go problems beyond PSPACE.
For Japanese rules they suffice to go beyond (assuming EXPTIME != PSPACE),
but for Chinese rules it's an open problem.
regards,
-John
Abdallah Saffidine
uurtamo
Marcel Crasmaru
reduction from a Robson problem to Go - I hope is correct.
The Problem: https://drive.google.com/file/d/1tmClDIs-baXUqRC7fQ2iKzMRXoQuGmz2/view?usp=sharing
Black just captured in the marked ko. How should White play to save
the lower group?
> no ko fights and no counting (i.e. first capture) could put this in P.
Not true - please read Tromp et al paper: Ladders are PSPACE hard
without ko - that is, you can reduce any PSPACE problem in reasonable
time to a Go problem without kos.
--Marcel
Junyan Xu
> I am interested in formalizing results about the game of Go as my next
> project. I have have a repository of computer-verified proofs here:
> https://puszcza.gnu.org.ua/projects/hol-proofs/
I have been wondering what proof assistant I should use. Coq seems to be a suitable choice, since people have been using it for retrograde analysis in chess, and it's also what the machine learning environment GamePad uses. (https://arxiv.org/abs/1806.00608) But personally I am familiar with neither Coq nor HOL to judge which will be more efficient for proving facts about Go.
It's probably hopeless to determine the best play for an arbitrary initial position, but starting from the empty board, there should be relatively simple forced lines towards the optimal score under different rulesets: at least many human individuals have pruned the game tree enough that they are convinced of the alleged optimal solutions for 6x6 and 7x7, and computers can be more exhaustive and quicker through automation. That's why I believe producing formally verified proofs is a feasible task with the advent of deep learning.
For interested people, this 2015 article is the most comprehensive analysis of 7x7 Go (by Li Zhe 6p) I've seen: https://m.newsmth.net/article/Weiqi/615932 "In terms of tsumego difficulty, 6x6 optimal solution is about amateur 6d, and 7x7 is much harder than Hatsuyōron problems. The most important reason is that a usual tsumego has only one solution, which is not the case for an empty small board (and we have no idea how many solutions there are)." Compared to the 7x7 article by J. Davies, it also explains why some variations do not work.
There has been a debate here 10 years ago about 6x6 komi; now people seem to have settled that it's 4, but a computer proof is still lacking. If anyone has trained 6x6 networks with komi's 3.5/4.5 which have nearly 100%/0% initial winrate respectively, that would be very helpful for the move ordering in the tree search stage (and the winrate would help determine when to apply other proof tactics), but these are easy to train nowadays anyway (using Leela Zero or Minigo or whatever).
Best,
Junyan
John Tromp
> I've eventually managed to create a problem that should show a full
> reduction from a Robson problem to Go - I hope is correct.
>
> The Problem: https://drive.google.com/file/d/1tmClDIs-baXUqRC7fQ2iKzMRXoQuGmz2/view?usp=sharing
> Black just captured in the marked ko. How should White play to save
> the lower group?
It looks like White needs to hold the middle ko and either top or
bottom ko to make the ladders work.
White can start one ladder as a ko threat to take back the middle ko,
and black will then take the top ko.
Now if white (possibly using another ladder ko threat) takes back
either top or bottom ko, Black can retake
the middle one and White has made no progress. So it looks like White
is doomed?!
Marcel Crasmaru
Thank you John for verifying the problem!
I claim that White cannot use the ladders as a ko thread because:
- if W plays R4 as a ko threat then B responds with S4
- if next W takes a ko back on the board then B kills the group
locally by playing S6: the left ladder is no longer a ladder and if W
gets out of the right ladder then the bottom W group ends in 2
liberties and B can capture it
Is the above reasoning sound?
--Marcel
John Tromp
>> White can start one ladder as a ko threat to take back the middle ko, and black will then take the top ko.
> I claim that White cannot use the ladders as a ko thread because:
> - if W plays R4 as a ko threat then B responds with S4
> - if next W takes a ko back on the board then B kills the group
> locally by playing S6: the left ladder is no longer a ladder and if W
> gets out of the right ladder then the bottom W group ends in 2
> liberties and B can capture it
>
> Is the above reasoning sound?
Thanks for correcting me. You're right White can't use the ladders as
ko threats.
I also seem to have confused the formula expressed by the choice gadgets.
If we call the three kos x,y,z from top to bottom, then a succesfull
White ladder amounts to
(x || y) && (y || z). Which is equivalent to y || (x && z).
So with y currently false, and White unable to flip it, White should
take the bottom ko to make z true.
Black can the make x false, but that allows White to make y true,
after which she can successfully escape
in a ladder.
Marcel Crasmaru
I think you are right and the solution is W takes at z, B is forced to
take at x, W is forced to take at y and no matter what B does next W
escapes from one of the ladders and makes the group alive.
Now the question is how hard is to program a tsumego solver for this
(kind of) problem.
Cheers,
Marcel
uurtamo
Marcel Crasmaru
I think there is some misunderstanding here as in this thread several
problems are discussed in parallel.
If by _first capture_ you mean to find an answer to the question "what
is the computational difficulty of Capture GO?" then as far as I know
no one proved anything yet. Capture GO might be in P but to prove this
doesn't look like an easy task. I personally think it is either
(1) in P but very hard to prove it, or
(2) at least NP hard because, empirically, you may still create few
convoluted ladders that don't capture stones and interact to each
other in unexpected ways etc. Using loose ladders might be a another
way to try building NP hard instances. However, without a proof this
assumption is still as valid as (1).
I am curious what's John Tromp opinion on the above.
(Please note that the problem I've created has nothing to do with Capture GO.)
Thanks,
Marcel
uurtamo
John Tromp
> "what is the computational difficulty of Capture GO?" then as far as I know
> no one proved anything yet. Capture GO might be in P but to prove this
> doesn't look like an easy task. I personally think it is either
>
> (1) in P but very hard to prove it, or
> (2) at least NP hard because, empirically, you may still create few
> convoluted ladders that don't capture stones and interact to each
> other in unexpected ways etc. Using loose ladders might be a another
> way to try building NP hard instances. However, without a proof this
> assumption is still as valid as (1).
>
> I am curious what's John Tromp opinion on the above.
I spent some time thinking about the loss-less-ladder problem, that
asks if Black can capture
a given white group in a ladder without losing any stones herself.
I've come to suspect that this is an instance of (1), and that it
might be easier to prove than
the general capture go problem of which it is a special case.
Mario Xerxes Castelán Castro
wrong). Unfortunately I do not have time to read in detail all your
links, but I took a glance at all of them.
> I have been wondering what proof assistant I should use
and I can recommend it. I do not recommend Coq because its logic is very
complex and appears to be nowhere described in full detail. In my
opinion, formalizing something in a proof assistant whose logical
framework is uncertain defeats the purpose of formalizing the theory in
the first place. Originally I started learning Coq but I switched to
HOL4 after became aware of this shortcoming. The logic of HOL4 is very
simple (subjectively, simpler than ZFC) and a description in the natural
language customarily used for mathematics is found in the HOL4 manual.
The base logic of HOL4 is proven consistent relative to ZFC. Normally
one works by adding definitions that preserve soundness (assured by the
logical kernel). If needed, axioms can be added easily, to have a
stronger theory, losing the soundness guarantee. HOL4 is basically an
implementation of the formalization of higher order logic as a typed
lambda calculus proposed by Church in 1940.
HOL4 is written as just a library in the Standard ML programming
language. Thus it can be extended easily with derived inference rules
and the logical kernel verifies the primitive inference steps, thereby
there is no risk of introducing unsoundness with new proof tools. One
can also formalize and _run_ functional programs within the HOL4 logic.
There is an extensible library “computeLib” that returns a theorem
equating the original expression to its evaluated form according to the
transformation rules defined by the user; the resulting theorem is like
any other in that it is created using the primitive inference rules and
the same soundness guarantees apply.
> It's probably hopeless to determine the best play for an arbitrary
> initial position, but starting from the empty board, there should be
> relatively simple forced lines towards the optimal score under different
> rulesets: at least many human individuals have pruned the game tree
> enough that they are convinced of the alleged optimal solutions for 6x6
> and 7x7, and computers can be more exhaustive and quicker through
> automation. That's why I believe producing formally verified proofs is a
> feasible task with the advent of deep learning.
one would write a decision procedure for Go that generates a proof
verified by the kernel, just as we already have for Presburger
arithmetic, boolean formulas and some more.
I suspect the key to fast decision procedures for Go is using the
advances of SAT solvers: clause learning, restarts, and some heuristics.
Intuitively, I doubt that the computer learning “““advances””” applying
ANN to Go will be of any use in automated theorem proving. The field of
computer learning, and the computers used thereby have been getting
dumber since it started. Around 40 years ago computer learning was about
giving _provably_ correct answers to extremely hard problems. The hot
topics were automated theorem proving and constraint satisfaction
solvers and decision procedures. Great theoretical and practical
advances were made. Now “computer learning”, “deep learning”, etc. is
just applying heuristics at vaguely defined problems to get approximate
answers. They use the dumbest hardware that I have seen: vector
computers (“““GPGPU”””) that can only do brute number crunching with
small floats (and they are often not even IEEE 754 compliant!!!). What a
shame.
> For interested people, this 2015 article is the most comprehensive
> analysis of 7x7 Go (by Li Zhe 6p) I've seen:
> https://m.newsmth.net/article/Weiqi/615932
I can not promise any immediate result or cooperation, because I am
still working with my formalization of Gregorian calendars algorithms in
HOL4, but I am interested in writing a decision procedure for Go coupled
with the HOL4 proof assistant.
Regards.
John Tromp
> White ladder amounts to
> (x || y) && (y || z). Which is equivalent to y || (x && z).
> So with y currently false, and White unable to flip it, White should
> take the bottom ko to make z true.
> Black can the make x false, but that allows White to make y true,
> after which she can successfully escape
> in a ladder.
I have attempted to reduce this y || (x && z) problem to the minimum
number of stones
at the bottom of my Go page http://tromp.github.io/go.html, which also
contains an sgf link.
Direct link to image: http://tromp.github.io/img/WO5lives.png
John Tromp
> number of stones
> at the bottom of my Go page http://tromp.github.io/go.html, which also
> contains an sgf link.
> Direct link to image: http://tromp.github.io/img/WO5lives.png
Unfortunately, my ko gadgets don't work properly.
Black can connect 2 of her stones (eg. at P12) to break the ko for White.
Back to the drawing board...
Mario Xerxes Castelán Castro
> Unfortunately, my ko gadgets don't work properly.
> Black can connect 2 of her stones (eg. at P12) to break the ko for White.
> Back to the drawing board...
gender, but “she” always excludes men.
Dan Schmidt
Why the misandry? In English, “he” serves for both neutral and male
gender, but “she” always excludes men.
Sighris
Standards change...
... here is one starting point if you are interested in the topic, as you seem to be: https://www.apaonline.org/page/nonsexist (the American Philosophical Association's "Guidelines for Non-Sexist Use Of Language"). Searching for "gender-fair language" on the internet will turn up plenty of other resources.Dan
_______________________________________________
Computer-go mailing list
uurtamo
John Tromp
>> number of stones
>> at the bottom of my Go page http://tromp.github.io/go.html, which also
>> contains an sgf link.
>> Direct link to image: http://tromp.github.io/img/WO5lives.png
>
> Unfortunately, my ko gadgets don't work properly.
> Black can connect 2 of her stones (eg. at P12) to break the ko for White.
> Back to the drawing board...
Hopefully fixed now. Please let me know if you find any problems with
the optimizations...
Mario Xerxes Castelán Castro
excluded, is because he wants to feel excluded or is intentionally
playing the ignorant card. What happen is that the social justice
warrior-dominated United States is the source of many attempts to
redefine reality when it goes against the ultraliberal agenda.
John Tromp
Might be useful for go event organizers in need of arrow signs...
uurtamo
Álvaro Begué
pronoun selection. I am here for the discussions about computer go,
not gender politics.
Sighris
_______________________________________________
Computer-go mailing list
uurtamo
uurtamo
Mario Xerxes Castelán Castro
> I am here for the discussions about computer go,
> not gender politics.
Absolutely. Neither I am. I subscribed to ask help to finding a paper
about Go (the origin of this thread), that Marcel and Andreis kindly
helped me with, not to get misandrist propaganda.
Darren Cook
> equivalent to ladder, which frankly baffles me. I'd love to understand that.
Just different definitions of "hard"? Ko is still way harder (more
confusing, harder to discover a winning move when one exists) than
ladders in the way they each appear in typical games.
> http://tromp.github.io/img/WO5lives.png
>
> Might be useful for go event organizers in need of arrow signs...
:-)
...though it might end up with blocked corridors, as people stand around
the signs and argue about the best move, instead of going where the
organizers want them to go!
Darren
Stephan K
Stephan K
I assume after white plays at U22, black T20, white T19, black should
have a choice of playing either at S21, capturing one white stone and
leading the ladder to the top ko, or at S20, leading the ladder to the
middle ko.
However, if black plays at S21, the sequence:
wS20 bT21 wR20 bS22 wS23 bR22 wQ22 bR23 wR24
Results in a win for white, regardless of who is holding the top ko.
2018-06-22 0:27 UTC+02:00, John Tromp <john....@gmail.com>:
John Tromp
This fails the goal of saving White O5, as Black will just P5, and
White's only means of escape,
with the ladder M3 N4 N5 M5 M6, fails when Black directs it to N17.
John Tromp
Nope. Still no good. White can play O13, M11, or Q11 instead of recapturing ko.
The hunt for the simplest possible ko gadget continues...
John Tromp
Latest attempt at the usual place:
>>> at the bottom of my Go page http://tromp.github.io/go.html, which also
>>> contains an sgf link.
>>> Direct link to image: http://tromp.github.io/img/WO5lives.png
Unfortunately not as pretty as the previous arrow.
But let's get it correct before getting it pretty...
John Tromp
>>>> contains an sgf link.
>>>> Direct link to image: http://tromp.github.io/img/WO5lives.png
Enlarging the board to 29x29 allows for a much better final (I hope)
look, close to my first attempt.
-John
Marcel Crasmaru
Just one observation: I think this encodes x && y || y || z and W is
dead already thus is arguably a easier problem :)
Should make for a great wall poster.
Marcel Crasmaru
z && (y || x)
with x = 1, y = 0, z = 0 and W cannot play at z. Thus W is already
dead you cannot make the formula true.
--Marcel
Marcel Crasmaru
1. mark the middle ko and then
2. problem should be: B just captured in the middle ko and W is to
move - is the group alive?
See here: https://drive.google.com/file/d/1J5Xn4XkOqSsYx0AEBQJj6EL-SjNqNq-o/view?usp=sharing
Assuming x is the top ko, y the middle one etc. the problem is then
equivalent to
F = z && (y || x) with (x = 1, y = 0, z = 0, F is false) and W cannot play at y.
As F is false W has to take the ko at z (x = 1, y = 0, z = 1, F becomes true)
B takes at x (x = 0, y = 0, z = 1 F is false)
W takes at y (x = 0, y = 1, z = 1, F true),
B takes at z (x = 0, y = 1, z = 0, F false) and W is dead as no matter
what W does F remains false (equivalent to ladders failing for W).
--Marcel
Marcel Crasmaru
F = z || (y && x) :-)
Mea culpa I didn't see that the ladder choices are reversed. I let
other people try showing that the group is alive in John's initial
problem (last move was B capture at x, the lower side ko).
--Marcel
Marcel Crasmaru
1 the last move Black did in the ko:
https://drive.google.com/file/d/1L62m7i_IJX8FCB_8rIOwjYK3tR1GZZaq/view?usp=sharing