Welcome back!
This proof is a total of three pages. Hopefully, you have already digested the
First Page.
This page is perhaps the most complex page that I have ever placed onto the blog. None of the
steps illustrated below are easy. All of them, however, spring from the general concept of merely
appending bivalue/bilocation chains.
A strong link with 7 appended to AIC with 6s appended to Y Wing style with 47
There are many ways to view this one. Candidate 7 is proven strong at {def3,i2,f8}, all of
which bear down upon f2. In attempt to keep the strong inference sets clear, each is subscripted
below. Also, the notation is somewhat Eureka'd.
 {YWingStyle:(7)def3=_{1}(74)c3=_{2}(4)gh3(4=_{3}7)i2}
 =_{3}(6)i2{(6):ghi1=_{4}a1a4
 =_{5}{XWing at hi49_{56}}}
 =_{6}(67)e9=_{7}(7)f8
Hopefully, the following triangular matrix clearly illustrates that one can view the appendages
in many ways!
def3=7 
c3=7 
  
 
 c3=4  gh3=4     
i2=7   i2=4  i2=6    
   ghi1=6  a1=6   
   i4=6  a4=6  h4=6  
   i9=6   h9=6  e9=6 
f8=7       e9=7 
Please note that above we do not have a pigeonhole matrix, as i2=6 forbids in two dimensions
 along column i
 within box h2
For this reason, I view an elimination such as this one as being more complex than a typical
pigeonhole matrix.
For review, with a pigeonhole matrix, each matrix row is a strong inference set, and each
matrix column, except the first one, are members of a weak inference set. Merely counting truths
proves the first column is a strong set.
With a triangular matrix, the top member of each column, except the first column, is in conflict
with each item below it. Each row is still a strong inference set. Some items must be unfilled:
Each row i is not filled beyond column i+1. If the item in row 1 column 1 is false, then truths must
either cascade down the slope of the triangle or revert back to column 1. Since the triangle ends
bluntly, the last row must revert back to column 1 if no other row has already done so.
Typically, one can find an elimination that requires a triangular matrix representation by
appending combined almost chains. In this case, the intersection of the almost Y wing style with
the 6 almost forbidden by the almost chain on 6s is the key. This intersection occurs at cell i2.
If one could resolve this cell, i2, to one fewer canidate, this puzzle would be significantly
simpler to solve. Unfortunately, I could not find an efficient way to do so.
Also, there is almost always an alternative coloring chain available, which generally makes
almost chains with a single candidate easier to locate. In this case, one could also find:
 (7)f8=(76)e9=(6)hi9(6)g7={(6):g13=g5hi4=a4a1=ghi1}(6)i2={YWS{(47)i2,(4)cgh3,(7)cdef3}}=>f2≠7
Although this elimination uses one more strong inference set, its existence certainly makes
finding the elimination less daunting. Moreover, this alternative can be represented by
a pigeonhole matrix, not the more complex reasoning required for a triangular matrix. I am
very curious as to whether or not this alternative would be viewed as being more simple.
Below, find the alternative chain represented as a pigeonhole matrix:
def3=7 
c3=7 
  
  
 c3=4  gh3=4      
i2=7   i2=4  i2=6     
   ghi1=6  a1=6    
    a4=6  hi4=6   
   g13=6   g5=6  g7=6  
      hi9=6  e9=6 
f8=7        e9=7 
I believe such redundancy on single candidate chains to be axiomatic. Similar redundancies abound
with all types of chains, and also with all types of almost chains. I think searching for such
redundancies is very instructive, as it gives one a feel for where chains must exist. Certainly,
it has served that purpose for me. Perhaps someday I will treat the concept of redundancy in
the proving of sudoku proofs more formally. However, some redundancies exist only because of
uniqueness of solution.
Perhaps I have beat the elimination illustrated above to death. However, I find it to be a very
instructive example. The next elimination has been the subject of some discussion at some sudoku
forums. I do not find it to be any more complex than the previous one. Nevertheless, it introduces,
conceptually, another way to append chains.
Trilocation 7s and 2s chained together with a few appendages
Above, but for the 2 at b6, a chain exists forbidding 5 from f2. Merely appending two
strong inferences to the ends of these chains completes the justification for eliminating 8 from
a2. The two inferences are: (8)b6=a6 and (5=8)f2. Here is one way to write the chain:not the
only one, nor perhaps the best one
 (8)a6=_{1}(82)b6
 =_{2}{(5=_{3}2)e1(2)e4=_{4}(2)d5(2)b5=_{2}(27)b4
 =_{5}{(7):e4=_{5}a4a8=_{6}f8}
 (7=_{7}5)f5}(5=_{8}8)f2
To help find such an elimination, I find it helpful to employ GEMlike logic. Basically, any chain
snippet that one may find proves something. That something may not lead to an elimination, but
it has effectively reduced the set of possible solutions to the puzzle. Simply remember the
chain snippets, and perhaps connect some of them later. Fortunately, any information one uncovers
is true, and this truth must prevail throughout the puzzle solution. I must credit the idea
to Bruno Greco, who introduced it in conjunction to his solution of a tough puzzle at sudoku.com.au
in February of 2006.
Moving Strong Sets
This idea, as used below, basically says that one can prove a new set of strong inferences, and
then use that knowledge as if the proven strong inferences are actually native strong inferences.
As such, it is relatively simple. There are more complex ways to use this concept, but I am not
certain that I have successfully unraveled puzzles that require them.
First, one can establish (7)b4=(8)f2 with either a triangular matrix, or the more concise:
 (7)b4=_{1}{(7):e4=_{1}a4a8=f8}(7=5)f5(5=8)f2
Then one simply applies this proven strong set in either a chain, or the following pigeonhole
matrix:
f2=8 
f2=5 
  

 e1=5  e1=2    
  e4=2  d5=2   
   b5=2  b4=2  b6=2 
f2=8     b4=7  
a6=8      b6=8 
Always, such complex chains can be viewed as accumulated appendages of simple bivalue/bilocation
chains. Please note: I am not advocating that one should employ matrices to find chains or
eliminations. Instead, the study of the matrix representation of any elimination lets one infer
what appendages could have existed without interfering with the validity of the elimination. Then,
one can apply that knowledge to see through seemingly complex groups of inferences with greater
clarity.
After a2≠8, finally another cell solves: a6 = 8 %column. The puzzle is seemingly only
advanced trivially, but in fact, almost all the information for the next elimination has been
considered previously! To illustrate this fact, I have broken the next step down into small pieces.
Almost AIC with candidate 7
Above, three weak links have been added in anticipation of the eventual deduction. One way
to write the chain snippet derived above is:
 (7):i2i1={{Column XWing at ab14}=e4f9=e8}a8
The strong set that is proven is:(7)i1={XWing ab14=e8}
Although it is not my preferred style, without any loss of generality, it has also been
proven that:(7):a8i2. Previously, I would have called this a remote weak link. There is no
logical reason not to also store for future use such proven weak inferences.
Note that the 7s in row 4 are used again in a fashion very similar to the previous step. It
is difficult to not see this chain snippet once one has found the previous step.
Previous chain snippet with candidates 6 & 7
Earlier on this page, we established the information graphed above. I have merely not
graphed the Almost Chain on 6s. There is no need for one to find the relationship again,
as it must still exist! Putting this together with the previous illustration, but for the
4 at i2, clearly a8≠7. However, something has happened in column a that allows one
to easily now connect the dots. This new relationship is clearly indicated by the standard
puzzle markup that I advocate.
The chain with built upon deductions noted in shorthand
Adding to the previous information only the strong cell i2 and two strong by location links in
column a, 7 is forbidden from a8. One could write:
 (3)a8=(34)a5=(4)a2(4)i2
 =_{3}{{(7):f8=e9e4=_{5}ab14}
 =_{6}(7)i1(7=_{3}6)i2{(6):ghi1=a1a4=_{8}hi49}
 =_{9}(67)e9=(7)f8}
 =>(3)a8={(7):f8=a14} => a8≠7
But, one does not have to think it all at once. In fact, one only needs to think as graphed above:
 (3)a8=(34)a5=(4)a2(4)i2={(~7)a8=(7)i1(7=6)i2(7)e9=(7)f8}=>a8≠7
There are of course many equivalent ways to think about this elimination.
Fortunately, after making the elimination graphed above, one can solve column f %cells and i4=5 %box,column & row.
This concludes the second page of this puzzle proof. The hardest and most interesting parts
of this proof are finished. What remains is the clean up! The beginning of that process
can be viewed on the
final page.
Feedback requests
The use of subscripts in an attempt to clarify strong inferences that are partioned and then
considered in pieces seems to obfuscate rather than help. If this is your experience in reading this
page, kindly let me know. Perhaps also suggest a better alternative! Thanks!
Also, if I am abusing Eureka notation, it is still too new for me. Any pointers on its correct
usage would be helpful. Of course, I may well be a hopeless case in this regard!