Nishio vs Supercolouring

AMcK · Last edited by AMcK on Sat Aug 06, 2005 8:45 am; edited 1 time in total

Apologies for the length and detail of this post but I suspect that I may have stumbled on a major breakthrough.

I finally discovered the last rule in multi-colouring that allowed it so solve all of Nick 70’s advanced colouring examples. The final trick is to propagate the multi-colour implication rules across all the possibles to prove colour identities within single possible colour maps which create new excluding pairs.

I was writing a paper on the finished theory with a worked example (anyone wants a copy email me) when several obvious conclusions hit me.

1) Colouring was a simple initial idea but it has become far too complicated because of all the bolt-on rules we had to add to make it work.

2) Most of the work is done by three very powerful principles:

a) Colouring of conjugate pairs
b) Iterative closure of the implication matrix
c) Proving colour contradictions so that we can assert colour pairs to be true/false
d) Proving colour identities so that we can discover new excluding pairs

I wondered if it would be possible to throw away everything except the above 4 ideas. So I tried to program it and it worked even better than I imagined. It ate up all the colouring examples with ease and solves many of the hardest published puzzles.

The new “supercoloring” approach uses matrix algebra to solve puzzles which have stalled using conventional methods and uses strict logic. It solves all of Rubylips’s “Nishio” puzzles without any suspect “what if” arguments. It’s very simple to program and very fast. I’ve not tried it yet but you could do it by hand on 81x81 grid paper 

I will outline the method and then show briefly how it solves Nishio 1.

1) Assign colours
Assign a different colour to every instance of every possible in the partial grid, ignoring certainties. This is quite different from simple colouring, which only colours conjugate pairs.

2) Create an exclusion matrix where excludes(u,v) = true if colour u excludes colour v somewhere on the partial grid. If we know that u=true then we can assert that v=false or if we know that u=true then we can assert that v=false. But if we only know that u=false we can assert nothing about v and if we only know that v=false we can assert nothing about u. This is quite different from simple colouring.

Formally, excludes(u,v) = not(u and v)

Colours exclude each other either if they sit as different possibles in the same cell or they are conjugate pairs of the same possible within a row, column or box. Note that the exclusion matrix is half symmetric, so that excludes(u,v) = excludes(v,u).

3) Create a conjugate matrix where conjugate(u,v) is true if colours u and v form a conjugate pair within a row, column or box.

Formally, conjugate(u,v) = (u and (not v)) or ((not u) and v)

The conjugate matrix is fully symmetrical - as in simple colouring – so that either (u=true and v=false) or (u=false and u=true). It is possible to compute the closure of this matrix by noting that if conjugate(u,v) and conjugate(v,w) then we can assert that u and w are identical and reduce the number of colours. This algorithm will iteratively determine the minimum number of conjugate colours and reduce the size of the matrices, but it is not necessary for the algorithm to complete. It’s a much better method that the clumsy ones I proposed originally for simple colouring.

4) Calculate an implication matrix where implies(u,v) is true if colour u implies v. If we know that u is true then v must also be true but if we know that u is false then we can assert nothing about v.

Formally, implies(u,v) = not(not(u) and v).

The implication matrix is easily initialised by setting implies(u,w) for every combination of u, v and w such that excludes(u,v) and conjugate(v,w).

5) Although the implication matrix is not symmetric, it is helpfully transitive. This enables us to compute the closure by iteratively setting implies(v,w) for every combination of colours u, v and w where implies(u,v) and implies(v,w). We now have everything we need to apply the two supercolouring rules.

6) The contradiction rule

If we can find a combination of colours u, v, w such that implies(u,v), implies(u,w) but excludes(v,w) then we have a contradiction which allows us to assert that u=false. This permits us to remove the possibles coloured u from everywhere on the grid. We can also assert that x=true for any colour x where conjugate(u,x), when enables us to force the possibles coloured x everywhere on the grid..

7) The identity rule

If we can prove that implies(u,v) and implies(v,u) where u and v are colours for the same possible p, the we can recolour the colour map for possible p by replacing every instance of colour v on the grid by colour u or vice-versa. We should of course do this consistently by selecting the lowest colour in every case. This may enable us to discover new excluding pairs.

That’s all there is to it … for the moment.

The puzzle “Nishio1” was one of 4 set by rubylips on Thu Apr 14 as follows: [updated 6-Aug to correct some errors in the transcript]

angusj · Site Admin

Nick70 · Posted: Sat Jul 30, 2005 10:25 am Post subject:

Thanks Andrew for the fresh look at coloring algorithms.

Of course your description is equivalent to the one I gave here, but I like the way you have formalized the final steps.

What I perhaps don't like is your use of three matrices (excludes[], conjugate[], implies[]) where I only use two (excludes[] and conjugate[]). I will give some careful thought to which of the two approaches is more efficient. I like excludes[] and conjugate[] because they are both symmetrical, while implies[] is not.
Implies[] is redundant, because it can always be derived from the other two. But that's not really important, because I use a set of rules which is equivalent to yours but doesn't need implies[] at all. This leads me to believe that my algorithm is more efficient.

angusj · Site Admin

Nick70 · Posted: Sat Jul 30, 2005 11:20 am Post subject:

angusj · Site Admin

AMcK · Posted: Sun Jul 31, 2005 1:39 pm Post subject:

Thanks for confirmation of consistency of the idea.
In its defence, the beauty of implies[i,j] is that computing the closure is that it's transitive so just a few lines of iterative code does an amazing amount of work.
I've now had to put logical backtrace from a log so that I can understand the complex logical reasoning. Example from Nishio2 below.
Interesting that it solves the Nishios Smile

AMcK

Nick70 · Posted: Sun Jul 31, 2005 3:31 pm Post subject:

angusj · Site Admin

Nick70 · Posted: Sun Jul 31, 2005 10:52 pm Post subject:

angusj · Site Admin

AMcK · Posted: Sun Jul 31, 2005 11:55 pm Post subject:

Here's the pseudo code that explains how I adapted my logical solver to do brute force - and also multiple solution counting.

Nick70 · Posted: Mon Aug 01, 2005 7:08 am Post subject:

[quote="AMcK"]

Nick70 · Posted: Mon Aug 01, 2005 7:22 am Post subject:

angusj · Site Admin