Top95: Our common benchmark?

Bob Hanson · Posted: Tue Nov 08, 2005 6:35 pm Post subject:

I apologize again for the long URL!!!!

Lummox JR · Posted: Wed Nov 09, 2005 11:19 pm Post subject:

Bob Hanson · Posted: Wed Nov 09, 2005 11:50 pm Post subject:

I'm sorry about the reverse logic idea. It isn't bifurcation, but it is equivalent to it -- that's what I learned from Nick.

In short, what I learned from Sudoku Assistant is that Nick's "forward bifurcation" was unnecessary. If he had instead picked a slightly different node -- one that was in the same chain as the one he did choose, then he could have come up with the EXACT same implication in a forward, no-bifurcation sense.

It's a little complicated, for sure.

I think it goes like this:

normal forcing logic, without bifurcation or application of the {?FFFF} --> {TFFFF} trick gets stuck.

One way around this is via bifurcation. (If a or b or c, then .... X can be eliminated.) Nick called this a verity or proof, I think., but it's tricky, because he expressed it as "X cannot be eliminated" but that was just because he HAPPENED to pick a conjugate pair.

Ey. I don't know if I'm explaining this well. Bear with me.

Another way around this is via normal forcing logic with application of the {?FFFF} --> {TFFFF} trick. (All except one is false in a group allows us to set the last one TRUE and continue with implications). No bifurcation is necessary. The result is a proof that the hypothesis "A is TRUE" is false, allowing us to eliminate A.

These two methods are equivalent.

BUT, it turns out that you can go the other way -- The sort of reverse logic that Nick was doing -- his innovation to build the table "backward" back to his bifurcation proved that the bifurcation worked.

I -- unfortunately, perhaps -- used that reverse tabling for my first analysis, and it worked. Voile! All Sudokus attempted solved. But it worked only when I stated the hypothesis "X can be eliminated", not "X cannot be eliminated."

In the end, I implemented the logic both ways and showed the bifurcation is simply not necessary -- picking the correct hypothesis on the correct set of nodes you can use standard, forward logic "disproof" at Sudoku Assistant -- and it all works just fine. You just have to be sure to apply the {?FFFFF} --> {TFFFFF} trick.

Next step, if this still doesn't make any sense is for me to show the forward -- normal -- table that corresponds to Nick's reverse one, with no bifurcation and the same result. I'm happy to do that. Should I?
_________________
Bob Hanson
Professor of Chemistry
St. Olaf College
Northfield, MN
http://www.stolaf.edu/people/hansonr

Lummox JR · Posted: Thu Nov 10, 2005 12:48 am Post subject:

I guess where I'm losing you is that it looks like both techniques are trying to prove the same thing. That is, you're trying to prove the hypothesis that a certain value is false, and that's where you put the a. I can understand "forward" in terms of a placement proving/disproving other placements, or contradicting itself, and "reverse" in terms of the bifurcating chains technique starting with the end result and trying to prove that from other a set of choices which must be true.

I'm not sure I get the whole {?FFFF} -> {TFFFF} thing, since that's not how Nick70's bifurcating chains work. Instead, it's {F????}->{FTTTT} and {?TTTT}->{FTTTT}. "Forward", if I understand the way you're using it, would indeed be {?FFFF}->{TFFFF} and {T????}->{TFFFF}, but the graph you posted doesn't show that. (You did mention that one was reverse, though, so maybe I'm basing too much of this off your graph.)

And I still don't see how your method is avoiding bifurcation. The graph you built is still doing just that, only at a much lesser degree by not following up fully at each step. I'm also not sure I see how a forward version (checking a placement to see what it reveals) could show more than a reverse version (looking for which placements prove a thesis).

Bob Hanson · Posted: Thu Nov 10, 2005 1:02 am Post subject:

Please understand that I have stopped using this reverse business myself, in favor of the forward, normal logic. It took me some time to realize the equivalence, and the connection to bifurcation. But now that I see that you can use FORWARD--normal--logic to avoid bifurcation just as well as reverse, I see no particular point in going that way. The table that initiated this discussion was "reverse" -- providing a proof that "X can be eliminated". Instead, I now think it much more sensible and understandable to do it the normal way and just not do the bifurcation, since it APPEARS to not be necessary.

Maybe we should just forget about that table and start with a new one.

Take a look at this one:

http://www.stolaf.edu/people/hansonr/sudoku/tableexample.htm

This is, I think, the same Sudoku that Nick was introducing. The logic trail shows how the hypothesis "Chain 1(1) cannot be eliminated."

results in:

g: found that the hypothesis leads to both states for r4c5#1.
The hypothesis is disproven.

This is essentially the same as what Nick was trying to do, with no bifurcation.
_________________
Bob Hanson
Professor of Chemistry
St. Olaf College
Northfield, MN
http://www.stolaf.edu/people/hansonr

Lummox JR · Posted: Thu Nov 10, 2005 1:59 am Post subject:

Well, I definitely don't get that table. I see the forward aspect of it, but I don't understand this:

Bob Hanson · Posted: Thu Nov 10, 2005 4:05 am Post subject:

Sorry. I saw that and changed the bottom but not the top. It should read:

g: found that the hypothesis leads to both states for r4c5#1

What has happened is that F has set both r4c3#1 and r4c5#1 TRUE.
However, these are conjugate pairs. One must be false and one true.
In the final step, g, we try to "set" r4c5#1 FALSE, because if r4c3#1 is TRUE, then it must be FALSE. But we have just set it TRUE, so it can't be both TRUE and FALSE, and the hypothesis, "Chain 1(1) cannot be eliminated" is FALSE. Chain 1(1) CAN be eliminated. Chain 1 in this case is r6c1#2 and r4c1#2. The hypothesis was that r4c1#2 could NOT be eliminated -- A. But that was proven false, so r4c1#2 CAN be eliminated. And the solution progresses.

Yes, that's right. We could have stopped at Step F. It's a bit more expensive to check for all-TRUE rows than simply a node conflict, so that's what the algorithm is doing here. It checks the all-TRUEness only once a cycle, and it's already done that in this cycle.

Since it's the last step, it probably doesn't pay to make this more efficient. But, yes, one could stop just before this as well, at F.

Anyway, I hope you agree -- no bifurcation necessary. Just straight A --> a --> B --> b ---> C ---> etc.
_________________
Bob Hanson
Professor of Chemistry
St. Olaf College
Northfield, MN
http://www.stolaf.edu/people/hansonr

Lummox JR · Posted: Thu Nov 10, 2005 4:51 am Post subject:

rkral · Posted: Thu Nov 10, 2005 12:14 pm Post subject:

Lummox JR · Posted: Thu Nov 10, 2005 8:28 pm Post subject:

It's not conjugates that matter in bifurcating chains, but rather when placing false values you must find a constraint that's filled with all true values except for one unfilled placement. Every other 2 in row 2 is marked true: B, C, and D. The only one left is r2c5=2. If that is false, one of the others is true, and if one of those is true then the hypothesis is true.

Bob Hanson · Posted: Fri Nov 11, 2005 4:07 pm Post subject:

Lummox JR:

That's a fine idea -- even if it doesn't catch the {TTT}, at least check for it just before exiting and report it that way. It's the last step--we know there is an elimination, just reporting it slightly differently. OK, that's implemented that way now in http://www.stolaf.edu/people/hansonr/sudoku

bifurcation: My impressioni was that "bifurcation" refers to the parallel checking of multiple possibilities:

If X then either

Y, in which case......

or

Z, in which case......

To me, that's fundamentally different in concept than simply going

If X then ....

then .....

then .....

Which is all we are (or at least I am) doing here. One can show that, in the end, the two arrive at identical results, provided one includes recognition that {?FFFFF} --> {TFFFFF} in "nonbifurcating" logical analysis.

I guess if you want to say that adding that consideration amounts to "bifurcation" I guess you can. But there are still two fundamentally different ways --programming wise-- of getting to that same conclusion. One that (I think, maybe?) requires some sort of keeping of parallel records and cross-checking, and one that just follows the logical consequences directly. Maybe I misuderstand how one would implement "bifurcation". I don't know.

rkral: right, with this "reverse logic" technique, it's that last "All TRUE except 1 unknown forces the last FALSE".

Again, you don't need to do this sort of reverse logic unless you really like it. (I've decided it drives me nuts.) The same conclusion could be arrived at using simple "normal forcing" logic simply by initially placing an A at r2c3#9 and following the logic in the standard implicating way. (Since r2c3 is 9, it can't be 2, 3, or 4.) Then "B" would become "a", "b" would become "B", "C" would become "b", etc. until, in the end, row 2#2 would be "all false except for r2c5" and we could place a "D" there and continue. In the end, if we arrive at a logical inconsistency, then you say, "Oh, OK then, in that case I WILL eliminated r2c3#9."

If that didn't make any sense, or you are not convinced, try Sudoku Assistant, the "Proof" sample. Solve it first using "disproof" (the normal forcing logic route) and then solve it also using the "proof" (as you and Lummox JR are doing, above) method. Then compare the logic trails.

They will be nearly identical.
_________________
Bob Hanson
Professor of Chemistry
St. Olaf College
Northfield, MN
http://www.stolaf.edu/people/hansonr

Lummox JR · Posted: Fri Nov 11, 2005 7:08 pm Post subject:

Lummox JR · Posted: Fri Nov 11, 2005 7:27 pm Post subject:

You know, in just ruminating over my last post, I realized you could probably amp up this technique considerably by combining both the forward and reverse methods. Say I want to prove a placement (A) true, and also show 1) what implies it, and 2) what it implies.

If you go after 2 first, of course, you'll be able to find out if A is invalid.

If A is invalid by the forward method, then the reverse will tell you which other placements you could eliminate as a result. Any marker, true or false, that shows up in that analysis is wrong. When you think about it this is huge. You can eliminate all positive markers, and place any negative ones. You also know at this point that two negatives will not coexist, or a constraint will not be all positive, because those would have proved A true which it is not.

If A is plausible by the forward method (since you can't confirm it's true that way, even if you fill the grid), you can use reverse to confirm its truth. That will tell you if 1) it's possible to prove A true, or else 2) if any placements within the same constraint (i.e., same digit same house, or different digit same cell) imply A, thus contradicting themselves. I thought it might also be possible to say that if the same placement implies A while true but is proved false by A, or vice-versa, it must be wrong; but I can find no logic to back that up.

This is also easy to do with standard bifurcating chains (reverse order) alone. That is, if you hypothesize a and prove it, that placement is false. Set that to A and do the analysis again, but eliminate any true markers and place the false markers. So no matter what results you pull out of bifurcating chains, you can say this: If a placement is false, any placement or elimination that implied it is wrong.

Bob Hanson · Posted: Fri Nov 11, 2005 8:51 pm Post subject:

rkral · Posted: Sat Nov 12, 2005 4:49 pm Post subject: