The New Sudoku Players' Forum

[nazaz]

Theorem 1: Let S be a theory in FOL (e.g. the theory consisting of the 4 basic Sudoku axioms plus the givens of a puzzle P). Let T be a theorem of S, i.e. any formula that can be deduced from the axioms of T (typo: you meant S) according to the principles of FOL (e.g. the assertion of a candidate as a value for some cell: rc=n). Then any formula F derivable from S+T is derivable from S.
The proof is obvious: take any proof of F using T and replace any mention of T in it by the proof of T in S. This gives a proof of F that doesn't explicitly use T.

Yes.

Corollary (formal version): any candidate asserted at any step of a resolution of a puzzle (based on the principles of FOL) can be used in further steps exactly as if it was a given.

Not necessarily.

You can choose how you encode Sudoku as a FOL, in particular which predicates you'll use. It is entirely reasonable to represent the givens by IsGiven(n,r,c) predicates, and to assert the initial candidates by means of a formula like ∀n ∀r ∀c (IsGiven(n,r,c)→IsCandidate(n,r,c)). A uniqueness rule will have expressions like IsCandidate(1,2,3)∧¬IsGiven(1,2,3) within it. To use candidate 1r2c3 (for example) "as if it were a given", the uniqueness rule would become IsGiven(1,2,3)∧¬IsGiven(1,2,3), aborting the solving path with a contradiction. But in a puzzle with a non-zero number of solutions, aborting with a contradiction should be impossible.

The problem in the corollary stems from a lack of precision about the word, "given". When it refers to the IsGiven predicates in a FOL as described in the previous paragraph, the corollary is false. When it refers to the IsCandidate predicates supplied as premises in a FOL that lacks IsGiven predicates, the corollary is true. The specific encoding of the sudoku puzzle as a FOL really matters.

[denis_berthier]

Corollary (formal version): any candidate asserted at any step of a resolution of a puzzle (based on the principles of FOL) can be used in further steps exactly as if it was a given.

Not necessarily.

Necessarily! Contrary to what you suggest, the word "given" is perfectly clear here; it means a given in the usual sense.
Adding a predicate given(x) doesn't change the corollary. It may allow you to write rules that try to make a difference, but it doesn't change the fact that a given (in the usual sense) is and can be used as a decided value.

Now, the real question is, why one would want to use predicates and to write rules that intend to go against the natural workings of FOL? Especially when no example has ever been proposed showing it would be useful?

It is entirely reasonable to represent the givens by IsGiven(n,r,c) predicates,...

Do you think nobody has suggested this before?

to assert the initial candidates by means of a formula like ∀n ∀r ∀c (IsGiven(n,r,c)→IsCandidate(n,r,c)).

Too complicated. During initialisation, one would assert both given(x) and decided-value(x) for the givens, and candidate(x) for the rest.

the uniqueness rule would become IsGiven(1,2,3)∧¬IsGiven(1,2,3), aborting the solving path with a contradiction

This is devoid of any meaning. Predicate given(x) can only be asserted during initialisation. given(x) ∧ ¬given(x) can never appear in a resolution path.

.

[denis_berthier]

.
I think the following result was missing in this thread (but I'm too lazy to re-read everything in order to check this).

Theorem:
Suppose that (according to definition 1 in the first post of this thread), at some point in a resolution path, one has the following UR1.1 pattern of four cells spanning two rows (say r1 r2), two columns (say c1 c4) and two blocks (say b1 b2):

Code: Select all

1  .  .  |  2  .  .
2  .  .  |  13 .  .

In addition, suppose the 3 decided cells with 1 or 2 were not given.
Then, at the start there was a non-degenerate UR1 (with an undefined number of guardians in addition to the 3).

Code: Select all

12 .  .  |  21  .  .
21 .  .  |  123 .  .

Proof: I'll show only that r1c1 must have 2 as a candidate at the start.
If this wasn't true, it would mean that 2 appears as a given in either in r1, c1 or b1. Obviously impossible.

Said otherwise, unless its decided cells are given, UR1.1 can only appear as a degenerated form of a previous UR1.

Consequence for SudoRules: UR1.1 can be dealt with without any additional rule (wrt UR1), just by applying the generic ultra-persistency rules for ORk-relations.
.

[nazaz]

Corollary (intuitive version 1): FOL cannot make any difference between a given and a value derived from the givens..

I've explained above that it can. Just introduce the IsGiven predicate. It's a wild, wild claim that FOL is so restrictive a framework that it can't be used to model such a trivial piece of information.

Let S be your Sudoku theory, for a particular puzzle, that lacks the IsGiven predicate. Let S' = S + G + U where G consists solely of the IsGiven(n,r,c) predicates for the puzzle's givens, n@(r,c), and U contains formulae that depend upon the IsGiven predicate, e.g. UR-based deductions. Any formula that S can derive, S' can too, obviously. Yet S' retains knowledge of what was a given, contrary to your "intuitive version 1". The formulae in U are available to be used in S', not but in S. It makes no sense to say that a candidate n@(r,c) in S' for which IsGiven(n,r,c) does not hold can be used "exactly as if it were a given", i.e. as if IsGiven(n,r,c) were proven, by a formula in U that makes explicit use of the IsGiven predicate.

[denis_berthier]

Corollary (intuitive version 1): FOL cannot make any difference between a given and a value derived from the givens..

I've explained above that it can. Just introduce the IsGiven predicate. It's a wild, wild claim that FOL is so restrictive a framework that it can't be used to model such a trivial piece of information.

As I've never said it can't do it in your modified sense, there's nothing to reply.

[nazaz]

Proof: I'll show only that r1c1 must have 2 as a candidate at the start.
...

Don't you also need to show that 3,4,5,6,7,8 and 9 are not initial candidates in that cell? Otherwise, your initial candidates could have non-{1,2} values in cells other than the bottom right. I'm not sure if you're allowing that when you say "with an undefined number of guardians in addition to the 3".

It seems perfectly plausible that a distinct rule for UR1.1 isn't needed in addition to UR1. But you seem to be saying something much stronger, that any UR1.1 elimination (at any point in the resolution path) can be handled instead by an equivalent UR1, on the same cells, right at the start. Do you mean that? "At the start" as in immediately after removal of all candidates that see the givens?

[denis_berthier]

Proof: I'll show only that r1c1 must have 2 as a candidate at the start.
...

Don't you also need to show that 3,4,5,6,7,8 and 9 are not initial candidates in that cell? Otherwise, your initial candidates could have non-{1,2} values in cells other than the bottom right. I'm not sure if you're allowing that when you say "with an undefined number of guardians in addition to the 3".

I do. A guardian is any candidate other than those of the deadly pattern, in a cell of the deadly pattern

It seems perfectly plausible that a distinct rule for UR1.1 isn't needed in addition to UR1. But you seem to be saying something much stronger, that any UR1.1 elimination (at any point in the resolution path) can be handled instead by an equivalent UR1, on the same cells, right at the start. Do you mean that? "At the start" as in immediately after removal of all candidates that see the givens?

At the start, the UR1 is detected and an ORk-relation between the guardians is asserted. In and of itself, if there's more than one guardian, it allows nothing. But as resolution proceeds along the path where the UR1.1 would be met, the UR1 pattern degenerates, some of the guardians disappear and the ORk-relation looses some of its terms but it's still there (modified - that's ultra-persistency of ORk-relations). At this point, you don't have to identify any UR1.1, the remaining ORk-relation does its job.

But there's also a bonus. You don't have to wait until you reach the UR1.1 situation. You can use the ORk-relation earlier by applying the generic ORk-chains.
.

[denis_berthier]

.
Just thinking to myself.
Why did it take so long to reach the final conclusion in my 3rd post above?
One reason is, I've never been very interested in uniqueness and I didn't invest much time thinking of it.

However, there are three more points worth mentioning:
- the idea that the UR1.1 might always be preceded by a UR1 has been formulated long ago but never proven. And there's a good reason for the latter: it may not be true. In order to reach a provable formulation, one needs to allow more guardians in the UR1 (in which case the proof becomes trivial).
- once proven, the result doesn't immediately lead to any useful conclusion: this step further requires the ORk-relation and ultra-persistency ideas. I developed these ideas as a result of analysing the tridagon pattern and developing generic ORk-chains applicable to it. Later I applied this machinery to more general impossible patterns, and then (only recently) to the deadly patterns.
- the reason why a UR1.1 may not be preceded by a mere UR1 is, the UR1 with additional guardians present at the start may completely degenerate before loosing its additional guardians; only the ORk-relation remains true.
.

[nazaz]

UR1.1 may not be preceded by a mere UR1

I ran some tests using a modified version of PGExplainer that asserts the single guardian, x, whenever it finds a 12-12-12-12x UR pattern or a degeneration thereof. The call into the UR4 code is queued up at the end of the directHintProducers ArrayList in Sudoku.java. When run on the 17-clue collection, it hits 771 times in total, affecting 725 of the 49158 puzzles.

Since it runs after the NakedSingles code, there are only three possible UR shapes it could act upon. Of the 771 hits, there were

• 686 of type 12-12-12-12x,
• 19 of type 12-12-12-1x,
• 66 of type 1-2-2-1x.

So, yes, UR1.1 can crop up without previously being clobbered by a vanilla UR1 elimination.

[denis_berthier]

.
Good to have examples. Now, you could check that they all have a UR1 + guardians at the start and that it doesn't matter not to have a standard UR1.
.

[nazaz]

Well it's obvious that both UR digits will appear in all four cells at the start; you already gave an elementary proof. As for the other part of the check you requested: I'm sure that in most cases there'll be loads of messy additional digits in those same cells. I'll confirm if I have time.

[denis_berthier]

Well it's obvious that both UR digits will appear in all four cells at the start; you already gave an elementary proof. As for the other part of the check you requested: I'm sure that in most cases there'll be loads of messy additional digits in those same cells. I'll confirm if I have time.

Additional candidates, sure.
Messy, I wouldn't say so. They allow ORk-chains to produce earlier eliminations.
.

[nazaz]

Your first post could do with some tidying-up.

After some tweaking, I also found a puzzle directly contradicting the UR 1.1 rule as I stated it

Given that you are working with your personal non-standard definition of UR1.1 here, ignoring the standard requirement for givens, the example has no relevance to the actual UR1.1 technique. You should make that clearer, e.g. calling your variant fake-UR1.1.

Corollary (intuitive version 1): FOL cannot make any difference between a given and a value derived from the givens

Since you already rowed-back on that overgeneralised claim here, you might want to edit your corollaries to clarify that they apply only to Sudoku FOL models constructed without an IsGiven(n,r,c) predicate or similar.

As a second result, any tentative formulation of an UR1.1 rule can only be what I first stated, without any mention of unclued cells.

There's no such consequence for the UR1.1 rule, only for the FOL model that describes it. Any formulation of UR1.1 in a FOL model of Sudoku requires something, like an IsGiven(n,r,c) predicate, to equip the model with the expressive power required to describe a unique rectangle.

[denis_berthier]

1.

After some tweaking, I also found a puzzle directly contradicting the UR 1.1 rule as I stated it

Given that you are working with your personal non-standard definition of UR1.1 here, ignoring the standard requirement for givens, the example has no relevance to the actual UR1.1 technique. You should make that clearer, e.g. calling your variant fake-UR1.1.

As my example conforms to my definition, I don't see any point here.

2;

Corollary (intuitive version 1): FOL cannot make any difference between a given and a value derived from the givens

Since you already rowed-back on that overgeneralised claim here, you might want to edit your corollaries to clarify that they apply only to Sudoku FOL models constructed without an IsGiven(n,r,c) predicate or similar.

Once more, you failed to understand what I wrote. This corollary applies to ANY Sudoku model in which "given" really means "given". You can always introduce an isGiven predicate (a name that sounds more Java-like than FOL-like). But as you don't allow it to be used for any inferencing, you could as well call it isCupOfTea: it doesn't in any way represent the role of a given in Sudoku.
Think of it that way: FOL is not smart enough to understand natural language. But FOL was precisely built for that purpose.
In short, you're confusing the natural meaning of "given" which I use in my informal corollary (as I clearly stated it), and a formal predicate to which you fail to give any meaning.

3.

As a second result, any tentative formulation of an UR1.1 rule can only be what I first stated, without any mention of unclued cells.

There's no such consequence for the UR1.1 rule, only for the FOL model that describes it. Any formulation of UR1.1 in a FOL model of Sudoku requires something, like an IsGiven(n,r,c) predicate, to equip the model with the expressive power required to describe a unique rectangle.

See point 2.

Anyway, the only interesting result of all this thread is what I stated before. I repeat it here, so that it isn't clogged with irrelevant objections.
Theorem:
Suppose that (according to definition 1 in the first post of this thread), at some point in a resolution path, one has the following UR1.1 pattern of four cells spanning two rows (say r1 r2), two columns (say c1 c4) and two blocks (say b1 b2):

Code: Select all

1  .  .  |  2  .  .
2  .  .  |  13 .  .

In addition, suppose the 3 decided cells with 1 or 2 were not given.
Then, at the start there was a non-degenerate UR1 (with an undefined number of guardians in addition to the 3).

Code: Select all

12 .  .  |  21  .  .
21 .  .  |  123 .  .

Proof: I'll show only that r1c1 must have 2 as a candidate at the start.
If this wasn't true, it would mean that 2 appears as a given in either in r1, c1 or b1. Obviously impossible.

Said otherwise, unless its decided cells are given, UR1.1 can only appear as a degenerated form of a previous UR1.


[Edit]: One can also consider this result as a reality check. You can try as hard as you can to go against the natural workings of FOL; at some point, it will catch up with you.

.