The graph HCrb‘rk is now solved. Patrick added the efficiently computable lower bound max_odd_minus_odd_horizontal, which correctly predicted the independence number and matched the best computed upper bound.
Then Patrick ran INP to find the next difficult graph – which has 10 vertices. So, n=9 is solved (it was solved before using my branch of the code – and a more costly version recursive version of max_even_minus_even_horizontal – but now we’ve switched exclusively to Patrick’s code). This means that every graph with fewer than 10 vertices can either be reduced in polynomial time – or the independence number can be predicted from efficiently computable lower and upper bounds which match. On to n=10!
The next difficult graph is I?b@fd}^_ Here’s a picture: