Sudoku Programmers Forum Index

 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister   ProfileProfile   Log inLog in          Games  Calendar

Log in to check your private messagesLog in to check your private messages   

Table Solving
Goto page 1, 2  Next
 
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Solving sudoku
View previous topic :: View next topic  
Author Message
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Tue Jul 26, 2005 5:50 pm    Post subject: Table Solving Reply with quote

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:

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   . #   # | 1 3 6 . ##### . ##### | ##### . 1 3 9 . 1 3 6 |
|     # .       . #   # | 9     . #   # . #     |     # .       . 9     |
| ##### .       . ##### |       . ##### . ##### |     # .       .       |
| #     .       .     # |       . #   # .     # |     # .       .       |
| ##### .       .     # |       . ##### . ##### |     # .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6 7 .   #   . ##### | 3 6 7 . ##### . 3 7 9 | 3 8 9 . #   # . 3 6 8 |
|       .   #   . #     | 9     .     # .       |       . #   # . 9     |
|       .   #   . ##### |       . ##### .       |       . ##### .       |
|       .   #   .     # |       . #     .       |       .     # .       |
|       .   #   . ##### |       . ##### .       |       .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6 7 . ##### . ##### | 1 3 6 . 1 6   . #   # | ##### . ##### . 1 3 6 |
|       . #   # . #   # | 7     .       . #   # |     # . #     .       |
|       . ##### . ##### |       .       . ##### | ##### . ##### .       |
|       .     # . #   # |       .       .     # | #     .     # .       |
|       .     # . ##### |       .       .     # | ##### . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4   . ##### | 3 4 5 . 4 5 9 . ##### |   #   . 3 9   . ##### |
| #   # .       .     # | 9     .       . #     |   #   .       .     # |
| ##### .       . ##### |       .       . ##### |   #   .       .     # |
| #   # .       . #     |       .       . #   # |   #   .       .     # |
| ##### .       . ##### |       .       . ##### |   #   .       .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4 6 . 1 3 6 | 1 3 4 . ##### . 3 8   | ##### . 6 8   . ##### |
| #   # .       .       | 8     .     # .       | #     .       .     # |
| ##### .       .       |       .     # .       | ##### .       . ##### |
|     # .       .       |       .     # .       |     # .       . #     |
|     # .       .       |       .     # .       | ##### .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . 1 3 6 | ##### . 1 9   . 3 8 9 | 3 9   . 6 8   . #   # |
| #     .     # .       |     # .       .       |       .       . #   # |
| ##### .     # .       | ##### .       .       |       .       . ##### |
|     # .     # .       | #     .       .       |       .       .     # |
| ##### .     # .       | ##### .       .       |       .       .     # |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 3 6   . ##### . ##### | 5 6 8 . 5 6   .   #   | #   # . ##### . 3 5 8 |
|       .     # . #   # |       .       .   #   | #   # .     # .       |
|       . ##### . ##### |       .       .   #   | ##### .     # .       |
|       . #     .     # |       .       .   #   |     # .     # .       |
|       . ##### .     # |       .       .   #   |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 4   . ##### . 3 6   | 4 6 7 . 4 6 9 . 7 8 9 | 3 8 9 . ##### . 1 3 8 |
|       . #     .       | 8 9   .       .       |       .     # . 9     |
|       . ##### .       |       .       .       |       . ##### .       |
|       .     # .       |       .       .       |       . #     .       |
|       . ##### .       |       .       .       |       . ##### .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 4   . ##### . ##### | 4 5 9 . ##### . ##### | ##### . 1 9   . 1 5 9 |
|       . #   # .     # |       .     # .     # | #     .       .       |
|       . ##### .     # |       .  #### . ##### | ##### .       .       |
|       . #   # .     # |       .     # . #     | #   # .       .       |
|       . ##### .     # |       . ##### . ##### | ##### .       .       |
+-----------------------+-----------------------+-----------------------+


Now consider the first unsolved square, R1C2=<36>. We can make 4 assertions about this square, R1C2=3, R1C2=6, R1C2<>3 and R1C2<>6. For each assertion, we can easily write down the implications of the assertion; the direct forces and pins generated in R1, C2 and B1 from the assertion, as well as the possibility reductions caused by the forces and pins:

Assertion R1C2 = 3 implies:
R4C2 = 4 (column force by R1C2 = 3)
R5C2 = 6 (column pin by R1C2 = 3)
R1C4 <> 3 (indirect implication of R1C2 = 3)
R1C8 <> 3 (indirect implication of R1C2 = 3)
R1C9 <> 3 (indirect implication of R1C2 = 3)
R2C1 <> 3 (indirect implication of R1C2 = 3)
R3C1 <> 3 (indirect implication of R1C2 = 3)
R4C4 <> 4 (indirect implication of R1C2 = 3) (for example, this is caused by R4C2 = 4)
R4C5 <> 4 (indirect implication of R1C2 = 3)
R5C3 <> 6 (indirect implication of R1C2 = 3)
R5C8 <> 6 (indirect implication of R1C2 = 3)
R6C3 <> 6 (indirect implication of R1C2 = 3)

Assertion R1C2 = 6 implies:
R1C4 <> 6 (indirect implication of R1C2 = 6)
R1C9 <> 6 (indirect implication of R1C2 = 6)
R2C1 <> 6 (indirect implication of R1C2 = 6)
R3C1 <> 6 (indirect implication of R1C2 = 6)
R5C2 <> 6 (indirect implication of R1C2 = 6)

Assertion R1C2 <> 3 implies:
R1C2 = 6 (force by R1C2 <> 3)
R1C4 <> 6 (indirect implication of R1C2 <> 3)
R1C9 <> 6 (indirect implication of R1C2 <> 3)
R2C1 <> 6 (indirect implication of R1C2 <> 3)
R3C1 <> 6 (indirect implication of R1C2 <> 3)
R5C2 <> 6 (indirect implication of R1C2 <> 3)

Assertion R1C2 <> 6 implies:
R1C2 = 3 (force by R1C2 <> 6)
R4C2 = 4 (column force by R1C2 <> 6)
R5C2 = 6 (column pin by R1C2 <> 6)
R1C4 <> 3 (indirect implication of R1C2 <> 6)
R1C8 <> 3 (indirect implication of R1C2 <> 6)
R1C9 <> 3 (indirect implication of R1C2 <> 6)
R2C1 <> 3 (indirect implication of R1C2 <> 6)
R3C1 <> 3 (indirect implication of R1C2 <> 6)
R4C4 <> 4 (indirect implication of R1C2 <> 6)
R4C5 <> 4 (indirect implication of R1C2 <> 6)
R5C3 <> 6 (indirect implication of R1C2 <> 6)
R5C8 <> 6 (indirect implication of R1C2 <> 6)
R6C3 <> 6 (indirect implication of R1C2 <> 6)

I currently don't go farther than this (though that is a topic for discussion). I'm just writing down the "obvious" implications of a choice.

In practice, if doing with paper and pencil, you'd just write them down in a line like this:

Assertion R1C2 = 3 implies: R4C2=4, R5C2=6, R1C4<>3, R1C8<>3, R1C9<>3, R2C1<>3, R3C1<>3, R4C4<>4, R4C5<>4, R5C3<>6, R5C8<>6, R6C3<>6

Assertion R1C2 <> 3 implies: R1C2=6, R1C4<>6, R1C9<>6, R2C1<>6, R3C1<>6, R5C2<>6

Assertion R1C2 = 6 implies: R1C4<>6, R1C9<>6, R2C1<>6, R3C1<>6, R5C2<>6

Assertion R1C2 <> 6 implies: R1C2=3, R4C2=4, R5C2=6, R1C4<>3, R1C8<>3, R1C9<>3, R2C1<>3, R3C1<>3, R4C4<>4, R4C5<>4, R5C3<>6, R5C8<>6, R6C3<>6

By itself, this usually doesn't tell us much, though we occasionally get an assertion that is immediately inconsistent, for example:

Invalid assertion R5C3 = 3 implies:
R5C4 = 1 (row pin by R5C3 = 3)
R5C6 = 8 (row force by R5C3 = 3)
R6C3 = 1 (column pin by R5C3 = 3)
R8C3 = 6 (column force by R5C3 = 3)
R4C2 = 4 (block force by R5C3 = 3)
R5C8 = 6 (row force by R5C3 = 3)
R5C2 = 6 (block force by R5C3 = 3)
R5C8 = ? (inconsistent; R5C3 = 3 cannot be true)
R1C2 <> 6 (indirect implication of R5C3 = 3)
R1C4 <> 1 (indirect implication of R5C3 = 3)
R3C4 <> 1 (indirect implication of R5C3 = 3)
R4C4 <> 4 (indirect implication of R5C3 = 3)
R4C5 <> 4 (indirect implication of R5C3 = 3)
R6C5 <> 1 (indirect implication of R5C3 = 3)
R6C6 <> 8 (indirect implication of R5C3 = 3)
R6C8 <> 6 (indirect implication of R5C3 = 3)
R7C1 <> 6 (indirect implication of R5C3 = 3)
R8C4 <> 6 (indirect implication of R5C3 = 3)
R8C5 <> 6 (indirect implication of R5C3 = 3)
R8C6 <> 8 (indirect implication of R5C3 = 3)

In this case, R5C3 = 3 forces both R5C8 and R5C2 to 3, which is inconsistent.

The real power of the method comes when you expand the implications. Looking back at our original, square, the first implication was:

Assertion R1C2 = 3 implies:
R4C2 = 4 (column force by R1C2 = 3)

If we table the assertion R4C2=4, we can add its implications to those of R1C2=3. In the paper version, we'd add the implications to the table line for R1C2=3, and put a dot over the implication R4C2=2 to indicate we'd expanded it.

In my experiments with the technique, I'm doing all the implications for all the squares, and expanding until I can't do anything more. In actual human execution, we'd be a lot more selective, and heuristics to decide what squares to attack is a subject for research. But note that one very nice feature is that once you figure out the implications of an assertion, they are true forever! You can revisit them if you get stuck later, even after
solving some squares. The caveats to this are that some of the implications may be rendered irrelevant, and the solving of squares may add extra implications to assertions because they permit additional forces and pins. However, by the time this becomes a significant issue, the puzzle will likely be reduced to a point where it becomes sensible to redo the tables (it seems to get it to a lot of interlinked locked sets).

Examining assertions for inconsistencies: I've found several ways to extract information from the tables. The simplest of course is when an assertion leads to a direct contradiction, containing implications like R1C2=3 and R1C2=6. Next comes exclusion, where two cells in the same R, C or B have the same value. Another one is extinction, where you get negative implications that exclude all possible values (if R1C2=<36>, then if there are implications R1C2 <> 3 and R1C2 <> 6, then the containing assertion must be false. And of course, assertions can ripple; if an assertion is invalid, then any assertion that contains it is also invalid.

But the most interesting one for me is what I call "eternal verities". If you look at the positive (=) assertions for a square, sometimes you can find implications that are true for all the possibilities. In other words, no matter what value the square has, something else HAS to be true. For example, in this puzzle, no matter what value R8C9 has, the following implications are always true:

R8C1 = 1
R9C1 <> 1
R9C1 = 4
R8C9 <> 1
R9C4 <> 4
R8C1 <> 4

In any case, if you expand everything in the puzzle, you find out that:

The following squares can be solved:
R4C4 = 5
R7C5 = 5
R8C1 = 1
R9C1 = 4
R9C8 = 1
R9C9 = 5

The following squares can have possibilities eliminated:
R1C4: remove <6> from <1369> leaving <139>.
R1C8: remove <1> from <139> leaving <39>.
R1C9: remove <3> from <1369> leaving <169>.
R3C1: remove <6> from <367> leaving <37>.
R3C4: remove <6> from <1367> leaving <137>.
R4C5: remove <5> from <459> leaving <49>.
R5C3: remove <3> from <136> leaving <16>.
R5C4: remove <8> from <1348> leaving <134>.
R7C4: remove <5> from <568> leaving <68>.
R7C9: remove <5> from <358> leaving <38>.
R8C5: remove <9> from <469> leaving <46>.
R8C6: remove <8> from <789> leaving <79>.
R8C9: remove <1> from <1389> leaving <389>.
R9C4: remove <45> from <459> leaving <9>.

Puzzle after tabling:

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   . #   # | 1 3   . ##### . ##### | ##### . 3 9   . 1 6 9 |
|     # .       . #   # |       . #   # . #     |     # .       .       |
| ##### .       . ##### |       . ##### . ##### |     # .       .       |
| #     .       .     # |       . #   # .     # |     # .       .       |
| ##### .       .     # |       . ##### . ##### |     # .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6 7 .   #   . ##### | 3 6 7 . ##### . 3 7 9 | 3 8 9 . #   # . 3 6 8 |
|       .   #   . #     |       .     # .       |       . #   # . 9     |
|       .   #   . ##### |       . ##### .       |       . ##### .       |
|       .   #   .     # |       . #     .       |       .     # .       |
|       .   #   . ##### |       . ##### .       |       .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 7   . ##### . ##### | 1 3 7 . 1 6   . #   # | ##### . ##### . 1 3 6 |
|       . #   # . #   # |       .       . #   # |     # . #     .       |
|       . ##### . ##### |       .       . ##### | ##### . ##### .       |
|       .     # . #   # |       .       .     # | #     .     # .       |
|       .     # . ##### |       .       .     # | ##### . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4   . ##### | ##### . 4 9   . ##### |   #   . 3 9   . ##### |
| #   # .       .     # | #     .       . #     |   #   .       .     # |
| ##### .       . ##### | ##### .       . ##### |   #   .       .     # |
| #   # .       . #     |     # .       . #   # |   #   .       .     # |
| ##### .       . ##### | ##### .       . ##### |   #   .       .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4 6 . 1 6   | 1 3 4 . ##### . 3 8   | ##### . 6 8   . ##### |
| #   # .       .       |       .     # .       | #     .       .     # |
| ##### .       .       |       .     # .       | ##### .       . ##### |
|     # .       .       |       .     # .       |     # .       . #     |
|     # .       .       |       .     # .       | ##### .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . 1 3 6 | ##### . 1 9   . 3 8 9 | 3 9   . 6 8   . #   # |
| #     .     # .       |     # .       .       |       .       . #   # |
| ##### .     # .       | ##### .       .       |       .       . ##### |
|     # .     # .       | #     .       .       |       .       .     # |
| ##### .     # .       | ##### .       .       |       .       .     # |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 3 6   . ##### . ##### | 6 8   . ##### .   #   | #   # . ##### . 3 8   |
|       .     # . #   # |       . #     .   #   | #   # .     # .       |
|       . ##### . ##### |       . ##### .   #   | ##### .     # .       |
|       . #     .     # |       .     # .   #   |     # .     # .       |
|       . ##### .     # |       . ##### .   #   |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
|   #   . ##### . 3 6   | 4 6 7 . 4 6   . 7     | 3 8 9 . ##### . 3 8 9 |
|   #   . #     .       | 8     .       .       |       .     # .       |
|   #   . ##### .       |       .       .       |       . ##### .       |
|   #   .     # .       |       .       .       |       . #     .       |
|   #   . ##### .       |       .       .       |       . ##### .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | ##### . ##### . ##### | ##### .   #   . ##### |
| #   # . #   # .     # | #   # .     # .     # | #     .   #   . #     |
| ##### . ##### .     # | ##### .  #### . ##### | ##### .   #   . ##### |
|     # . #   # .     # |     # .     # . #     | #   # .   #   .     # |
|     # . ##### .     # |     # . ##### . ##### | ##### .   #   . ##### |
+-----------------------+-----------------------+-----------------------+


And you can then make the following simple deductions:

* R8C6 must be <7>.

* R2C6 is the only square in block 2 that can be a <9>. It is thus pinned to that value.

* 2 squares in block 5 form a simple locked pair. R5C6 and R6C6 share possibilities <38>. Thus, these possibilities can be removed from the rest of the block.

R5C4 - removing <3> from <134> leaving <14>.

Which gets us to:

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   . #   # | 1 3   . ##### . ##### | ##### . 3 9   . 1 6 9 |
|     # .       . #   # |       . #   # . #     |     # .       .       |
| ##### .       . ##### |       . ##### . ##### |     # .       .       |
| #     .       .     # |       . #   # .     # |     # .       .       |
| ##### .       .     # |       . ##### . ##### |     # .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6 7 .   #   . ##### | 3 6 7 . ##### . ##### | 3 8   . #   # . 3 6 8 |
|       .   #   . #     |       .     # . #   # |       . #   # .       |
|       .   #   . ##### |       . ##### . ##### |       . ##### .       |
|       .   #   .     # |       . #     .     # |       .     # .       |
|       .   #   . ##### |       . ##### .     # |       .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 7   . ##### . ##### | 1 3 7 . 1 6   . #   # | ##### . ##### . 1 3 6 |
|       . #   # . #   # |       .       . #   # |     # . #     .       |
|       . ##### . ##### |       .       . ##### | ##### . ##### .       |
|       .     # . #   # |       .       .     # | #     .     # .       |
|       .     # . ##### |       .       .     # | ##### . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4   . ##### | ##### . 4 9   . ##### |   #   . 3 9   . ##### |
| #   # .       .     # | #     .       . #     |   #   .       .     # |
| ##### .       . ##### | ##### .       . ##### |   #   .       .     # |
| #   # .       . #     |     # .       . #   # |   #   .       .     # |
| ##### .       . ##### | ##### .       . ##### |   #   .       .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 3 4 6 . 1 6   | 1 4   . ##### . 3 8   | ##### . 6 8   . ##### |
| #   # .       .       |       .     # .       | #     .       .     # |
| ##### .       .       |       .     # .       | ##### .       . ##### |
|     # .       .       |       .     # .       |     # .       . #     |
|     # .       .       |       .     # .       | ##### .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . 1 3 6 | ##### . 1 9   . 3 8   | 3 9   . 6 8   . #   # |
| #     .     # .       |     # .       .       |       .       . #   # |
| ##### .     # .       | ##### .       .       |       .       . ##### |
|     # .     # .       | #     .       .       |       .       .     # |
| ##### .     # .       | ##### .       .       |       .       .     # |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 3 6   . ##### . ##### | 6 8   . ##### .   #   | #   # . ##### . 3 8   |
|       .     # . #   # |       . #     .   #   | #   # .     # .       |
|       . ##### . ##### |       . ##### .   #   | ##### .     # .       |
|       . #     .     # |       .     # .   #   |     # .     # .       |
|       . ##### .     # |       . ##### .   #   |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
|   #   . ##### . 3 6   | 4 6 8 . 4 6   . ##### | 3 8 9 . ##### . 3 8 9 |
|   #   . #     .       |       .       .     # |       .     # .       |
|   #   . ##### .       |       .       .     # |       . ##### .       |
|   #   .     # .       |       .       .     # |       . #     .       |
|   #   . ##### .       |       .       .     # |       . ##### .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | ##### . ##### . ##### | ##### .   #   . ##### |
| #   # . #   # .     # | #   # .     # .     # | #     .   #   . #     |
| ##### . ##### .     # | ##### .  #### . ##### | ##### .   #   . ##### |
|     # . #   # .     # |     # .     # . #     | #   # .   #   .     # |
|     # . ##### .     # |     # . ##### . ##### | ##### .   #   . ##### |
+-----------------------+-----------------------+-----------------------+


Now, reviewing the tables (no added computation, just checking in light of the additional constraints we found, gives us this:

The following squares can be solved:
R3C5 = 6
R5C3 = 1
R6C5 = 1

The following squares can have possibilities eliminated:
R2C4: remove <6> from <367> leaving <37>.
R3C9: remove <6> from <136> leaving <13>.
R5C4: remove <1> from <14> leaving <4>.
R6C3: remove <1> from <136> leaving <36>.
R8C5: remove <6> from <46> leaving <4>.

Which leads to the following basic deductions:

* R4C5 must be <9>.

From this deduction, the following moves are immediately forced:

R4C8 must be <3>.
R4C2 must be <4>.
R1C8 must be <9>.
R6C7 must be <9>.

* R8C9 is the only square in row 8 that can be a <9>. It is thus pinned to that value.

At this point, re-examining the tables doesn't get us anything more, but note how stuff has reduced to a lot of locked sets

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   . #   # | 1 3   . ##### . ##### | ##### . ##### . 1 6   |
|     # .       . #   # |       . #   # . #     |     # . #   # .       |
| ##### .       . ##### |       . ##### . ##### |     # . ##### .       |
| #     .       .     # |       . #   # .     # |     # .     # .       |
| ##### .       .     # |       . ##### . ##### |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6 7 .   #   . ##### | 3 7   . ##### . ##### | 3 8   . #   # . 3 6 8 |
|       .   #   . #     |       .     # . #   # |       . #   # .       |
|       .   #   . ##### |       . ##### . ##### |       . ##### .       |
|       .   #   .     # |       . #     .     # |       .     # .       |
|       .   #   . ##### |       . ##### .     # |       .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 7   . ##### . ##### | 1 3 7 . ##### . #   # | ##### . ##### . 1 3   |
|       . #   # . #   # |       . #     . #   # |     # . #     .       |
|       . ##### . ##### |       . ##### . ##### | ##### . ##### .       |
|       .     # . #   # |       . #   # .     # | #     .     # .       |
|       .     # . ##### |       . ##### .     # | ##### . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . #   # . ##### | ##### . ##### . ##### |   #   . ##### . ##### |
| #   # . #   # .     # | #     . #   # . #     |   #   .     # .     # |
| ##### . ##### . ##### | ##### . ##### . ##### |   #   .  #### .     # |
| #   # .     # . #     |     # .     # . #   # |   #   .     # .     # |
| ##### .     # . ##### | ##### .     # . ##### |   #   . ##### .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   .   #   | #   # . ##### . 3 8   | ##### . 6 8   . ##### |
| #   # .       .   #   | #   # .     # .       | #     .       .     # |
| ##### .       .   #   | ##### .     # .       | ##### .       . ##### |
|     # .       .   #   |     # .     # .       |     # .       . #     |
|     # .       .   #   |     # .     # .       | ##### .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . 3 6   | ##### .   #   . 3 8   | ##### . 6 8   . #   # |
| #     .     # .       |     # .   #   .       | #   # .       . #   # |
| ##### .     # .       | ##### .   #   .       | ##### .       . ##### |
|     # .     # .       | #     .   #   .       |     # .       .     # |
| ##### .     # .       | ##### .   #   .       |     # .       .     # |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 3 6   . ##### . ##### | 6 8   . ##### .   #   | #   # . ##### . 3 8   |
|       .     # . #   # |       . #     .   #   | #   # .     # .       |
|       . ##### . ##### |       . ##### .   #   | ##### .     # .       |
|       . #     .     # |       .     # .   #   |     # .     # .       |
|       . ##### .     # |       . ##### .   #   |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
|   #   . ##### . 3 6   | 6 8   . #   # . ##### | 3 8   . ##### . ##### |
|   #   . #     .       |       . #   # .     # |       .     # . #   # |
|   #   . ##### .       |       . ##### .     # |       . ##### . ##### |
|   #   .     # .       |       .     # .     # |       . #     .     # |
|   #   . ##### .       |       .     # .     # |       . ##### .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | ##### . ##### . ##### | ##### .   #   . ##### |
| #   # . #   # .     # | #   # .     # .     # | #     .   #   . #     |
| ##### . ##### .     # | ##### .  #### . ##### | ##### .   #   . ##### |
|     # . #   # .     # |     # .     # . #     | #   # .   #   .     # |
|     # . ##### .     # |     # . ##### . ##### | ##### .   #   . ##### |
+-----------------------+-----------------------+-----------------------+


But clearing the tables and starting over (with fewer squares, and fewer options) does give us an improvement. The first pass (without expansion), tells us:

The following squares can have possibilities eliminated:
R3C1: remove <3> from <37> leaving <7>.

Which immediately leads to:

* R2C4 is the only square in row 2 that can be a <7>. It is thus pinned to that value.

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   . #   # | 1 3   . ##### . ##### | ##### . ##### . 1 6   |
|     # .       . #   # |       . #   # . #     |     # . #   # .       |
| ##### .       . ##### |       . ##### . ##### |     # . ##### .       |
| #     .       .     # |       . #   # .     # |     # .     # .       |
| ##### .       .     # |       . ##### . ##### |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 3 6   .   #   . ##### | ##### . ##### . ##### | 3 8   . #   # . 3 6 8 |
|       .   #   . #     |     # .     # . #   # |       . #   # .       |
|       .   #   . ##### |     # . ##### . ##### |       . ##### .       |
|       .   #   .     # |     # . #     .     # |       .     # .       |
|       .   #   . ##### |     # . ##### .     # |       .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . ##### | 1 3   . ##### . #   # | ##### . ##### . 1 3   |
|     # . #   # . #   # |       . #     . #   # |     # . #     .       |
|     # . ##### . ##### |       . ##### . ##### | ##### . ##### .       |
|     # .     # . #   # |       . #   # .     # | #     .     # .       |
|     # .     # . ##### |       . ##### .     # | ##### . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . #   # . ##### | ##### . ##### . ##### |   #   . ##### . ##### |
| #   # . #   # .     # | #     . #   # . #     |   #   .     # .     # |
| ##### . ##### . ##### | ##### . ##### . ##### |   #   .  #### .     # |
| #   # .     # . #     |     # .     # . #   # |   #   .     # .     # |
| ##### .     # . ##### | ##### .     # . ##### |   #   . ##### .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 3 6   .   #   | #   # . ##### . 3 8   | ##### . 6 8   . ##### |
| #   # .       .   #   | #   # .     # .       | #     .       .     # |
| ##### .       .   #   | ##### .     # .       | ##### .       . ##### |
|     # .       .   #   |     # .     # .       |     # .       . #     |
|     # .       .   #   |     # .     # .       | ##### .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . ##### . 3 6   | ##### .   #   . 3 8   | ##### . 6 8   . #   # |
| #     .     # .       |     # .   #   .       | #   # .       . #   # |
| ##### .     # .       | ##### .   #   .       | ##### .       . ##### |
|     # .     # .       | #     .   #   .       |     # .       .     # |
| ##### .     # .       | ##### .   #   .       |     # .       .     # |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 3 6   . ##### . ##### | 6 8   . ##### .   #   | #   # . ##### . 3 8   |
|       .     # . #   # |       . #     .   #   | #   # .     # .       |
|       . ##### . ##### |       . ##### .   #   | ##### .     # .       |
|       . #     .     # |       .     # .   #   |     # .     # .       |
|       . ##### .     # |       . ##### .   #   |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
|   #   . ##### . 3 6   | 6 8   . #   # . ##### | 3 8   . ##### . ##### |
|   #   . #     .       |       . #   # .     # |       .     # . #   # |
|   #   . ##### .       |       . ##### .     # |       . ##### . ##### |
|   #   .     # .       |       .     # .     # |       . #     .     # |
|   #   . ##### .       |       .     # .     # |       . ##### .     # |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | ##### . ##### . ##### | ##### .   #   . ##### |
| #   # . #   # .     # | #   # .     # .     # | #     .   #   . #     |
| ##### . ##### .     # | ##### .  #### . ##### | ##### .   #   . ##### |
|     # . #   # .     # |     # .     # . #     | #   # .   #   .     # |
|     # . ##### .     # |     # . ##### . ##### | ##### .   #   . ##### |
+-----------------------+-----------------------+-----------------------+


Then expanding the assertions gives us:

The following squares can have possibilities eliminated:
R1C2: remove <6> from <36> leaving <3>.
R1C4: remove <3> from <13> leaving <1>.
R1C9: remove <1> from <16> leaving <6>.
R2C1: remove <3> from <36> leaving <6>.
R2C7: remove <3> from <38> leaving <8>.
R2C9: remove <68> from <368> leaving <3>.
R3C4: remove <1> from <13> leaving <3>.
R3C9: remove <3> from <13> leaving <1>.
R5C2: remove <3> from <36> leaving <6>.
R5C6: remove <8> from <38> leaving <3>.
R5C8: remove <6> from <68> leaving <8>.
R6C3: remove <6> from <36> leaving <3>.
R6C6: remove <3> from <38> leaving <8>.
R6C8: remove <8> from <68> leaving <6>.
R7C1: remove <6> from <36> leaving <3>.
R7C4: remove <8> from <68> leaving <6>.
R7C9: remove <3> from <38> leaving <8>.
R8C3: remove <3> from <36> leaving <6>.
R8C4: remove <6> from <68> leaving <8>.
R8C7: remove <8> from <38> leaving <3>.

which solves the puzzle!

Code:

+-------+-------+-------+
| 2 3 4 | 1 8 5 | 7 9 6 |
| 6 1 5 | 7 2 9 | 8 4 3 |
| 7 9 8 | 3 6 4 | 2 5 1 |
+-------+-------+-------+
| 8 4 2 | 5 9 6 | 1 3 7 |
| 9 6 1 | 4 7 3 | 5 8 2 |
| 5 7 3 | 2 1 8 | 9 6 4 |
+-------+-------+-------+
| 3 2 9 | 6 5 1 | 4 7 8 |
| 1 5 6 | 8 4 7 | 3 2 9 |
| 4 8 7 | 9 3 2 | 6 1 5 |
+-------+-------+-------+


All is not wonderful, however. I do have an example puzzle that defeats the tabling algorithm. Doug Bowman found it, it's a real ballbreaker; it laughs at the advanced algorithms.

Code:

+-------+-------+-------+
| . . . | . 7 . | 9 4 . |
| . 7 . | . 9 . | . . 5 |
| 3 . . | . . 5 | . 7 . |
+-------+-------+-------+
| . 8 7 | 4 . . | 1 . . |
| 4 6 3 | . 8 . | . . . |
| . . . | . . 7 | . 8 . |
+-------+-------+-------+
| 8 . . | 7 . . | . . . |
| 7 . . | . . . | . 2 8 |
| . 5 . | 2 6 8 | . . . |
+-------+-------+-------+


After basic solves, you get:

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2   . 1 2 5 | 1 3 6 . ##### . 1 2 3 | ##### . #   # . 1 2 3 |
| 6     .       . 8     | 8     .     # . 6     | #   # . #   # . 6     |
|       .       .       |       .     # .       | ##### . ##### .       |
|       .       .       |       .     # .       |     # .     # .       |
|       .       .       |       .     # .       |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 6 . ##### . 1 2 4 | 1 3 6 . ##### . 1 2 3 | 2 3 6 . 1 3 6 . ##### |
|       .     # . 8     | 8     . #   # . 4 6   | 8     .       . #     |
|       .     # .       |       . ##### .       |       .       . ##### |
|       .     # .       |       .     # .       |       .       .     # |
|       .     # .       |       .     # .       |       .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 2 4 . 1 2 4 | 1 6 8 . 1 2 4 . ##### | 2 6 8 . ##### . 1 2 6 |
|     # . 9     . 8 9   |       .       . #     |       .     # .       |
|  #### .       .       |       .       . ##### |       .     # .       |
|     # .       .       |       .       .     # |       .     # .       |
| ##### .       .       |       .       . ##### |       .     # .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 2 5 9 . ##### . ##### | #   # . 2 3 5 . 2 3 6 |   #   . 3 5 6 . 2 3 6 |
|       . #   # .     # | #   # .       . 9     |   #   . 9     . 9     |
|       . ##### .     # | ##### .       .       |   #   .       .       |
|       . #   # .     # |     # .       .       |   #   .       .       |
|       . ##### .     # |     # .       .       |   #   .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | 1 5 9 . ##### . 1 2 9 | 2 5 7 . 5 9   . 2 7 9 |
| #   # . #     .     # |       . #   # .       |       .       .       |
| ##### . ##### .  #### |       . ##### .       |       .       .       |
|     # . #   # .     # |       . #   # .       |       .       .       |
|     # . ##### . ##### |       . ##### .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2 9 . 1 2 5 | 3 5 6 . 2 3 5 . ##### | 2 3 4 . ##### . 2 3 4 |
| 9     .       . 9     | 9     .       .     # | 5 6   . #   # . 6 9   |
|       .       .       |       .       .     # |       . ##### .       |
|       .       .       |       .       .     # |       . #   # .       |
|       .       .       |       .       .     # |       . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 1 2 3 . 1 2 4 | ##### . 1 3 4 . 1 3 4 | 4 5 6 . 1 5 6 . 1 4 6 |
| #   # . 4 9   . 6 9   |     # . 5     . 9     |       . 9     . 9     |
| ##### .       .       |     # .       .       |       .       .       |
| #   # .       .       |     # .       .       |       .       .       |
| ##### .       .       |     # .       .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 3 4 . 1 4 6 | 1 3 5 . 1 3 4 . 1 3 4 | 4 5 6 . ##### . ##### |
|     # . 9     . 9     | 9     . 5     . 9     |       .     # . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|     # .       .       |       .       .       |       . #     . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 9   . ##### . 1 4 9 | ##### . ##### . ##### | 3 4 7 . 1 3 9 . 1 3 4 |
|       . #     .       |     # . #     . #   # |       .       . 7 9   |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
|       .     # .       | #     . #   # . #   # |       .       .       |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
+-----------------------+-----------------------+-----------------------+


Tabling gives:

The following squares can have possibilities eliminated:
R3C3: remove <2> from <12489> leaving <1489>.
R7C3: remove <9> from <12469> leaving <1246>.
R8C3: remove <9> from <1469> leaving <146>.

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2   . 1 2 5 | 1 3 6 . ##### . 1 2 3 | ##### . #   # . 1 2 3 |
| 6     .       . 8     | 8     .     # . 6     | #   # . #   # . 6     |
|       .       .       |       .     # .       | ##### . ##### .       |
|       .       .       |       .     # .       |     # .     # .       |
|       .       .       |       .     # .       |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 6 . ##### . 1 2 4 | 1 3 6 . ##### . 1 2 3 | 2 3 6 . 1 3 6 . ##### |
|       .     # . 8     | 8     . #   # . 4 6   | 8     .       . #     |
|       .     # .       |       . ##### .       |       .       . ##### |
|       .     # .       |       .     # .       |       .       .     # |
|       .     # .       |       .     # .       |       .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 2 4 . 1 4 8 | 1 6 8 . 1 2 4 . ##### | 2 6 8 . ##### . 1 2 6 |
|     # . 9     . 9     |       .       . #     |       .     # .       |
|  #### .       .       |       .       . ##### |       .     # .       |
|     # .       .       |       .       .     # |       .     # .       |
| ##### .       .       |       .       . ##### |       .     # .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 2 5 9 . ##### . ##### | #   # . 2 3 5 . 2 3 6 |   #   . 3 5 6 . 2 3 6 |
|       . #   # .     # | #   # .       . 9     |   #   . 9     . 9     |
|       . ##### .     # | ##### .       .       |   #   .       .       |
|       . #   # .     # |     # .       .       |   #   .       .       |
|       . ##### .     # |     # .       .       |   #   .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | 1 5 9 . ##### . 1 2 9 | 2 5 7 . 5 9   . 2 7 9 |
| #   # . #     .     # |       . #   # .       |       .       .       |
| ##### . ##### .  #### |       . ##### .       |       .       .       |
|     # . #   # .     # |       . #   # .       |       .       .       |
|     # . ##### . ##### |       . ##### .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2 9 . 1 2 5 | 3 5 6 . 2 3 5 . ##### | 2 3 4 . ##### . 2 3 4 |
| 9     .       . 9     | 9     .       .     # | 5 6   . #   # . 6 9   |
|       .       .       |       .       .     # |       . ##### .       |
|       .       .       |       .       .     # |       . #   # .       |
|       .       .       |       .       .     # |       . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 1 2 3 . 1 2 4 | ##### . 1 3 4 . 1 3 4 | 4 5 6 . 1 5 6 . 1 4 6 |
| #   # . 4 9   . 6     |     # . 5     . 9     |       . 9     . 9     |
| ##### .       .       |     # .       .       |       .       .       |
| #   # .       .       |     # .       .       |       .       .       |
| ##### .       .       |     # .       .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 3 4 . 1 4 6 | 1 3 5 . 1 3 4 . 1 3 4 | 4 5 6 . ##### . ##### |
|     # . 9     .       | 9     . 5     . 9     |       .     # . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|     # .       .       |       .       .       |       . #     . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 9   . ##### . 1 4 9 | ##### . ##### . ##### | 3 4 7 . 1 3 9 . 1 3 4 |
|       . #     .       |     # . #     . #   # |       .       . 7 9   |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
|       .     # .       | #     . #   # . #   # |       .       .       |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
+-----------------------+-----------------------+-----------------------+

Basic deductive work gives no progress.

Rechecking the tables gives no progress.

Redoing and re-expanding the tables gives no joy.

Throwing the deductive book at the puzzle (fishy cycles, nishio, forcing chains and bowman bingo) generates some improvements, through incredibly long bowman bingos (41 cycles in one case!).

We get to here:

Code:

+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2   . 1 5 8 | 1 3 6 . ##### . 1 2 3 | ##### . #   # . 1 2 3 |
| 6     .       .       | 8     .     # . 6     | #   # . #   # . 6     |
|       .       .       |       .     # .       | ##### . ##### .       |
|       .       .       |       .     # .       |     # .     # .       |
|       .       .       |       .     # .       |     # .     # .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 6 . ##### . 1 2 4 | 1 3 6 . ##### . 2 3 4 | 2 3 6 . 1 3 6 . ##### |
|       .     # . 8     | 8     . #   # . 6     | 8     .       . #     |
|       .     # .       |       . ##### .       |       .       . ##### |
|       .     # .       |       .     # .       |       .       .     # |
|       .     # .       |       .     # .       |       .       . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 4 9 . 1 4 8 | 1 6 8 . 1 2 4 . ##### | 2 6 8 . ##### . 1 2 6 |
|     # .       . 9     |       .       . #     |       .     # .       |
|  #### .       .       |       .       . ##### |       .     # .       |
|     # .       .       |       .       .     # |       .     # .       |
| ##### .       .       |       .       . ##### |       .     # .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| 2 5 9 . ##### . ##### | #   # . 2 3 5 . 2 3 6 |   #   . 3 5 6 . 2 3 6 |
|       . #   # .     # | #   # .       . 9     |   #   . 9     . 9     |
|       . ##### .     # | ##### .       .       |   #   .       .       |
|       . #   # .     # |     # .       .       |   #   .       .       |
|       . ##### .     # |     # .       .       |   #   .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| #   # . ##### . ##### | 1 5 9 . ##### . 1 2 9 | 2 5 7 . 5 9   . 2 7 9 |
| #   # . #     .     # |       . #   # .       |       .       .       |
| ##### . ##### .  #### |       . ##### .       |       .       .       |
|     # . #   # .     # |       . #   # .       |       .       .       |
|     # . ##### . ##### |       . ##### .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 2 5 . 1 2 9 . 1 2 5 | 3 5 6 . 2 3 5 . ##### | 2 3 4 . ##### . 2 3 4 |
| 9     .       . 9     | 9     .       .     # | 5 6   . #   # . 6     |
|       .       .       |       .       .     # |       . ##### .       |
|       .       .       |       .       .     # |       . #   # .       |
|       .       .       |       .       .     # |       . ##### .       |
+-----------------------+-----------------------+-----------------------+
|       .       .       |       .       .       |       .       .       |
| ##### . 1 2 3 . 1 2 4 | ##### . 1 3 4 . 1 3 4 | 4 5 6 . 1 5 6 . 1 4 6 |
| #   # . 4 9   . 6     |     # . 5     . 9     |       . 9     . 9     |
| ##### .       .       |     # .       .       |       .       .       |
| #   # .       .       |     # .       .       |       .       .       |
| ##### .       .       |     # .       .       |       .       .       |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| ##### . 1 3 4 . 1 4 6 | 1 3 5 . 1 3 4 . 1 3 4 | 4 5 6 . ##### . ##### |
|     # . 9     .       | 9     . 5     . 9     |       .     # . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|     # .       .       |       .       .       |       . #     . #   # |
|     # .       .       |       .       .       |       . ##### . ##### |
|.......................|.......................|.......................|
|       .       .       |       .       .       |       .       .       |
| 1 9   . ##### . 1 4 9 | ##### . ##### . ##### | 3 4 7 . 1 3 9 . 1 3 4 |
|       . #     .       |     # . #     . #   # |       .       . 7 9   |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
|       .     # .       | #     . #   # . #   # |       .       .       |
|       . ##### .       | ##### . ##### . ##### |       .       .       |
+-----------------------+-----------------------+-----------------------+


At which point, no joy. Oh well.

Possible discussion subjects:

* Heuristics for deciding what squares to attack in order to make practical progress on puzzles without tabling the whole thing.

* Additional "easy" implications that can be made (perhaps noting created locked sets?) that might crack complex puzzles.
Back to top
View user's profile Send private message Visit poster's website AIM Address
Nick70

Joined: 08 Jun 2005
Posts: 160
:

Items
PostPosted: Tue Jul 26, 2005 7:36 pm    Post subject: Reply with quote

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.


Last edited by Nick70 on Sat Jul 30, 2005 11:30 am; edited 1 time in total
Back to top
View user's profile Send private message
tilps

Joined: 19 Jun 2005
Posts: 44
:

Items
PostPosted: Wed Jul 27, 2005 11:06 pm    Post subject: Reply with quote

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.
Back to top
View user's profile Send private message
Doug

Joined: 28 May 2005
Posts: 42
:

Items
PostPosted: Thu Aug 04, 2005 12:25 am    Post subject: Reply with quote

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
Back to top
View user's profile Send private message Send e-mail
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Tue Aug 09, 2005 11:36 am    Post subject: Tables Improved - Now cracks the above puzzle Reply with quote

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.
Back to top
View user's profile Send private message Visit poster's website AIM Address
Nick70

Joined: 08 Jun 2005
Posts: 160
:

Items
PostPosted: Tue Aug 09, 2005 12:52 pm    Post subject: Re: Tables Improved - Now cracks the above puzzle Reply with quote

MadOverlord wrote:
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.

Right. This is a multiple forcing chain. The algorithm that finds double forcing chains can find these as well.

Don't forget the negative version of that, which always results in a double forcing chain: if there are N cells in a unit that can have value V, then the intersection of the <>V assertions for any two of these cells must be true.

MadOverlord wrote:
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.

Don't you mean the union of R1C1=2 and R1C1=3?
This is a special case of multiple forcing chain, however.

MadOverlord wrote:
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.

Right. THis is a special case of multiple forcing chain where all chains except one are identical starting from the second link.
Back to top
View user's profile Send private message
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Tue Aug 09, 2005 2:59 pm    Post subject: Re: Tables Improved - Now cracks the above puzzle Reply with quote

Nick70 wrote:
Right. This is a multiple forcing chain. The algorithm that finds double forcing chains can find these as well.

Don't forget the negative version of that, which always results in a double forcing chain: if there are N cells in a unit that can have value V, then the intersection of the <>V assertions for any two of these cells must be true.


I shall check to see if that is true. An interesting observation.

Nick70 wrote:
MadOverlord wrote:
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.

Don't you mean the union of R1C1=2 and R1C1=3?
This is a special case of multiple forcing chain, however.


AFAICT its the intersection. At that point, if R1C1<>1, then it must be 2 or 3; so anything that is true for BOTH R1C1=2 and R1C1=3 must be true for R1C1<>1. If you take the union, then consider there might be stuff in R1C1=2 or R1C1=3 that are also true for R1C1=1, which you don't want in R1C1<>1.

Hmmm... I am wondering if it might be possible to use the union, excluding stuff that is in R1C1=1. However, since R1C1=1 might get expanded later on, that would corrupt R1C1<>1...

I have a feeling that as R1C1=2 or 3 get expanded, they'll in turn expand R1C1<>1, so it'll work out
Back to top
View user's profile Send private message Visit poster's website AIM Address
Nick70

Joined: 08 Jun 2005
Posts: 160
:

Items
PostPosted: Tue Aug 09, 2005 4:46 pm    Post subject: Re: Tables Improved - Now cracks the above puzzle Reply with quote

MadOverlord wrote:
Nick70 wrote:
MadOverlord wrote:
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.

Don't you mean the union of R1C1=2 and R1C1=3?
AFAICT its the intersection.

Sorry you are right--I was reading it the other way around.
Back to top
View user's profile Send private message
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Wed Aug 10, 2005 6:27 pm    Post subject: Reply with quote

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.

Code:

+-------+-------+-------+
| . . . | . 7 . | 9 4 . |
| . 7 . | . 9 . | . . 5 |
| 3 . . | . . 5 | . 7 . |
+-------+-------+-------+
| . 8 7 | 4 . . | 1 . . |
| 4 6 3 | . 8 . | . . . |
| . . . | . . 7 | . 8 . |
+-------+-------+-------+
| 8 . . | 7 . . | . . . |
| 7 . . | . . . | . 2 8 |
| . 5 . | 2 6 8 | . . . |
+-------+-------+-------+

Deduction pass 1; 28 squares solved; 53 remaining.

* Intersection of row 5 with block 5. The value <1> can only appear in squares R5C4, R5C5 and R5C6 of row 5.  Thus, the non-intersecting squares of block 5 cannot contain this value.

   R6C4 - removing <1> from <13569> leaving <3569>.
   R6C5 - removing <1> from <1235> leaving <235>.

Deduction pass 2; 28 squares solved; 53 remaining.

* Intersection of row 9 with block 9. The values <37> can only appear in squares R9C7, R9C8 and R9C9 of row 9.  Thus, the non-intersecting squares of block 9 cannot contain these values.

   R7C7 - removing <3> from <3456> leaving <456>.
   R7C8 - removing <3> from <13569> leaving <1569>.
   R7C9 - removing <3> from <13469> leaving <1469>.
   R8C7 - removing <3> from <3456> leaving <456>.

Deduction pass 3; 28 squares solved; 53 remaining.

* Intersection of column 1 with block 1. The value <6> can only appear in squares R1C1, R2C1 and R3C1 of column 1.  Thus, the non-intersecting squares of block 1 cannot contain this value.

   R1C3 - removing <6> from <12568> leaving <1258>.
   R2C3 - removing <6> from <12468> leaving <1248>.
   R3C3 - removing <6> from <124689> leaving <12489>.

Deduction pass 4; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 11 cycles, it became clear that R3C3 could not be a <2>, because this would force both R6C1 and R9C1 to be <1>.  As they are in the same column, this is a contradiction.

   R3C3 - removing <2> from <12489> leaving <1489>.

Deduction pass 5; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 13 cycles, it became clear that R7C3 could not be a <9>, because this would force both R2C1 and R1C1 to be <6>.  As they are in the same column, this is a contradiction.

   R7C3 - removing <9> from <12469> leaving <1246>.

Deduction pass 6; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 15 cycles, it became clear that R8C3 could not be a <9>, because this would force both R2C1 and R1C1 to be <6>.  As they are in the same column, this is a contradiction.

   R8C3 - removing <9> from <1469> leaving <146>.

Deduction pass 7; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 22 cycles, it became clear that R1C3 could not be a <2>, because this would force both R6C4 and R3C4 to be <6>.  As they are in the same column, this is a contradiction.

   R1C3 - removing <2> from <1258> leaving <158>.

Deduction pass 8; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 23 cycles, it became clear that R6C9 could not be a <9>, because this would force both R1C2 and R6C2 to be <1>.  As they are in the same column, this is a contradiction.

   R6C9 - removing <9> from <23469> leaving <2346>.

Deduction pass 9; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 27 cycles, it became clear that R3C2 could not be a <2>, because this would force both R7C5 and R4C5 to be <5>.  As they are in the same column, this is a contradiction.

   R3C2 - removing <2> from <1249> leaving <149>.

Deduction pass 10; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 41 cycles, it became clear that R2C6 could not be a <1>, because this would force both R9C1 and R9C3 to be <1>.  As they are in the same row, this is a contradiction.

   R2C6 - removing <1> from <12346> leaving <2346>.

Deduction pass 11; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle:

The following verities were found (only first verity proving the assertion is shown):
  R1C1 proves that R2C6<>6

The following veracities were found (may duplicate verities, above):
  R2C6<>6 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R2C6: remove <6> from <2346> leaving <234>.

Deduction pass 12; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 29 cycles, it became clear that R6C7 could not be a <5>, because this would force both R4C8 and R9C8 to be <3>.  As they are in the same column, this is a contradiction.

   R6C7 - removing <5> from <23456> leaving <2346>.

Deduction pass 13; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 26 cycles, it became clear that R4C6 could not be a <9>, because this would force both R6C7 and R6C9 to be <3>.  As they are in the same row, this is a contradiction.

   R4C6 - removing <9> from <2369> leaving <236>.

Deduction pass 14; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 11 cycles, it became clear that R6C7 could not be a <2>, because this would force both R6C1 and R6C3 to be <5>.  As they are in the same row, this is a contradiction.

   R6C7 - removing <2> from <2346> leaving <346>.

Deduction pass 15; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 11 cycles, it became clear that R6C9 could not be a <2>, because this would force both R6C1 and R6C3 to be <5>.  As they are in the same row, this is a contradiction.

   R6C9 - removing <2> from <2346> leaving <346>.

Deduction pass 16; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 13 cycles, it became clear that R5C7 could not be a <5>, because this would force both R4C8 and R9C8 to be <3>.  As they are in the same column, this is a contradiction.

   R5C7 - removing <5> from <257> leaving <27>.

Deduction pass 17; 28 squares solved; 53 remaining.

* Intersection of column 7 with block 9. The value <5> can only appear in squares R7C7, R8C7 and R9C7 of column 7.  Thus, the non-intersecting squares of block 9 cannot contain this value.

   R7C8 - removing <5> from <1569> leaving <169>.

Deduction pass 18; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 22 cycles, it became clear that R2C3 could not be a <2>, because this would force both R2C4 and R3C4 to be <8>.  As they are in the same column, this is a contradiction.

   R2C3 - removing <2> from <1248> leaving <148>.

Deduction pass 19; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R1C9 could not be a <2>, because this would force both R3C5 and R4C5 to be <2>.  As they are in the same column, this is a contradiction.

   R1C9 - removing <2> from <1236> leaving <136>.

Deduction pass 20; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 23 cycles, it became clear that R2C3 could not be a <1>, because this would force both R6C7 and R6C9 to be <4>.  As they are in the same row, this is a contradiction.

   R2C3 - removing <1> from <148> leaving <48>.

Deduction pass 21; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R3C7 could not be a <6>, because this would force both R7C7 and R8C7 to be <5>.  As they are in the same column, this is a contradiction.

   R3C7 - removing <6> from <268> leaving <28>.

Deduction pass 22; 28 squares solved; 53 remaining.

* Found a Nishio contradiction.  After 2 cycles, it became clear that R4C9 could not be a <6>.

   R4C9 - removing <6> from <2369> leaving <239>.

Deduction pass 23; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 20 cycles, it became clear that R8C2 could not be a <1>, because this would force both R8C5 and R8C7 to be <4>.  As they are in the same row, this is a contradiction.

   R8C2 - removing <1> from <1349> leaving <349>.

Deduction pass 24; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 20 cycles, it became clear that R9C9 could not be a <9>, because this would force both R2C7 and R2C4 to be <3>.  As they are in the same row, this is a contradiction.

   R9C9 - removing <9> from <13479> leaving <1347>.

Deduction pass 25; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 21 cycles, it became clear that R9C9 could not be a <3>, because this would force both R1C1 and R1C9 to be <6>.  As they are in the same row, this is a contradiction.

   R9C9 - removing <3> from <1347> leaving <147>.

Deduction pass 26; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 24 cycles, it became clear that R5C6 could not be a <2>, because this would force both R2C8 and R3C9 to be <1>.  As they are in the same block, this is a contradiction.

   R5C6 - removing <2> from <129> leaving <19>.

Deduction pass 27; 28 squares solved; 53 remaining.

* A set of 2 squares can be constrained.  R5C7 and R5C9 share possibilities <27>.  No other squares in row 5 have those possibilities.  Thus, any additional possibilties they have can be eliminated.

   R5C9 - removing <9> from <279> leaving <27>.

Deduction pass 28; 28 squares solved; 53 remaining.

* 2 squares in block 6 form a simple locked pair.  R5C7 and R5C9 share possibilities <27>.  Thus, these possibilities can be removed from the rest of the block.

   R4C9 - removing <2> from <239> leaving <39>.

Deduction pass 29; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 14 cycles, it became clear that R6C9 could not be a <3>, because this would force both R1C9 and R1C2 to be <1>.  As they are in the same row, this is a contradiction.

   R6C9 - removing <3> from <346> leaving <46>.

Deduction pass 30; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 17 cycles, it became clear that R4C1 could not be a <9>, because this would force both R1C9 and R1C2 to be <1>.  As they are in the same row, this is a contradiction.

   R4C1 - removing <9> from <259> leaving <25>.

Deduction pass 31; 28 squares solved; 53 remaining.

* Intersection of row 4 with block 6. The value <9> can only appear in squares R4C7, R4C8 and R4C9 of row 4.  Thus, the non-intersecting squares of block 6 cannot contain this value.

   R5C8 - removing <9> from <59> leaving <5>.


Deduction pass 32; 29 squares solved; 52 remaining.

* 2 squares in block 5 form a simple locked pair.  R5C4 and R5C6 share possibilities <19>.  Thus, these possibilities can be removed from the rest of the block.

   R6C4 - removing <9> from <3569> leaving <356>.

Deduction pass 33; 29 squares solved; 52 remaining.

* Found a contradiction by Bowman Bingo.  After 12 cycles, it became clear that R2C7 could not be a <6>, because this would force both R4C6 and R4C8 to be <6>.  As they are in the same row, this is a contradiction.

   R2C7 - removing <6> from <2368> leaving <238>.

Deduction pass 34; 29 squares solved; 52 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R3C5 could not be a <1>, because this would force both R1C9 and R2C7 to be <3>.  As they are in the same block, this is a contradiction.

   R3C5 - removing <1> from <124> leaving <24>.

Deduction pass 35; 29 squares solved; 52 remaining.

* Intersection of column 5 with block 8. The value <1> can only appear in squares R7C5, R8C5 and R9C5 of column 5.  Thus, the non-intersecting squares of block 8 cannot contain this value.

   R7C6 - removing <1> from <1349> leaving <349>.
   R8C4 - removing <1> from <1359> leaving <359>.
   R8C6 - removing <1> from <1349> leaving <349>.

Deduction pass 36; 29 squares solved; 52 remaining.

* Found a contradiction by Bowman Bingo.  After 4 cycles, it became clear that R8C5 could not be a <3>, because this would force both R9C3 and R8C2 to be <4>.  As they are in the same block, this is a contradiction.

   R8C5 - removing <3> from <1345> leaving <145>.

Deduction pass 37; 29 squares solved; 52 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R9C9 could not be a <1>, because this would force both R3C5 and R3C2 to be <4>.  As they are in the same row, this is a contradiction.

   R9C9 - removing <1> from <147> leaving <47>.

Deduction pass 38; 29 squares solved; 52 remaining.

* Found a contradiction by Bowman Bingo.  After 11 cycles, it became clear that R4C1 could not be a <2>, because this would force both R7C2 and R7C6 to be <4>.  As they are in the same row, this is a contradiction.

   R4C1 - removing <2> from <25> leaving <5>.


Deduction pass 39; 30 squares solved; 51 remaining.

* R1C3 is the only square in row 1 that can be a <5>.  It is thus pinned to that value.


Deduction pass 40; 31 squares solved; 50 remaining.

* R1C4 is the only square in row 1 that can be a <8>.  It is thus pinned to that value.


Deduction pass 41; 32 squares solved; 49 remaining.

* 3 squares in row 6 form a simple locked triplet.  R6C1, R6C2 and R6C3 share possibilities <129>.  Thus, these possibilities can be removed from the rest of the row.

   R6C5 - removing <2> from <235> leaving <35>.

Deduction pass 42; 32 squares solved; 49 remaining.

* Found a contradiction by Bowman Bingo.  After 3 cycles, it became clear that R3C2 could not be a <1>, because this would force both R1C1 and R2C1 to be <6>.  As they are in the same column, this is a contradiction.

   R3C2 - removing <1> from <149> leaving <49>.

Deduction pass 43; 32 squares solved; 49 remaining.

* Found a contradiction by Bowman Bingo.  After 3 cycles, it became clear that R3C3 could not be a <1>, because this would force both R1C1 and R2C1 to be <6>.  As they are in the same column, this is a contradiction.

   R3C3 - removing <1> from <1489> leaving <489>.

Deduction pass 44; 32 squares solved; 49 remaining.

* A set of 2 squares can be constrained.  R3C4 and R3C9 share possibilities <16>.  No other squares in row 3 have those possibilities.  Thus, any additional possibilties they have can be eliminated.

   R3C9 - removing <2> from <126> leaving <16>.

Deduction pass 45; 32 squares solved; 49 remaining.

* R5C9 is the only square in column 9 that can be a <2>.  It is thus pinned to that value.

From this deduction, the following moves are immediately forced:

   R5C7 must be <7>.

Deduction pass 46; 34 squares solved; 47 remaining.

* R9C9 is the only square in row 9 that can be a <7>.  It is thus pinned to that value.


Deduction pass 47; 35 squares solved; 46 remaining.

* A set of 2 squares can be constrained.  R2C7 and R3C7 share possibilities <28>.  No other squares in column 7 have those possibilities.  Thus, any additional possibilties they have can be eliminated.

   R2C7 - removing <3> from <238> leaving <28>.

Deduction pass 48; 35 squares solved; 46 remaining.

* Found a contradiction by Bowman Bingo.  After 10 cycles, it became clear that R7C9 could not be a <9>, because this would force both R9C3 and R2C3 to be <4>.  As they are in the same column, this is a contradiction.

   R7C9 - removing <9> from <1469> leaving <146>.

Deduction pass 49; 35 squares solved; 46 remaining.

* R4C9 is the only square in column 9 that can be a <9>.  It is thus pinned to that value.


Deduction pass 50; 36 squares solved; 45 remaining.

* R1C9 is the only square in column 9 that can be a <3>.  It is thus pinned to that value.


Deduction pass 51; 37 squares solved; 44 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R6C7 could not be a <6>, because this would force both R3C2 and R3C3 to be <9>.  As they are in the same row, this is a contradiction.

   R6C7 - removing <6> from <346> leaving <34>.

Deduction pass 52; 37 squares solved; 44 remaining.

* 2 squares in column 7 form a simple locked pair.  R6C7 and R9C7 share possibilities <34>.  Thus, these possibilities can be removed from the rest of the column.

   R7C7 - removing <4> from <456> leaving <56>.
   R8C7 - removing <4> from <456> leaving <56>.

Deduction pass 53; 37 squares solved; 44 remaining.

* 2 squares in block 9 form a simple locked pair.  R7C7 and R8C7 share possibilities <56>.  Thus, these possibilities can be removed from the rest of the block.

   R7C8 - removing <6> from <169> leaving <19>.
   R7C9 - removing <6> from <146> leaving <14>.

Deduction pass 54; 37 squares solved; 44 remaining.

* There is a "Fishy Cycle" in the puzzle, as follows:

   {R3} -- R3C4 -- (C4) -- R6C4 -- {R6}
   {R6} -- R6C9 -- (B6) -- R4C8 -- {C8}
   {C8} -- R2C8 -- (B3) -- R3C9 -- {R3}

   R2C4 - removing <6> from <136> leaving <13>.

Deduction pass 55; 37 squares solved; 44 remaining.

* Found a contradiction by Bowman Bingo.  After 9 cycles, it became clear that R9C7 could not be a <3>, because this would force both R2C6 and R3C5 to be <4>.  As they are in the same block, this is a contradiction.

   R9C7 - removing <3> from <34> leaving <4>.

From this deduction, the following moves are immediately forced:

   R6C7 must be <3>.
   R7C9 must be <1>.
   R6C5 must be <5>.
   R4C8 must be <6>.
   R7C8 must be <9>.
   R3C9 must be <6>.
   R3C4 must be <1>.
   R6C9 must be <4>.
   R2C8 must be <1>.
   R6C4 must be <6>.
   R9C8 must be <3>.
   R2C4 must be <3>.
   R5C4 must be <9>.
   R5C6 must be <1>.
   R8C4 must be <5>.
   R8C7 must be <6>.
   R7C7 must be <5>.

Deduction pass 56; 55 squares solved; 26 remaining.

* R2C1 is the only square in row 2 that can be a <6>.  It is thus pinned to that value.


Deduction pass 57; 56 squares solved; 25 remaining.

* R1C6 is the only square in row 1 that can be a <6>.  It is thus pinned to that value.


Deduction pass 58; 57 squares solved; 24 remaining.

* R7C3 is the only square in row 7 that can be a <6>.  It is thus pinned to that value.


Deduction pass 59; 58 squares solved; 23 remaining.

* R7C2 is the only square in row 7 that can be a <2>.  It is thus pinned to that value.

From this deduction, the following moves are immediately forced:

   R1C2 must be <1>.
   R1C1 must be <2>.
   R6C2 must be <9>.
   R3C2 must be <4>.
   R6C1 must be <1>.
   R3C5 must be <2>.
   R8C2 must be <3>.
   R2C3 must be <8>.
   R3C7 must be <8>.
   R4C5 must be <3>.
   R2C6 must be <4>.
   R3C3 must be <9>.
   R2C7 must be <2>.
   R4C6 must be <2>.
   R7C5 must be <4>.
   R6C3 must be <2>.
   R9C1 must be <9>.
   R7C6 must be <3>.
   R8C5 must be <1>.
   R8C6 must be <9>.
   R8C3 must be <4>.
   R9C3 must be <1>.

Deduction pass 60; 81 squares solved; 0 remaining.

Solution found!

Deduction completed...

Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Wed Aug 10, 2005 6:41 pm    Post subject: Reply with quote

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

Code:

Deduction pass 1; 28 squares solved; 53 remaining.

* Intersection of row 5 with block 5. The value <1> can only appear in squares R5C4, R5C5 and R5C6 of row 5.  Thus, the non-intersecting squares of block 5 cannot contain this value.

   R6C4 - removing <1> from <13569> leaving <3569>.
   R6C5 - removing <1> from <1235> leaving <235>.

Deduction pass 2; 28 squares solved; 53 remaining.

* Intersection of row 9 with block 9. The values <37> can only appear in squares R9C7, R9C8 and R9C9 of row 9.  Thus, the non-intersecting squares of block 9 cannot contain these values.

   R7C7 - removing <3> from <3456> leaving <456>.
   R7C8 - removing <3> from <13569> leaving <1569>.
   R7C9 - removing <3> from <13469> leaving <1469>.
   R8C7 - removing <3> from <3456> leaving <456>.

Deduction pass 3; 28 squares solved; 53 remaining.

* Intersection of column 1 with block 1. The value <6> can only appear in squares R1C1, R2C1 and R3C1 of column 1.  Thus, the non-intersecting squares of block 1 cannot contain this value.

   R1C3 - removing <6> from <12568> leaving <1258>.
   R2C3 - removing <6> from <12468> leaving <1248>.
   R3C3 - removing <6> from <124689> leaving <12489>.

Deduction pass 4; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 8279 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R3C3<>2 (Implied by all possible values of R1C1)
  R7C3<>9 (Implied by all possible values of R1C1)
  R8C3<>9 (Implied by all possible values of R1C1)
  R1C3<>2 (Implied by all possible values of R1C1)
  R2C6<>1 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R1C3<>2 (Implied by all R1=1 squares)
  R2C6<>1 (Implied by all R1=1 squares)
  R3C3<>2 (Implied by all R1=1 squares)
  R7C3<>9 (Implied by all R1=1 squares)
  R8C3<>9 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R1C3: remove <2> from <1258> leaving <158>.
   R2C6: remove <1> from <12346> leaving <2346>.
   R3C3: remove <2> from <12489> leaving <1489>.
   R7C3: remove <9> from <12469> leaving <1246>.
   R8C3: remove <9> from <1469> leaving <146>.

Deduction pass 5; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 23 cycles, it became clear that R6C9 could not be a <9>, because this would force both R1C2 and R6C2 to be <1>.  As they are in the same column, this is a contradiction.

   R6C9 - removing <9> from <23469> leaving <2346>.

Deduction pass 6; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 6059 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R2C6<>6 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R2C6<>6 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R2C6: remove <6> from <2346> leaving <234>.

Deduction pass 7; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 6149 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R2C7<>6 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R2C7<>6 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R2C7: remove <6> from <2368> leaving <238>.

Deduction pass 8; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 27 cycles, it became clear that R3C2 could not be a <2>, because this would force both R7C5 and R4C5 to be <5>.  As they are in the same column, this is a contradiction.

   R3C2 - removing <2> from <1249> leaving <149>.

Deduction pass 9; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 29 cycles, it became clear that R6C7 could not be a <5>, because this would force both R4C8 and R9C8 to be <3>.  As they are in the same column, this is a contradiction.

   R6C7 - removing <5> from <23456> leaving <2346>.

Deduction pass 10; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 26 cycles, it became clear that R4C6 could not be a <9>, because this would force both R6C7 and R6C9 to be <3>.  As they are in the same row, this is a contradiction.

   R4C6 - removing <9> from <2369> leaving <236>.

Deduction pass 11; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 6072 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R8C3<>1 (Implied by all possible values of R1C1)
  R8C6<>4 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R8C3<>1 (Implied by all R1=1 squares)
  R8C6<>4 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R8C3: remove <1> from <146> leaving <46>.
   R8C6: remove <4> from <1349> leaving <139>.

Deduction pass 12; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 6135 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R3C2<>1 (Implied by all possible values of R1C1)
  R3C3<>1 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R3C2<>1 (Implied by all R1=1 squares)
  R3C3<>1 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R3C2: remove <1> from <149> leaving <49>.
   R3C3: remove <1> from <1489> leaving <489>.

Deduction pass 13; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 5900 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R1C4<>1 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R1C4<>1 (Implied by all R1=1 squares)

The following squares can have possibilities eliminated:
   R1C4: remove <1> from <1368> leaving <368>.

Deduction pass 14; 28 squares solved; 53 remaining.

* Found a contradiction by Bowman Bingo.  After 11 cycles, it became clear that R6C7 could not be a <2>, because this would force both R6C1 and R6C3 to be <5>.  As they are in the same row, this is a contradiction.

   R6C7 - removing <2> from <2346> leaving <346>.

Deduction pass 15; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 6101 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R5C7<>5 (Implied by all possible values of R1C1)
  R5C9<>9 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R5C7<>5 (Implied by all R1=1 squares)
  R5C9<>9 (Implied by all R1=1 squares)
  R7C8<>5 (Implied by all R7=5 squares)

The following squares can have possibilities eliminated:
   R5C7: remove <5> from <257> leaving <27>.
   R5C9: remove <9> from <279> leaving <27>.
   R7C8: remove <5> from <1569> leaving <169>.

Deduction pass 16; 28 squares solved; 53 remaining.

* 2 squares in row 5 form a simple locked pair.  R5C7 and R5C9 share possibilities <27>.  Thus, these possibilities can be removed from the rest of the row.

   R5C6 - removing <2> from <129> leaving <19>.

Deduction pass 17; 28 squares solved; 53 remaining.

* 2 squares in block 6 form a simple locked pair.  R5C7 and R5C9 share possibilities <27>.  Thus, these possibilities can be removed from the rest of the block.

   R4C9 - removing <2> from <2369> leaving <369>.
   R6C9 - removing <2> from <2346> leaving <346>.

Deduction pass 18; 28 squares solved; 53 remaining.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 12520 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R2C1=6 (Implied by all possible values of R1C1)
  R1C1<>6 (Implied by all possible values of R1C1)
  R1C6<>1 (Implied by all possible values of R1C1)
  R2C3<>1 (Implied by all possible values of R1C1)
  R2C3<>2 (Implied by all possible values of R1C1)
  R2C4<>6 (Implied by all possible values of R1C1)
  R2C8<>6 (Implied by all possible values of R1C1)
  R3C4<>8 (Implied by all possible values of R1C1)
  R2C1<>2 (Implied by all possible values of R1C1)
  R2C1<>1 (Implied by all possible values of R1C1)
  R1C4<>6 (Implied by all possible values of R1C1)
  R7C5<>3 (Implied by all possible values of R1C1)
  R8C2<>1 (Implied by all possible values of R1C1)
  R4C6<>3 (Implied by all possible values of R1C1)
  R1C6<>3 (Implied by all possible values of R1C1)
  R8C5<>3 (Implied by all possible values of R1C1)
  R7C2<>1 (Implied by all possible values of R1C1)
  R2C3<>4 (Implied by all possible values of R1C1)
  R3C5<>4 (Implied by all possible values of R1C1)
  R3C3<>8 (Implied by all possible values of R1C1)
  R2C6=4 (Implied by all possible values of R1C1)
  R7C6<>4 (Implied by all possible values of R1C1)
  R2C6<>2 (Implied by all possible values of R1C1)
  R2C6<>3 (Implied by all possible values of R1C1)
  R8C4<>3 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R1C1<>1 (Implied by all R7=6 squares)
  R1C1<>5 (Implied by all R4=5 squares)
  R1C1<>6 (Implied by all R1=6 squares)
  R1C2=1 (Implied by all R7=6 squares)
  R1C2<>2 (Implied by all R7=6 squares)
  R1C3=5 (Implied by all R4=5 squares)
  R1C3<>1 (Implied by all R4=5 squares)
  R1C3<>8 (Implied by all R1=8 squares)
  R1C4=8 (Implied by the last remaining R1<>8 square)
  R1C4<>3 (Implied by all R1=3 squares)
  R1C4<>6 (Implied by all R1=1 squares)
  R1C6=6 (Implied by all R4=2 squares)
  R1C6<>1 (Implied by all R1=1 squares)
  R1C6<>2 (Implied by all R1=2 squares)
  R1C6<>3 (Implied by all R1=1 squares)
  R1C9<>1 (Implied by all R1=1 squares)
  R1C9<>2 (Implied by all R1=2 squares)
  R1C9<>6 (Implied by all R1=3 squares)
  R2C1=6 (Implied by all R1=6 squares)
  R2C1<>1 (Implied by all R1=1 squares)
  R2C1<>2 (Implied by all R1=1 squares)
  R2C3<>1 (Implied by all R1=1 squares)
  R2C3<>2 (Implied by all R1=1 squares)
  R2C3<>4 (Implied by all R1=1 squares)
  R2C4<>1 (Implied by all R2=1 squares)
  R2C4<>6 (Implied by all R1=6 squares)
  R2C4<>8 (Implied by all R1=8 squares)
  R2C6=4 (Implied by all R1=1 squares)
  R2C6<>2 (Implied by all R1=1 squares)
  R2C6<>3 (Implied by all R1=1 squares)
  R2C7<>3 (Implied by all R1=3 squares)
  R2C7<>8 (Implied by all R2=2 squares)
  R2C8<>3 (Implied by all R1=3 squares)
  R2C8<>6 (Implied by all R1=6 squares)
  R3C2=4 (Implied by all R7=6 squares)
  R3C2<>9 (Implied by all R7=6 squares)
  R3C3=9 (Implied by all R7=6 squares)
  R3C3<>4 (Implied by all R7=6 squares)
  R3C3<>8 (Implied by all R1=1 squares)
  R3C4<>6 (Implied by all R1=6 squares)
  R3C4<>8 (Implied by all R1=1 squares)
  R3C5<>1 (Implied by all R3=1 squares)
  R3C5<>4 (Implied by all R1=1 squares)
  R3C7=8 (Implied by all R2=2 squares)
  R3C7<>2 (Implied by all R2=2 squares)
  R3C7<>6 (Implied by all R2=2 squares)
  R3C9<>1 (Implied by all R2=1 squares)
  R3C9<>2 (Implied by all R2=2 squares)
  R4C1<>2 (Implied by all R4=2 squares)
  R4C1<>9 (Implied by all R4=5 squares)
  R4C5<>2 (Implied by all R3=2 squares)
  R4C5<>5 (Implied by all R4=3 squares)
  R4C6<>3 (Implied by all R1=1 squares)
  R4C6<>6 (Implied by all R1=6 squares)
  R4C8<>3 (Implied by all R4=3 squares)
  R4C8<>5 (Implied by all R4=5 squares)
  R4C8<>9 (Implied by all R4=6 squares)
  R4C9=9 (Implied by all R4=6 squares)
  R4C9<>3 (Implied by all R1=3 squares)
  R4C9<>6 (Implied by all R3=6 squares)
  R5C4<>1 (Implied by all R3=1 squares)
  R5C4<>5 (Implied by all R4=5 squares)
  R5C6=1 (Implied by all R3=1 squares)
  R5C6<>9 (Implied by all R3=1 squares)
  R5C7=7 (Implied by all R2=2 squares)
  R5C7<>2 (Implied by all R2=2 squares)
  R5C8=5 (Implied by all R4=5 squares)
  R5C8<>9 (Implied by all R4=5 squares)
  R5C9=2 (Implied by all R2=2 squares)
  R5C9<>7 (Implied by all R2=2 squares)
  R6C1<>5 (Implied by all R4=5 squares)
  R6C1<>9 (Implied by all R7=6 squares)
  R6C2=9 (Implied by all R7=6 squares)
  R6C2<>1 (Implied by all R7=6 squares)
  R6C2<>2 (Implied by all R7=6 squares)
  R6C3<>5 (Implied by all R4=5 squares)
  R6C3<>9 (Implied by all R7=6 squares)
  R6C4=6 (Implied by all R1=6 squares)
  R6C4<>3 (Implied by all R1=6 squares)
  R6C4<>5 (Implied by all R1=6 squares)
  R6C4<>9 (Implied by all R1=3 squares)
  R6C5<>2 (Implied by all R3=2 squares)
  R6C5<>3 (Implied by all R4=3 squares)
  R6C7<>4 (Implied by all R6=3 squares)
  R6C7<>6 (Implied by all R1=6 squares)
  R6C9=4 (Implied by all R6=3 squares)
  R6C9<>3 (Implied by all R1=3 squares)
  R6C9<>6 (Implied by all R1=6 squares)
  R7C2=2 (Implied by all R7=6 squares)
  R7C2<>1 (Implied by all R1=1 squares)
  R7C2<>3 (Implied by all R7=6 squares)
  R7C2<>4 (Implied by all R7=4 squares)
  R7C2<>9 (Implied by all R7=6 squares)
  R7C3=6 (Implied by all R8=4 squares)
  R7C3<>1 (Implied by all R7=1 squares)
  R7C3<>2 (Implied by all R7=6 squares)
  R7C3<>4 (Implied by all R7=4 squares)
  R7C5<>1 (Implied by all R7=1 squares)
  R7C5<>3 (Implied by all R1=1 squares)
  R7C5<>5 (Implied by all R7=4 squares)
  R7C6<>1 (Implied by all R3=1 squares)
  R7C6<>4 (Implied by all R1=1 squares)
  R7C6<>9 (Implied by all R7=6 squares)
  R7C7=5 (Implied by all R7=4 squares)
  R7C7<>4 (Implied by all R7=4 squares)
  R7C7<>6 (Implied by all R7=4 squares)
  R7C8<>1 (Implied by all R2=1 squares)
  R7C8<>6 (Implied by all R4=6 squares)
  R7C9<>4 (Implied by all R6=3 squares)
  R7C9<>6 (Implied by all R3=6 squares)
  R7C9<>9 (Implied by all R4=6 squares)
  R8C2=3 (Implied by all R7=6 squares)
  R8C2<>1 (Implied by all R1=1 squares)
  R8C2<>4 (Implied by all R7=4 squares)
  R8C2<>9 (Implied by all R7=6 squares)
  R8C3=4 (Implied by all R7=6 squares)
  R8C3<>6 (Implied by all R7=6 squares)
  R8C4<>1 (Implied by all R3=1 squares)
  R8C4<>3 (Implied by all R1=1 squares)
  R8C4<>9 (Implied by all R3=1 squares)
  R8C5<>3 (Implied by all R1=1 squares)
  R8C5<>4 (Implied by all R7=4 squares)
  R8C5<>5 (Implied by all R8=1 squares)
  R8C6<>1 (Implied by all R3=1 squares)
  R8C6<>3 (Implied by all R7=6 squares)
  R8C7=6 (Implied by all R7=6 squares)
  R8C7<>4 (Implied by all R7=6 squares)
  R8C7<>5 (Implied by all R7=4 squares)
  R9C3<>4 (Implied by all R7=6 squares)
  R9C3<>9 (Implied by all R7=6 squares)
  R9C7<>3 (Implied by all R6=3 squares)
  R9C7<>7 (Implied by all R2=2 squares)
  R9C8=3 (Implied by all R7=6 squares)
  R9C8<>1 (Implied by all R2=1 squares)
  R9C8<>9 (Implied by all R7=6 squares)
  R9C9=7 (Implied by all R2=2 squares)
  R9C9<>1 (Implied by all R2=2 squares)
  R9C9<>3 (Implied by all R1=3 squares)
  R9C9<>4 (Implied by all R1=3 squares)
  R9C9<>9 (Implied by all R1=3 squares)

The following squares can have possibilities eliminated:
   R1C1: remove <6> from <1256> leaving <125>.
   R1C3: remove <8> from <158> leaving <15>.
   R3C3: remove <8> from <489> leaving <49>.
   R7C2: remove <14> from <12349> leaving <239>.
   R7C3: remove <14> from <1246> leaving <26>.
   R7C6: remove <14> from <1349> leaving <39>.
   R8C2: remove <14> from <1349> leaving <39>.
   R8C6: remove <1> from <139> leaving <39>.

The following squares can be solved:
   R1C4 = 8
   R1C6 = 6
   R1C9 = 3
   R2C1 = 6
   R2C3 = 8
   R2C4 = 3
   R2C6 = 4
   R2C7 = 2
   R2C8 = 1
   R3C4 = 1
   R3C5 = 2
   R3C7 = 8
   R3C9 = 6
   R4C1 = 5
   R4C5 = 3
   R4C6 = 2
   R4C8 = 6
   R4C9 = 9
   R5C4 = 9
   R5C6 = 1
   R5C7 = 7
   R5C8 = 5
   R5C9 = 2
   R6C4 = 6
   R6C5 = 5
   R6C7 = 3
   R6C9 = 4
   R7C5 = 4
   R7C7 = 5
   R7C8 = 9
   R7C9 = 1
   R8C4 = 5
   R8C5 = 1
   R8C7 = 6
   R9C7 = 4
   R9C8 = 3
   R9C9 = 7

Tabling was terminated 8 rounds after finding the first reduction or solve...

From this deduction, the following moves are immediately forced:

   R7C6 must be <3>.
   R8C3 must be <4>.
   R7C2 must be <2>.
   R8C6 must be <9>.
   R3C3 must be <9>.
   R8C2 must be <3>.
   R3C2 must be <4>.
   R9C3 must be <1>.
   R7C3 must be <6>.
   R1C2 must be <1>.
   R9C1 must be <9>.
   R1C3 must be <5>.
   R6C3 must be <2>.
   R1C1 must be <2>.
   R6C2 must be <9>.
   R6C1 must be <1>.

Deduction pass 19; 81 squares solved; 0 remaining.

Solution found!
Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Thu Aug 11, 2005 9:50 am    Post subject: Praise be to Doug! Tables now cracks everything by itself. Reply with quote

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:

Code:

Susser Buster #2
+-------+-------+-------+
| . . . | . 7 . | 9 4 . |
| . 7 . | . 9 . | . . 5 |
| 3 . . | . . 5 | . 7 . |
+-------+-------+-------+
| . 8 7 | 4 . . | 1 . . |
| 4 6 3 | . 8 . | . . . |
| . . . | . . 7 | . 8 . |
+-------+-------+-------+
| 8 . . | 7 . . | . . . |
| 7 . . | . . . | . 2 8 |
| . 5 . | 2 6 8 | . . . |
+-------+-------+-------+

Prepare to be shocked.  Tables now destroys the puzzle.  2 tables and its solved!

* Intersection of row 5 with block 5. The value <1> can only appear in squares R5C4, R5C5 and R5C6 of row 5.  Thus, the non-intersecting squares of block 5 cannot contain this value.

   R6C4 - removing <1> from <13569> leaving <3569>.
   R6C5 - removing <1> from <1235> leaving <235>.

* Intersection of row 9 with block 9. The values <37> can only appear in squares R9C7, R9C8 and R9C9 of row 9.  Thus, the non-intersecting squares of block 9 cannot contain these values.

   R7C7 - removing <3> from <3456> leaving <456>.
   R7C8 - removing <3> from <13569> leaving <1569>.
   R7C9 - removing <3> from <13469> leaving <1469>.
   R8C7 - removing <3> from <3456> leaving <456>.

* Intersection of column 1 with block 1. The value <6> can only appear in squares R1C1, R2C1 and R3C1 of column 1.  Thus, the non-intersecting squares of block 1 cannot contain this value.

   R1C3 - removing <6> from <12568> leaving <1258>.
   R2C3 - removing <6> from <12468> leaving <1248>.
   R3C3 - removing <6> from <124689> leaving <12489>.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 14028 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R3C3<>2 (Implied by all possible values of R1C1)
  R7C3<>9 (Implied by all possible values of R1C1)
  R8C3<>9 (Implied by all possible values of R1C1)
  R1C3<>2 (Implied by all possible values of R1C1)
  R2C6<>1 (Implied by all possible values of R1C1)
  R2C6<>3 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R1C3<>2 (Implied by all R1=1 squares)
  R2C6<>1 (Implied by all R1=1 squares)
  R2C6<>3 (Implied by all R1=1 squares)
  R2C6<>6 (Implied by all R1=3 squares)
  R2C7<>6 (Implied by at least 2 R8<>6 squares)
  R3C2<>1 (Implied by at least 2 R4<>2 squares)
  R3C2<>2 (Implied by all R3=1 squares)
  R3C3<>1 (Implied by all R4=5 squares)
  R3C3<>2 (Implied by all R1=1 squares)
  R3C3<>4 (Implied by at least 2 R8<>3 squares)
  R4C6<>3 (Implied by all R8=3 squares)
  R5C7<>5 (Implied by at least 2 R5<>2 squares)
  R6C4<>3 (Implied by all C5=3 squares)
  R6C7<>2 (Implied by all R1=3 squares)
  R6C7<>5 (Implied by all R6=4 squares)
  R6C9<>2 (Implied by all R2=1 squares)
  R6C9<>9 (Implied by all R2=1 squares)
  R7C3<>4 (Implied by at least 2 R8<>3 squares)
  R7C3<>9 (Implied by all R1=1 squares)
  R7C5<>3 (Implied by at least 2 R5<>1 squares)
  R7C6<>1 (Implied by all R7=1 squares)
  R7C8<>5 (Implied by all C7=5 squares)
  R8C2<>1 (Implied by all R1=1 squares)
  R8C3<>9 (Implied by all R1=1 squares)
  R8C5<>3 (Implied by all R8=1 squares)

The following squares can have possibilities eliminated:
   R1C3: remove <2> from <1258> leaving <158>.
   R2C6: remove <136> from <12346> leaving <24>.
   R2C7: remove <6> from <2368> leaving <238>.
   R3C2: remove <12> from <1249> leaving <49>.
   R3C3: remove <124> from <12489> leaving <89>.
   R4C6: remove <3> from <2369> leaving <269>.
   R5C7: remove <5> from <257> leaving <27>.
   R6C4: remove <3> from <3569> leaving <569>.
   R6C7: remove <25> from <23456> leaving <346>.
   R6C9: remove <29> from <23469> leaving <346>.
   R7C3: remove <49> from <12469> leaving <126>.
   R7C5: remove <3> from <1345> leaving <145>.
   R7C6: remove <1> from <1349> leaving <349>.
   R7C8: remove <5> from <1569> leaving <169>.
   R8C2: remove <1> from <1349> leaving <349>.
   R8C3: remove <9> from <1469> leaving <146>.
   R8C5: remove <3> from <1345> leaving <145>.

Tabling was terminated 8 rounds after finding the first reduction or solve, or as soon as at least 5 reductions or solves were found...

Notice this comment about terminating the run.  Likely if it had run on, it would have solved the puzzle in a single run!  I have some limits on how much the algorithm will do so that it doesn't run-away, but it is likely these can be removed.  If so, it should crack any puzzle in a single execution.

* Made progress using Trebor's Tables to find inferences about the puzzle.  A total of 13112 implications about the puzzle were generated and examined in order to find these inferences - you'd run through several pencils working them out by hand!

The following verities were found (only first verity proving the assertion is shown):
  R1C1<>1 (Implied by all possible values of R1C1)
  R6C3<>9 (Implied by all possible values of R1C1)

The following veracities were found (may duplicate verities, above):
  R1C1=2 (Implied by all R2=1 squares)
  R1C1<>1 (Implied by all R1=1 squares)
  R1C1<>5 (Implied by all R2=1 squares)
  R1C1<>6 (Implied by all R1=2 squares)
  R1C2=1 (Implied by all R1=1 squares)
  R1C2<>2 (Implied by all R1=1 squares)
  R1C3=5 (Implied by all R2=1 squares)
  R1C3<>1 (Implied by all R1=1 squares)
  R1C3<>8 (Implied by all R2=1 squares)
  R1C4=8 (Implied by all R2=1 squares)
  R1C4<>1 (Implied by all R1=1 squares)
  R1C4<>3 (Implied by all R2=1 squares)
  R1C4<>6 (Implied by all R2=1 squares)
  R1C6=6 (Implied by all R2=1 squares)
  R1C6<>1 (Implied by all R1=1 squares)
  R1C6<>2 (Implied by all R2=1 squares)
  R1C6<>3 (Implied by all R1=3 squares)
  R1C9=3 (Implied by all R2=1 squares)
  R1C9<>1 (Implied by all R1=1 squares)
  R1C9<>2 (Implied by all R2=1 squares)
  R1C9<>6 (Implied by all R1=6 squares)
  R2C1=6 (Implied by all R1=2 squares)
  R2C1<>1 (Implied by all R1=1 squares)
  R2C1<>2 (Implied by all R1=2 squares)
  R2C3=8 (Implied by all R2=1 squares)
  R2C3<>1 (Implied by all R1=1 squares)
  R2C3<>2 (Implied by all R2=1 squares)
  R2C3<>4 (Implied by all R1=3 squares)
  R2C4=3 (Implied by all R2=1 squares)
  R2C4<>1 (Implied by all R2=1 squares)
  R2C4<>6 (Implied by all R1=2 squares)
  R2C4<>8 (Implied by all R2=1 squares)
  R2C6=4 (Implied by all R1=3 squares)
  R2C6<>2 (Implied by all R1=3 squares)
  R2C7=2 (Implied by all R2=1 squares)
  R2C7<>3 (Implied by all R2=1 squares)
  R2C7<>8 (Implied by all R2=1 squares)
  R2C8=1 (Implied by all R2=1 squares)
  R2C8<>3 (Implied by all R2=1 squares)
  R2C8<>6 (Implied by all R1=2 squares)
  R3C2=4 (Implied by all R1=3 squares)
  R3C2<>9 (Implied by all R1=3 squares)
  R3C3=9 (Implied by at least 2 R1<>2 squares)
  R3C3<>8 (Implied by all R1=3 squares)
  R3C4=1 (Implied by all R2=1 squares)
  R3C4<>6 (Implied by all R2=1 squares)
  R3C4<>8 (Implied by all R1=2 squares)
  R3C5=2 (Implied by all R2=1 squares)
  R3C5<>1 (Implied by all R2=1 squares)
  R3C5<>4 (Implied by all R1=3 squares)
  R3C7=8 (Implied by all R2=1 squares)
  R3C7<>2 (Implied by all R2=1 squares)
  R3C7<>6 (Implied by all R2=1 squares)
  R3C9=6 (Implied by all R2=1 squares)
  R3C9<>1 (Implied by all R2=1 squares)
  R3C9<>2 (Implied by all R2=1 squares)
  R4C1=5 (Implied by all R2=1 squares)
  R4C1<>2 (Implied by all R2=1 squares)
  R4C1<>9 (Implied by all R2=1 squares)
  R4C5=3 (Implied by all R2=1 squares)
  R4C5<>2 (Implied by all R2=1 squares)
  R4C5<>5 (Implied by all R2=1 squares)
  R4C6=2 (Implied by all R2=1 squares)
  R4C6<>6 (Implied by all R2=1 squares)
  R4C6<>9 (Implied by at least 2 R1<>2 squares)
  R4C8=6 (Implied by all R2=1 squares)
  R4C8<>3 (Implied by all R2=1 squares)
  R4C8<>5 (Implied by all R2=1 squares)
  R4C8<>9 (Implied by all R2=1 squares)
  R4C9=9 (Implied by all R2=1 squares)
  R4C9<>2 (Implied by all R2=1 squares)
  R4C9<>3 (Implied by all R2=1 squares)
  R4C9<>6 (Implied by all R2=1 squares)
  R5C4=9 (Implied by all R2=1 squares)
  R5C4<>1 (Implied by all R2=1 squares)
  R5C4<>5 (Implied by all R2=1 squares)
  R5C6=1 (Implied by all R2=1 squares)
  R5C6<>2 (Implied by all R2=1 squares)
  R5C6<>9 (Implied by all R2=1 squares)
  R5C7=7 (Implied by all R2=1 squares)
  R5C7<>2 (Implied by all R2=1 squares)
  R5C8=5 (Implied by all R2=1 squares)
  R5C8<>9 (Implied by all R2=1 squares)
  R5C9=2 (Implied by all R2=1 squares)
  R5C9<>7 (Implied by all R2=1 squares)
  R5C9<>9 (Implied by all R2=1 squares)
  R6C1=1 (Implied by all R2=1 squares)
  R6C1<>2 (Implied by all R2=1 squares)
  R6C1<>5 (Implied by all R2=1 squares)
  R6C1<>9 (Implied by all R2=1 squares)
  R6C2=9 (Implied by all R2=1 squares)
  R6C2<>1 (Implied by all R1=1 squares)
  R6C2<>2 (Implied by all R2=1 squares)
  R6C3=2 (Implied by all R2=1 squares)
  R6C3<>1 (Implied by all R2=1 squares)
  R6C3<>5 (Implied by all R2=1 squares)
  R6C3<>9 (Implied by all R1=1 squares)
  R6C4=6 (Implied by all R2=1 squares)
  R6C4<>5 (Implied by all R2=1 squares)
  R6C4<>9 (Implied by all R2=1 squares)
  R6C5=5 (Implied by all R2=1 squares)
  R6C5<>2 (Implied by all R2=1 squares)
  R6C5<>3 (Implied by all R2=1 squares)
  R6C7=3 (Implied by all R2=1 squares)
  R6C7<>4 (Implied by all R2=1 squares)
  R6C7<>6 (Implied by all R2=1 squares)
  R6C9=4 (Implied by all R2=1 squares)
  R6C9<>3 (Implied by all R2=1 squares)
  R6C9<>6 (Implied by all R2=1 squares)
  R7C2=2 (Implied by all R2=1 squares)
  R7C2<>1 (Implied by all R1=1 squares)
  R7C2<>3 (Implied by all R2=1 squares)
  R7C2<>4 (Implied by all R1=1 squares)
  R7C2<>9 (Implied by all R2=1 squares)
  R7C3=6 (Implied by all R2=1 squares)
  R7C3<>1 (Implied by all R2=1 squares)
  R7C3<>2 (Implied by all R2=1 squares)
  R7C5=4 (Implied by all R2=1 squares)
  R7C5<>1 (Implied by all R2=1 squares)
  R7C5<>5 (Implied by all R2=1 squares)
  R7C6=3 (Implied by all R2=1 squares)
  R7C6<>4 (Implied by all R1=3 squares)
  R7C6<>9 (Implied by all R2=1 squares)
  R7C7=5 (Implied by all R2=1 squares)
  R7C7<>4 (Implied by all R2=1 squares)
  R7C7<>6 (Implied by all R1=3 squares)
  R7C8=9 (Implied by all R2=1 squares)
  R7C8<>1 (Implied by all R2=1 squares)
  R7C8<>6 (Implied by all R2=1 squares)
  R7C9=1 (Implied by all R2=1 squares)
  R7C9<>4 (Implied by all R2=1 squares)
  R7C9<>6 (Implied by all R2=1 squares)
  R7C9<>9 (Implied by all R2=1 squares)
  R8C2=3 (Implied by all R2=1 squares)
  R8C2<>4 (Implied by all R1=3 squares)
  R8C2<>9 (Implied by all R2=1 squares)
  R8C3=4 (Implied by all R2=1 squares)
  R8C3<>1 (Implied by all R2=1 squares)
  R8C3<>6 (Implied by all R2=1 squares)
  R8C4=5 (Implied by all R2=1 squares)
  R8C4<>1 (Implied by all R2=1 squares)
  R8C4<>3 (Implied by all R1=3 squares)
  R8C4<>9 (Implied by all R2=1 squares)
  R8C5=1 (Implied by all R2=1 squares)
  R8C5<>4 (Implied by all R2=1 squares)
  R8C5<>5 (Implied by all R2=1 squares)
  R8C6=9 (Implied by all R2=1 squares)
  R8C6<>1 (Implied by all R2=1 squares)
  R8C6<>3 (Implied by all R2=1 squares)
  R8C6<>4 (Implied by all R1=3 squares)
  R8C7=6 (Implied by all R2=1 squares)
  R8C7<>4 (Implied by all R2=1 squares)
  R8C7<>5 (Implied by all R2=1 squares)
  R9C1=9 (Implied by all R2=1 squares)
  R9C1<>1 (Implied by all R2=1 squares)
  R9C3=1 (Implied by all R2=1 squares)
  R9C3<>4 (Implied by all R2=1 squares)
  R9C3<>9 (Implied by at least 2 R1<>2 squares)
  R9C7=4 (Implied by all R2=1 squares)
  R9C7<>3 (Implied by all R2=1 squares)
  R9C7<>7 (Implied by all R2=1 squares)
  R9C8=3 (Implied by all R2=1 squares)
  R9C8<>1 (Implied by all R2=1 squares)
  R9C8<>9 (Implied by all R2=1 squares)
  R9C9=7 (Implied by all R2=1 squares)
  R9C9<>1 (Implied by all R2=1 squares)
  R9C9<>3 (Implied by all R2=1 squares)
  R9C9<>4 (Implied by all R2=1 squares)
  R9C9<>9 (Implied by all R2=1 squares)

The following squares can be solved:
   R1C1 = 2
   R1C2 = 1
   R1C3 = 5
   R1C4 = 8
   R1C6 = 6
   R1C9 = 3
   R2C1 = 6
   R2C3 = 8
   R2C4 = 3
   R2C6 = 4
   R2C7 = 2
   R2C8 = 1
   R3C2 = 4
   R3C3 = 9
   R3C4 = 1
   R3C5 = 2
   R3C7 = 8
   R3C9 = 6
   R4C1 = 5
   R4C5 = 3
   R4C6 = 2
   R4C8 = 6
   R4C9 = 9
   R5C4 = 9
   R5C6 = 1
   R5C7 = 7
   R5C8 = 5
   R5C9 = 2
   R6C1 = 1
   R6C2 = 9
   R6C3 = 2
   R6C4 = 6
   R6C5 = 5
   R6C7 = 3
   R6C9 = 4
   R7C2 = 2
   R7C3 = 6
   R7C5 = 4
   R7C6 = 3
   R7C7 = 5
   R7C8 = 9
   R7C9 = 1
   R8C2 = 3
   R8C3 = 4
   R8C4 = 5
   R8C5 = 1
   R8C6 = 9
   R8C7 = 6
   R9C1 = 9
   R9C3 = 1
   R9C7 = 4
   R9C8 = 3
   R9C9 = 7

Tabling was terminated 8 rounds after finding the first reduction or solve, or as soon as at least 5 reductions or solves were found...
Back to top
View user's profile Send private message Visit poster's website AIM Address
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Sat Aug 27, 2005 9:23 am    Post subject: Reply with quote

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
Code:
Susser Buster #2
+-------+-------+-------+
| . . . | . 7 . | 9 4 . |
| . 7 . | . 9 . | . . 5 |
| 3 . . | . . 5 | . 7 . |
+-------+-------+-------+
| . 8 7 | 4 . . | 1 . . |
| 4 6 3 | . 8 . | . . . |
| . . . | . . 7 | . 8 . |
+-------+-------+-------+
| 8 . . | 7 . . | . . . |
| 7 . . | . . . | . 2 8 |
| . 5 . | 2 6 8 | . . . |
+-------+-------+-------+

produced the following colour map
Code:
1a2a5a6a 1b2b       1c2c5b8a   1d3a6b8b 7        1e2d3b6c   9          4        1f2e3c6d   
1g2f6e   7          1h2g4a8c   1i3d6f8d 9        1j2h3e4b6g 2i3f6h8e   1k3g6i   5         
3        1l2j4c9a   1m2k4d8f9b 1n6j8g   1o2l4a   5          2m6k8h     7        1p2n6l     
2o5c9c   8          7          4        2p3h5d   2q3i6m9d   1          3j5e6n9e 2r3k6o9f   
4        6          3          1q5f9g   8        1r2s9h     2t5g7a     5h9i     2u7b9j     
1s2v5i9k 1t2w9l     1u2x5a9m   3l5k6p9n 2y3m5l   7          2z3n4f5m6q 8        2A3o4g6r9o
8        1v2B3p4h9p 1w2C4i6s9q 7        1x3q4j5n 1y3r4k9r   4l5o6t     1z5p6u9s 1A4m6v9t   
7        1B3s4n9u   1C4o6w9v   1D3t5q9w 1E3u4p5r 1F3v4q9x   4r5s6s     2        8         
1G9y     5          1H4s9z     2        6        8          3w4t7b     1I3x9A   1J3y4u7a9B


Supercolouring was unable to find and contradictions but when augmented by verities and veracities it scanned through the implies[u,v] matrix and discovered the following 3 verities:
Code:
Verities scan
Verity: {6,2}=1t2w9l all imply 2k=False
Reduction: 2k=false in {3,3} before=12489 after=1489
Verity: {6,2}=1t2w9l all imply 9q=False
Reduction: 9q=false in {7,3} before=12469 after=1246
Verity: {6,2}=1t2w9l all imply 9v=False
Reduction: 9v=false in {8,3} before=1469 after=146
Verities scan: 265 mS

Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Sun Aug 28, 2005 8:28 am    Post subject: Reply with quote

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

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.


Sorry, I'm just back from holiday and hadn't seen from your posting that you'd got there first. I hadn't intended to steal your thunder.

I haven't tried the negative verities/veracities because I hadn't initially thought they would add value.

One way to deal with the issue that colouring produces very long chains would be to store the length of the chain in the excludes[u,v] matrix. At the moment it's purely boolean and any subsequent deductions are simply discarded. In the quantitive enhancement, you could replace an excludes entry by a subsequent shorter one. If the length of each subchain is stored in the log as an additional tag then it should be possible to retrieve the shortest chain for the transcript when the exclusion is deployed. Matrices are still not very user-friendly when using pencil and paper, though.

Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Sun Aug 28, 2005 12:27 pm    Post subject: Reply with quote

AMcK wrote:
Matrices are still not very user-friendly when using pencil and paper, though.


Making things human-executable was a one of the driving forces behind tabling; it's human-executable (with inhuman patience, Surprised ).

Credit Doug for the verities/veracities insights. I came up with the tabling idea with an eye to finding contradiction chains, but he spotted the extra implications.

The interesting question now is: is there a way to be smart about tabling -- a way to identify features that are likely to generate verities and veracities so one can concentrate on them and not have to table the entire puzzle.
Back to top
View user's profile Send private message Visit poster's website AIM Address
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Sun Aug 28, 2005 11:22 pm    Post subject: Reply with quote

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
Code:
2      3a6a   4      1a3b6b9a   8      5      7      1b3c9b 1c3d6c9c
3e6d7a 1      5      3f6e7b9d   2      3g7c9e 3h8a9f 4      3i6f8b9g
3j6g7d 9      8      1d3k6h7a   1e6i   4      2      5      1f3l6j   
8      3m4a   2      3n4b5a9h   4c5b9i 6      1      3o9j   7       
9      3p4d6k 1g3q6l 1e3r4a8c   7      3s8d   5      6m8e   2       
5      7      1e3t6m 2          1g9k   3u8f9l 3c9m   6o8g   4       
3w6p   2      9      5c6q8h     5a6r   1      4      7      3x5e8i   
1k4f   5      3x6s   4g6t7c8j9n 4h6u9o 7g8k9p 3z8b9q 2      1l3A8m9r
1l4i   8      7      4j5e9s     3      2      6      1n9t   1o5g9u   
Note that (unlike Nick70) my colour alphabets are distinct for each possible - i.e. 1a is NOT identical to 9a.

Contradictions
Code:

[1] 1l [{8,9},{9,1}=1] excludes 1n [{9,8}=1] in box 9
[1] 1b [{1,8}=1] excludes 3c [{1,8},{6,7}=3] in {1,8}
[1] 3o [{4,8}=3] excludes 3m [{4,2}=3] in row 4
[3] 1b [{1,8}=1] excludes 3c [{1,8},{6,7}=3] conjugates 3o [{4,8}=3] excludes 3m [{4,2}=3] so 1b [{1,8}=1] excludes 3m [{4,2}=3]
[1] 4a [{4,2},{5,4}=4] excludes 4c [{4,5}=4] in box 5
[5] 1b [{1,8}=1] excludes 3m [{4,2}=3] conjugates 4a [{4,2},{5,4}=4] excludes 4c [{4,5}=4] so 1b [{1,8}=1] excludes 4c [{4,5}=4]
[1] 4h [{8,5}=4] excludes 4f [{8,1}=4] in row 8
[7] 1b [{1,8}=1] excludes 4c [{4,5}=4] conjugates 4h [{8,5}=4] excludes 4f [{8,1}=4] so 1b [{1,8}=1] excludes 4f [{8,1}=4]
[1] 1k [{8,1}=1] excludes 1l [{8,9},{9,1}=1] in box 7
[9] 1b [{1,8}=1] excludes 4f [{8,1}=4] conjugates 1k [{8,1}=1] excludes 1l [{8,9},{9,1}=1] so 1b [{1,8}=1] excludes 1l [{8,9},{9,1}=1]
[11] 1l [{8,9},{9,1}=1] excludes 1n [{9,8}=1] conjugates 1b [{1,8}=1] excludes 1l [{8,9},{9,1}=1] so 1l [{8,9},{9,1}=1] excludes 1l [{8,9},{9,1}=1]
Contradiction: 1l excludes itself
Reduction: 1l=false in {8,9} before=1389 after=389
Reduction: 1l=false in {9,1} before=14 after=4
1l=False in {9,1} implies 4i=True
4i=True and 4i = 1k implies 1k=True
Forcing: 1k=true {8,1} before=14 after=1
1k=True and 1k conjugates 4f implies 4f=False
4f=False and 4f = 4j implies 4j=False
Reduction: 4j=false in {9,4} before=459 after=59
[1] 3q [{5,3}=3] excludes 3s [{5,6}=3] in row 5
[1] 8d [{5,6}=8] excludes 8e [{5,8}=8] in row 5
[1] 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] in col 3
[1] 6p [{7,1}=6] excludes 3w [{7,1}=3] in {7,1}
[3] 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] conjugates 6p [{7,1}=6] excludes 3w [{7,1}=3] so 6m [{5,8},{6,3}=6] excludes 3w [{7,1}=3]
[5] 8d [{5,6}=8] excludes 8e [{5,8}=8] conjugates 6m [{5,8},{6,3}=6] excludes 3w [{7,1}=3] so 8d [{5,6}=8] excludes 3w [{7,1}=3]
[7] 3q [{5,3}=3] excludes 3s [{5,6}=3] conjugates 8d [{5,6}=8] excludes 3w [{7,1}=3] so 3q [{5,3}=3] excludes 3w [{7,1}=3]
[1] 3x [{7,9},{8,3}=3] excludes 3q [{5,3}=3] in col 3
[9] 3q [{5,3}=3] excludes 3w [{7,1}=3] conjugates 3x [{7,9},{8,3}=3] excludes 3q [{5,3}=3] so 3q [{5,3}=3] excludes 3q [{5,3}=3]
Contradiction: 3q excludes itself
Reduction: 3q=false in {5,3} before=136 after=16
[1] 6b [{1,4}=6] excludes 6i [{3,5}=6] in box 2
[1] 1e [{3,5},{5,4},{6,3}=1] excludes 4a [{4,2},{5,4}=4] in {5,4}
[1] 4d [{5,2}=4] excludes 6k [{5,2}=6] in {5,2}
[3] 1e [{3,5},{5,4},{6,3}=1] excludes 4a [{4,2},{5,4}=4] conjugates 4d [{5,2}=4] excludes 6k [{5,2}=6] so 1e [{3,5},{5,4},{6,3}=1] excludes 6k [{5,2}=6]
[1] 6a [{1,2}=6] excludes 6b [{1,4}=6] in row 1
[5] 1e [{3,5},{5,4},{6,3}=1] excludes 6k [{5,2}=6] conjugates 6a [{1,2}=6] excludes 6b [{1,4}=6] so 1e [{3,5},{5,4},{6,3}=1] excludes 6b [{1,4}=6]
[7] 6b [{1,4}=6] excludes 6i [{3,5}=6] conjugates 1e [{3,5},{5,4},{6,3}=1] excludes 6b [{1,4}=6] so 6b [{1,4}=6] excludes 6b [{1,4}=6]
Contradiction: 6b excludes itself
Reduction: 6b=false in {1,4} before=1369 after=139
[1] 6g [{3,1}=6] excludes 6i [{3,5}=6] in row 3
[1] 1e [{3,5},{5,4},{6,3}=1] excludes 4a [{4,2},{5,4}=4] in {5,4}
[1] 4d [{5,2}=4] excludes 6k [{5,2}=6] in {5,2}
[3] 1e [{3,5},{5,4},{6,3}=1] excludes 4a [{4,2},{5,4}=4] conjugates 4d [{5,2}=4] excludes 6k [{5,2}=6] so 1e [{3,5},{5,4},{6,3}=1] excludes 6k [{5,2}=6]
[1] 6a [{1,2}=6] excludes 6g [{3,1}=6] in box 1
[5] 1e [{3,5},{5,4},{6,3}=1] excludes 6k [{5,2}=6] conjugates 6a [{1,2}=6] excludes 6g [{3,1}=6] so 1e [{3,5},{5,4},{6,3}=1] excludes 6g [{3,1}=6]
[7] 6g [{3,1}=6] excludes 6i [{3,5}=6] conjugates 1e [{3,5},{5,4},{6,3}=1] excludes 6g [{3,1}=6] so 6g [{3,1}=6] excludes 6g [{3,1}=6]
Contradiction: 6g excludes itself
Reduction: 6g=false in {3,1} before=367 after=37
[1] 8c [{5,4}=8] excludes 8e [{5,8}=8] in row 5
[1] 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] in col 3
[1] 6p [{7,1}=6] excludes 3w [{7,1}=3] in {7,1}
[3] 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] conjugates 6p [{7,1}=6] excludes 3w [{7,1}=3] so 6m [{5,8},{6,3}=6] excludes 3w [{7,1}=3]
[5] 8c [{5,4}=8] excludes 8e [{5,8}=8] conjugates 6m [{5,8},{6,3}=6] excludes 3w [{7,1}=3] so 8c [{5,4}=8] excludes 3w [{7,1}=3]
[1] 3x [{7,9},{8,3}=3] excludes 8i [{7,9}=8] in {7,9}
[1] 8h [{7,4}=8] excludes 8c [{5,4}=8] in col 4
[3] 3x [{7,9},{8,3}=3] excludes 8i [{7,9}=8] conjugates 8h [{7,4}=8] excludes 8c [{5,4}=8] so 3x [{7,9},{8,3}=3] excludes 8c [{5,4}=8]
[9] 8c [{5,4}=8] excludes 3w [{7,1}=3] conjugates 3x [{7,9},{8,3}=3] excludes 8c [{5,4}=8] so 8c [{5,4}=8] excludes 8c [{5,4}=8]
Contradiction: 8c excludes itself
Reduction: 8c=false in {5,4} before=1348 after=134
[1] 8k [{8,6}=8] excludes 8f [{6,6}=8] in col 6
[1] 8g [{6,8}=8] excludes 6o [{6,8}=6] in {6,8}
[1] 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] in col 3
[3] 8g [{6,8}=8] excludes 6o [{6,8}=6] conjugates 6m [{5,8},{6,3}=6] excludes 6s [{8,3}=6] so 8g [{6,8}=8] excludes 6s [{8,3}=6]
[1] 6p [{7,1}=6] excludes 3w [{7,1}=3] in {7,1}
[1] 3x [{7,9},{8,3}=3] excludes 8i [{7,9}=8] in {7,9}
[1] 8h [{7,4}=8] excludes 8k [{8,6}=8] in box 8
[3] 3x [{7,9},{8,3}=3] excludes 8i [{7,9}=8] conjugates 8h [{7,4}=8] excludes 8k [{8,6}=8] so 3x [{7,9},{8,3}=3] excludes 8k [{8,6}=8]
[5] 6p [{7,1}=6] excludes 3w [{7,1}=3] conjugates 3x [{7,9},{8,3}=3] excludes 8k [{8,6}=8] so 6p [{7,1}=6] excludes 8k [{8,6}=8]
[9] 8g [{6,8}=8] excludes 6s [{8,3}=6] conjugates 6p [{7,1}=6] excludes 8k [{8,6}=8] so 8g [{6,8}=8] excludes 8k [{8,6}=8]
[11] 8k [{8,6}=8] excludes 8f [{6,6}=8] conjugates 8g [{6,8}=8] excludes 8k [{8,6}=8] so 8k [{8,6}=8] excludes 8k [{8,6}=8]
Contradiction: 8k excludes itself
Reduction: 8k=false in {8,6} before=789 after=79


unVerities
Code:

unVerity: {1,8}=1b3c9b all imply 1o=False
Reduction: 1o=false in {9,9} before=159 after=59
unVerity: {3,5}=1e6i all imply 3n=False
Reduction: 3n=false in {4,4} before=3459 after=459
unVerity: {3,5}=1e6i all imply 9h=False
Reduction: 9h=false in {4,4} before=459 after=45
unVerities: 47 mS


Verities
Code:

Verity: {3,9}=1f3l6j all imply 6h=False
Reduction: 6h=false in {3,4} before=1367 after=137
Verity: {5,2}=3p4d6k all imply 3d=False
Reduction: 3d=false in {1,9} before=1369 after=169
Verity: {5,3}=1g3q6l all imply 4b=False
Reduction: 4b=false in {4,4} before=45 after=5
4b=False in {4,4} implies 5a=True
Forcing: 5a=true {7,5} before=56 after=5
5a=True and 5a conjugates 5b implies 5b=False
Reduction: 5b=false in {4,5} before=459 after=49
5b=False and 5b = 6r implies 6r=False
5a=True and 5a excludes 5c implies 5c=False
Reduction: 5c=false in {7,4} before=568 after=68
5a=True and 5a excludes 5e implies 5e=False
Reduction: 5e=false in {7,9} before=358 after=38
Reduction: 5e=false in {9,4} before=59 after=9
5e=False in {9,4} implies 9s=True
9s=True and 9s excludes 1b implies 1b=False
Reduction: 1b=false in {1,8} before=139 after=39
1b=False and 1b conjugates 1n implies 1n=True
Forcing: 1n=true {9,8} before=19 after=1
1n=True and 1n conjugates 9t implies 9t=False
9s=True and 9s implies 5g implies 5g=True
Forcing: 5g=true {9,9} before=59 after=5
5g=True and 5g excludes 9u implies 9u=False
9s=True and 9s excludes 9a implies 9a=False
Reduction: 9a=false in {1,4} before=139 after=13
9s=True and 9s excludes 9d implies 9d=False
Reduction: 9d=false in {2,4} before=3679 after=367
9s=True and 9s excludes 9n implies 9n=False
Reduction: 9n=false in {8,4} before=46789 after=4678
9s=True and 9s excludes 9o implies 9o=False
Reduction: 9o=false in {8,5} before=469 after=46
9s=True and 9s excludes 9p implies 9p=False
Reduction: 9p=false in {8,6} before=79 after=7
9p=False in {8,6} implies 7g=True
7g=True and 7g conjugates 7c implies 7c=False
Reduction: 7c=false in {2,6} before=379 after=39
Reduction: 7c=false in {8,4} before=4678 after=468
Verity: {5,3}=1g3q6l all imply 5a=True
Verity: {5,3}=1g3q6l all imply 5b=False
Verity: {5,3}=1g3q6l all imply 5c=False
Verity: {5,3}=1g3q6l all imply 5e=False
Verity: {5,3}=1g3q6l all imply 5g=True
Verity: {5,3}=1g3q6l all imply 6r=False
Verity: {5,3}=1g3q6l all imply 9u=False
Verities: 141 mS


Incidentally, with verities and veracities, ultracolouring will now solve most puzzles from start to finish without needing any support from standard reduction methods other than elimination of certainties.

Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
Display posts from previous:   
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Solving sudoku All times are GMT
Goto page 1, 2  Next
Page 1 of 2

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
Sudoku Programmers topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group

Igloo Theme Version 1.0 :: Created By: Andrew Charron