Table Solving

MadOverlord · Posted: Tue Jul 26, 2005 5:50 pm Post subject: Table Solving

Over the past couple weeks, I've been working on a new deduction method that shows some promise, but I'm going to need some help in order to develop it further. The basic idea is to make tables of assertions about the puzzle and their implications, expand them, and look for contradictions that tell us things.

As you know, my interest is in algorithms that are "human executable". I personally suck at recognizing spatial patterns in the puzzles (the various cycles, wings, etc), so I decide to see if logical assertions about puzzles could be organized in a useful way.

To demonstrate it, I'll use the Menneske.no Super Hard #900610 puzzle. After doing the basic solving operations (but nothing fancy like Nishio, Bowman, Fishy Cycles or chains), we get to this state:

Nick70 · Posted: Tue Jul 26, 2005 7:36 pm Post subject:

I think that the table solving method is equivalent to the advanced coloring + advanced aliasing method.

Advanced coloring + advanced aliasing works like this:

1/ color pencilmarks (not cells) using conjugate colors for conjugate possibilities (i.e. only two candidates in a cell, only two position for a number in a unit). Make sure to follow all conjugations to use the least possible number of colors.
Pencilmarks that don't have conjugates should be colored anyway (they will have a unique color, whose conjugate is not present on the grid)

2/ take note of all exclusions. Exclusions are all colors that are, somewhere on the grid, in the same unit and therefore cannot be both true at the same time (but they can be both false at the same). All conjugate colors are exclusions by definition, but there are many more exclusions on the grid. For example if pencilmark 3 is in three cells in row 1, with colors A+, E+ and L-, then A+ ~ E+, A+ ~ L-, E+ ~ L- are exclusions.
[I'm using + and - after the color to indicate conjugation. A+ and A- are conjugate colors]

3/ use conjugate colors to expand the table of exclusions:
if A+ ~ B+ and B- ~ C+, then A+ ~ C+
That's because if A+ is true, B+ is false, then B- is true (because it's conjugate to B+), then C+ is false. Conversely, if C+ is true then A+ is false.

Bring 3/ as far as possible. During the process, several things can happen:

a/ you prove that e.g. A+ ~ A+. This means that A+ is false, so you have proven that A- is true, and you can immediately promote all pencilmarks colored that way to big numbers.
b/ you prove that e.g. A+ ~ B+ and A- ~ B+. This means that B+ is false, thefore B- is true and you can promote the pencilmarks colored that way.
c/ you prove that e.g. A+ ~ B- and A- ~ B+. This means that A+ = B+ and A- = B-. You may recolor the pencilmarks if you want, this will make the table smaller and easier to work with.

a/ b/ and c/ all work just by looking at the table of exclusions, without looking anymore at the sudoku grid.

The process up to this point should be equivalent to double forcing chains: everything that can be proven by a double forcing chain can be proven by this use of coloring, and everything that can be proven by this use of coloring can be proven by a double forcing chain.

If you look back at the grid, you can make it even more powerful:

d/ look at a set of colors that cover all possibilities for a cell or a unit. E.g. if candidate 3 in row 1 can be in three cells, that have pencilmarks A+, C- and D+. If A+ ~ G-, C- ~ G- and D+ ~ G-, then G- is false and G+ is true.

With the addition of d/, the process should be equivalent to multiple forcing chains.

The advantage of coloring over forcing chains is that, when you work on the color table, you work on a set smaller than the set of pencilmarks on the grid; therefore, on a simpler set.
The advantage of forcing chains is that, while harder to find, they are easier to follow and verify. And they aurely are more satisfying as a proof.

Coloring is more efficient to verify the existence of a forcing chain, however once the existance of such a chain is proven through coloring, it isn't trivial to reconstruct it. Also, you can't find a minimal forcing chain with coloring alone.

tilps · Posted: Wed Jul 27, 2005 11:06 pm Post subject:

That puzzle from Bowman is indeed very evil, my solver rated it a 1.12.4, requiring 12 iteration of forced lookaheads from a column with 4 options in the number 2, the 12 iterations average about 2 forced placements eachrequired for the next iterations deduction on the hardest branch of the 4.

That would make it the 3rd highest rated puzzle my solver has ever seen. Although i'm not convinced that with a 12 lookahead its not harder then both of the '2' rated puzzles which I have generated myself. I am currently in the process of formalizing a new 'better' way of rating the difficulty of various constructive logics, but it looks like it could be very slow to execute.

Doug · Posted: Thu Aug 04, 2005 12:25 am Post subject:

Edit: The puzzles I originally put here were defective and had more than one solution.

tilps--

How does your program produce the difficulty rating? (Specifically, are you basing the difficulty on your "minimal solver logic" implementation, or using the more prosaic backtracking counts ideas?)

Could you post the other top difficulty puzzles? I would love to see them!

Thanks.
_________________
Doug Bowman
www.flickr.com/photos/bistrosavage

MadOverlord

Thanks to some insights from Doug Bowman, we have managed to add some things to the Tables algorithm that permits it to crack the puzzle listed above!

Doug pointed out the following:

1) There is a new type of eternal verity we've dubbed a "veracity". If there are N squares in a group that can have value V, then the intersection of the =V assertions for these squares (what they have in common) must be true no matter what.

Example: In R1, only R1C1, R1C2 or R1C3 can have the value 4. Any implication that is in R1C1=4,R1C2=4 and R1C3=4 must be true for the entire puzzle.

2) Negative assertions (ie: R1C1<>1) can be computed from the positive assertions. For example, if R1C1=123, then R1C1<>1 is the intersection of R1C1=2 and R1C1=3.

I also noticed that there is a new type of verity, the exclusion verity. Any statement held in common by an assertion and its negative must be true (ie: the intersection of R1C1=1 and R1C1<>1). In practice, this finds the same verities as the regular kind, but they are easier for humans to see.

With the addition of these insights, the Menneske.no Super Hard #900610 puzzle cracks. It doesn't give up easily, though -- 49 more rounds of deduction, including Bowman Bingo, Nishio and Fishy Cycles are needed to crack it. The tables algorithm finds a single veracity (R2C6 <> 6) that opens the puzzle.

The next release of Sudoku Susser (1.2.6) will have a cleaned up version of the tables algorithm for people to play with. Also, Doug thinks there are more insights to be tweaked out of it, because there are problems that Bowman Bingo solves that Tables sticks on. He believes that Tables should be a superset of all the advanced algorithms.

Tilps says he's seen tougher puzzles. Let's see them.

Nick70

MadOverlord

Nick70

MadOverlord · Posted: Wed Aug 10, 2005 6:27 pm Post subject:

I've now added Tables (with some elegant extra tweaks Doug pointed out) to the Susser as an automatic deductive method. Here's the path to cracking the current "most difficult" puzzle.

I have modestly named this technique "Trebor's Tables"...

Note that currently Bowman Bingo can find things that Tables cannot, and vice-versa. Doug thinks that Tables has a blind-spot and that once we find it, it'll be a superset of Bingo. For this reason, in my automatic deductions, I'm running Bingo first, then Tables, at least for now. However, it seems that running Tables first generates shorter crack paths, so I'll probably flip them.

MadOverlord · Posted: Wed Aug 10, 2005 6:41 pm Post subject:

Running the Susser with Tables before Bingo gives this crack path. It also shows how many inferences Tables can generate!

MadOverlord

I am pleased (and quite proud) to announce that Doug Bowman and I have gotten the Tables algorithm extended to the point where it now cracks all known Sudoku puzzles without any guessing -- purely by logical deduction.

The crucial insight came when Doug took a close look at the inferences Bowman Bingo was making in particular cases and compared them to the current Tables algorithm. He noticed that Bowman was looking at both forces and pins, wheras Tables was only looking at forces. Adding pins to the mix did the trick.

Tables is human-executable with pencil and paper (and inhuman patience).

It will take us a few days to clean up the algorithm and trim it down to the simplest subset of possible inference operations. We'll post a complete description of the algorithm then.

Whew. Been a while since I pulled an all-nighter!

Here's the log of the solve:

AMcK · Posted: Sat Aug 27, 2005 9:23 am Post subject:

Many congratulations with your discovery.
I'm still tracing through the logic of your transcripts to see how it all works. I've been able to replicate some of what you show but it may be a little while before I'm able to replicate what you show in full.
I love the verities and veracities - I was looking for something like this and am very cross that you got there first.
Supercolouring and tabling seem to have much in common - as Nick70 has already pointed out. A true value for a colour is simply a shorthand for the assertion that the cells containg that colour take the value of the possible - the false value is the assertion that they do not take the value of the possible. I already compute the transitive closure of the implies[u,v] matrix which represents all of the implications. So adding verity and veracity scanning took just a few lines of additional code.

Your example

AMcK · Posted: Sun Aug 28, 2005 8:28 am Post subject:

MadOverlord · Posted: Sun Aug 28, 2005 12:27 pm Post subject:

AMcK · Posted: Sun Aug 28, 2005 11:22 pm Post subject:

I put some better logic transcript into the ultracolourer, including the new "shortest proof" logger. Sadly there only seems to be one proof for each deduction, so the proof never gets any shorter.

I also tried the suggested "unverity" and "unveracity" algorithm where any deductions common to at least two negative candidates in a cell or possibles in a house must be true. [Proof: since only one candidate can be true, at least one of any pair must be false and so any common implications must be from at least one correctly false assumption]. I got some hits for unverities but I'm still not convinced that this increases the power of the solver.

Here's part of Menneske 900610 again, starting from