# An explicit IP algorithm for chess?

If I have 2 large graphs to be tested for isomorphism, and can communicate with some (powerfull but untrusted) machine, I can choose graph at random, permute vertices, ask machine to guess which one was chosen, and the correct guess (100 times) proves me that the graphs are really non-isomorphic.

A famous IP=PSPACE theorem implies that a similar algorithm EXISTS for n$\times$n chess (with 50-moves rule): if a particular position is a winning one for whites, a machine can prove me this in polynomial time. Is it possible to formulate this algorithm in understandable way, in chess terms? It would be really interesing to see it. Also, is "polynomial time" here really implies "efficient": at least if n=8, is the number of operations I would need to perform can be done using a (standard current) computer in a reasonable time?

This is a good question and a nice way to study some complexity-theorems from the '90's. Reviewing Shamir's famous paper, it is not so much "if a particular position is a winning one for white, a machine can prove me this in polynomial time," it is more "if a particular position is a winning one for white, I can engage with a powerful prover machine in a number of rounds of challenge/response to be convinced by the prover that there is a winning position." In the challenge/response, the prover is pretty abstracted from chess and is merely proving that some polynomial over some finite field is non-zero.

For example, $$\mathcal{PSPACE}$$ refers to problems running in space polynomial to the input size. Much as $$\mathsf{3CNF}$$ is the standard example of an $$\mathcal{NPC}$$ decision problem, True Quantified Boolean Formula, $$\mathsf{TQBF}$$, is the standard example of a decision problem complete for $$\mathcal{PSPACE}$$. A $$\mathsf{QBF}$$ formula might be $$\forall x\ \exists y\ \exists z\ ((x \lor z) \land y)$$. The relation of $$\mathsf{TQBF}$$ to games such as chess or checkers is noted, in that a "white-to-mate-in-$$n$$" problem can also be cast as

$$\exists w_1\forall b_1\exists w_2\forall b_2\cdots\exists w_n:\phi(w_1,b_1,w_2,b_2,\cdots,w_n)$$ where $$\phi$$ is a Boolean encoding the rules of chess as applied to the given position. We can read this as "there is a move by white, such that for all moves by black, there is a counter-move by white, such that... white checkmates black.

Turning to $$\mathcal{IP}$$, interactive proofs involve two parties, say $$P$$ the prover and $$V$$ the verifier. $$V$$ and $$P$$ engage in rounds of challenges and responses. The "interactive proof" of graph non-isomorphism $$\mathsf{GNI}$$ given in the question is typically framed as a single round of challenge/response, that is amplified to improve soundness, say, 100 times. However, $$\mathcal{IP}$$ as used by Shamir involves a polynomial number of rounds of interaction between $$V$$ and $$P$$.

The denouement, of course, is that $$\mathcal{IP}=\mathcal{PSPACE}$$. Shamir and his predecessors showed (1) how to convert any $$\mathsf{TQBF}$$ problem into a canonical form ("simple QBF"), (2) how to "arithmetize" the simple QBF by replacing each $$\forall$$ with $$\Pi$$, each $$\exists$$ with $$\Sigma$$, each $$\land$$ with multiplication, etc. thus converting a simple QBF to a polynomial, and (3) how to have a verifier, $$V$$, challenge a prover, $$P$$, with random interactive coin tosses to establish that the polynomial is nonzero. Each round of the interaction simplifies the polynomial, and eventually, as long as $$V$$ is randomly choosing her coin tosses for each round after $$P$$ provides her answers, $$V$$ should be convinced by $$P$$,

However, $$P$$ really has to work hard to answer $$V$$'s challenges. For example, she must actually evaluate very large polynomials for each round. The work that the prover has to do does not seem very enlightening with respect to chess itself.

• Your formula for "white to mate in $n$" actually describes the existence of a strategy for black. It should begin $\exists w_1\forall b_1\dots$. Nov 20 '18 at 0:34