Inference Types
Alternating Inference Chains (AICs) just use weak and strong inferences to link a series of Boolean (true or false) arguments. As the name implies, within the chain these inferences must strictly alternate between weak and strong:
Weak inferences: Two Booleans cannot both be true (at least one must be false, but possibly both are). . . Linking symbol: -
Strong inferences: Two Booleans cannot both be false (at least one must be true, but possibly both are). . Linking symbol: =
Conjugate inferences: Two Booleans one of which must be true and the other false. . Linking symbol: Not Standardised ( ^ is one option)
A large number of inferences used in logic chains are 'conjugate' where the linked Booleans must contain one truth. Typical cases are a 'bivalue' cell holding two digits and a 'bilocal' digit that can only occupy two cells in a house. Conjugate inferences are therefore both weak and strong, but within AICs, they can only be used in one way or the other and must be notated accordingly using the standard '-' and '=" symbols.
Using this map of the cells holding digit 5 as a candidate in the top tier of boxes:
- Code: Select all
*-------*-------*-------*
r1 | . . 5 | . 5 . | . . 5 |
r2 | 5 . . | 5 5 5 | . 5 . |
r3 | 5 . 5 | . 5 . | . . . |
*-------*-------*-------*
Strong link: (5)r123c5 = (5)r2c456. At least one of these must be true and possibly both are (when (5)r2c5 is true).
Conjugate link: (5)r1c9 ^ (5)r2c8. One must be true and the other false, can be used either as a weak '-' or strong "=" link in an AIC.
A common misconception is that all strong inferences can also be used as weak, but the example above disproves that. Another more common case is for Almost Naked Sets:
- Code: Select all
*------------*
| 245 45 345 |
*------------*
AIC Logic
This simple example of an XY-Wing pattern illustrates how an alternating sequence of weak and strong links works:
- Code: Select all
*----------*----------*----------*
r1 | 12 . . | 23 * * | . . . | ./* = Any digits
r2 | . . . | . . . | . . . | * = (1) May be eliminated
r3 | * * * | . . 13 | . . . |
*----------*----------*----------*
In r1c1 when (1) is false (2) must be true (strong link). In r1c4 (2) must now be false (weak link) so (3) must be true, and in r3c6 (3) must be false and (1) true.
So when (1)r1c1 is false (1)r3c6 must be true.
Now working backwards along the chain, the same process in reverse shows that when (1)r3c6 is false, (1)r1c1 must be true.
Together these show that (1)r1c1 and (1)r3c6 are strongly linked (they both cannot be false) and could be summarised as (1)r1c1 =[...]= (1)r3c6.
Any candidate that is weakly linked to both these terms must therefore be false.
Note, it does not prove that when one is true the other is false. For example, if (2)r1c9 were true, it would be false in both r1c1 and r1c4 and (1) would have to be true in both the end cells of the chain.
This logic can be applied to any AIC to prove that two end Booleans that are reached on strong links are strongly linked. Similarly, two end Booleans reached on weak links are weakly linked.
Booleans that occupy odd and even positions in the chain will automatically have the same type of link to the central body of the chain. This means that the chain segment between any odd/even pair is reveals the relationship between them. Provided the chain is valid, these relationships are permanent and will exist in the final solution.
Elimination Rules
1. When an AIC starts and ends with strong links, any candidate weakly linked to both end nodes is false and can be eliminated.
2. When an AIC starts and ends with weak links to a particular candidate, it proves that this candidate is false and can be eliminated.
Basic Construction Rules
1. The links must strictly alternate between being weak and strong.
2. The linked conditions must be truly Boolean that can only be true or false and must be stand-alone, independent of any other links in the chain.
3. Each link in the chain must operate in both directions whatever way the digits are distributed in the specified cells.
Note, there are no restrictions regarding how many times a cell can be visited in a chain's path.
These construction rules guarantee that the chains can be read forwards and backwards and are therefore 'bidirectional'. It is therefore a good discipline to check
a) That ignoring any other terms in the chain, under no circumstances it is possible for both terms to be true for a weak link, or both false for a strong one.
b) That the link types always alternate
The AIC Closed Loop Theorem
An AIC closed loop is formed when the first and last nodes in a chain can be linked using an inference of the correct type. (This means a closed loop will always have even numbers of terms and links.)
- Code: Select all
+----------+----------+
r1 | 12 . . | 23 . . |
r2 | . . . | . . . |
r3 | . . 14 | . . 34 |
+----------+----------+
From the end terms of the chain, it can be seen that (1) must be true at r1c1 or r3c3. This excludes all the remaining (1)s in box 1 which makes the weak link from the last term back to the first one conjugate. But this loop can be broken at any weak inference along its length to prove that every link is conjugate. Therefore, either all the odd terms are true or all the even ones are. This also allows eliminations to be made using odd and even assassin terms 'across the loop' when they are not adjacent.
AICs vs Forcing Chains
Once the concept of how AICs work is understood it is possible to construct a chain without making any assumptions at all. For a chain to be bidirectional it is only necessary to ensure that the construction rules are correctly followed without having to consider which term in the original link is true. The elimination rules then follow automatically.
In comparison, a forcing chain, which can only be followed in one direction, will depend on the opening assumption and will only be able to prove whether that assumption is false because it would result in a contradiction.
These bald statements suggest that following implication chains can be done robotically de-humanising the way eliminations are found, but in practice a solver must consider the possible cases that can arise to verify each link in the chain is valid. Looked on in that way, a bidirectional chain follows two cases while a forcing chain only follows one. The fact is that bidirectional chains are generally more productive than forcing chains because they have a greater chance of revealing eliminations.
Another benefit from using AICs is that the relationships they find are long lasting and will persist through to the final solution, whereas the information from a forcing chain is conditional on the opening assumption being true and becomes worthless if it is found to be wrong.
Branched Chains and Networks
In logical terms the links in a linear AIC are alternately OR (at least one) and NAND (NOT AND, one at most) logical operators. When a chain is allowed to branch this introduces AND (both together) and NOR (neither) operators. Taken further, when several branches are followed simultaneously, it means that a network approach is being used.
When branching is used the question arises of whether the path can be followed both forwards and backwards, it is assumptive or not? Not surprisingly, here there are considerable differences of opinion about the acceptability of the various approaches. However there is a general consensus that it is acceptable to use recognisable, pre-analysed, patterns.
Patterns as Boolean Terms
An experienced eye can often recognise potential patterns in the distribution of candidates that provide known eliminations when they are formed. Some of these patterns, such as Wings, can be proved using AICs, while others, such as Fish and Unique Rectangles, need more complex analysis (which may involve comparing multiple possible outcomes).
It is very difficult to formulate a precise definition of a pattern, but one essential is that they should be capable of being identified without having to track any logic streams but just by counting and checking the defined elements exist in a qualifying distribution.
Patterns can be considered as Booleans that will be true when the pattern is formed and false when it is disrupted. There are therefore 'derived' inferences between a potential pattern and the set of candidates that would disrupt it that can be used in inference chains. These allow candidates that cannot be true in either case to be eliminated. A number of pre-analysed patterns have been defined that can be used in this way and they are described in the various solving guides. These allow a reader who is unfamiliar with a particular pattern to look it up when it is encountered.
TAGdpbAIC_Basics
[Edit 10th & 14 Aug 2017] Corrections - typos & clarifications - identified by Gordon Fick (thanks).
