David has good points. A couple of thoughts on what I subjectively count as "trial and error", "brute force" and "assumptive" (with my limited experience), though I'm not making any judgments on what is good or bad. For example, discontinuous nice loop proofs can be considered assumptive trial-and-error techniques, if you first pick a candidate and then look for a loop to eliminate or place it. I don't see how it's any different from simple Nishios which can be replaced with discontinuous loops anyway. They're both also a form of brute force, if the tested candidate is picked randomly (or systematically). If some intelligence is used in picking the candidate, then it's not brute force but it's still t&e.
In other words, whenever you start with what you're trying to prove, it's t&e, and if the target is chosen randomly then it's also a form of brute force. If, on the other hand, a pattern is found first and the eliminations follow from that, then it's not t&e (though searching for the pattern may be). AICs count as such unassumptive patterns in my book -- but only if they're found first and independently of their eliminations. I'm not saying it's necessarily better, however. Using only unassumptive methods may not be a very strategic approach, because there's no guarantee that the unassumed eliminations actually advance the puzzle. Strategically chosen assumptive trials may have a better chance at that. Like I said, I'm not making any judgments. Both approaches have their merits. Even brute force may have its place if nothing else helps, but few probably enjoy it much.
I'll try to explain my point with an example. Since the original poster mentioned SudokuWiki and its approach to Nishio, I took the example from there:
http://www.sudokuwiki.org/Nishio_Forcing_Chains.
- Code: Select all
+-----------------+------------------+--------------+
| 38 389 4 | 2 179 17 | 68 158 56 |
| 26 268 7 | 45 45 16 | 3 18 9 |
| 1 69 5 | 3 69 8 | 2 7 4 |
+-----------------+------------------+--------------+
| 9 4 26 | 16 267 1267 | 5 3 8 |
| 368 1 368 | 9 368 5 | 4 2 7 |
| 7 5 238 | 48 2348 23 | 9 6 1 |
+-----------------+------------------+--------------+
| 4 cF2+6- 1 | 7 256 9 | 68 58 3 |
| 5 38 9 | B168 B1268 123 | 7 4 C26 |
|bE2368 7 b368 |aA58-6 2358 4 | 1 9 D256 |
+-----------------+------------------+--------------+
Stuart's Nishio starts with 6@r9c4 and forms two branches that connect and prove a contradiction at r7c2:
1 (a-c): r9c4=6 => r9c13<>6 => r7c2=6
2 (A-F): r9c4=6 => r8c45<>6 => r8c9=6 => r9c9=2 => r9c1<>2 => r7c2=2 => r7c2<>6
=> contradiction => r9c4 <> 6
That's a logical proof, all right, but the real question is why someone would choose such a useless looking candidate to test. It looks like a totally random or systematic choice, i.e. brute force. Of course it makes even less sense to use Nishio here, when a grouped discontinuous loop is easily available (as Leren seems to have pointed out in the comments, and even Stuart's own solver sees it that way):
Discontinuous Nice Loop Type 1 (Grouped): (6)r9c4 - r9c13 = (6-2)r7c2 = r9c3 - r9c9 = (2-6)r8c9 = r8c45 - (6)r9c4 => -6 r9c4
That's much simpler, but it's just a tactical difference. From a strategic point of view it's no different, as there's still the question of why that particular candidate was chosen to be tested in the first place. It's still t&e and looks like brute force, too.
To me the least t&e and brute force way of finding that elimination is if you happen to see the grouped AIC as a pattern first:
AIC Type 1 (Grouped): (6)r9c13 = (6-2)r7c2 = r9c3 - r9c9 = (2-6)r8c9 = (6)r8c45 => -6 r9c4
Now we know that there must be a 6 in one of those two end nodes and we can eliminate any 6 that sees them both. That is an unassumptive pattern-based elimination. Neither the discontinuous loop or the Nishio is, even though they provide the same proof using essentially the same chain.
