The New Sudoku Players' Forum

[champagne]

Now, if you are able to express "rc=n is not a given" in logic, we're all ears.

This UR1.1 pattern recognition can be a problem in your solver, it would not be in mine.

As usual, you're mixing everything. McGuire's proof is based on unavoidable sets, not on expressing non-givens in logic.

I know very well the logic used in both cases. (16 clues or 17 clues search code)
The main filter is to check whether a given puzzle hit all known unavoidable sets. This is exactly the logic needed here. Again, it can be hard to add it to your frame, but this is another point.

[denis_berthier]

Now, if you are able to express "rc=n is not a given" in logic, we're all ears.

This UR1.1 pattern recognition can be a problem in your solver, it would not be in mine.

It is not a problem in my solver.
And the problem is not whether it can be expressed in a solver, it's whether it can be expressed in logic.

As usual, you're mixing everything. McGuire's proof is based on unavoidable sets, not on expressing non-givens in logic.

I know very well the logic used in both cases. (16 clues or 17 clues search code)
The main filter is to check whether a given puzzle hit all known unavoidable sets. This is exactly the logic needed here.

Once more, empty claims. And no answer to the real question:

how do you express "rc=n is not a given" in logic?

I'll help you (or anyone wanting to tackle this question).
In logic, everything is expressed in predicates and axioms.
So, you have to start from some ternary predicate "not-given(n, r, c)" with the intended meaning that rc=n is not a given. But introducing a predicate with some suggestive name is of little help; at this point, you could as well call it "hamburger(n, r, c)", that'd make no difference.
You have to write axioms for it and these axioms have to confer it the intended meaning.
That's where problems begin. This is impossible in any consistent logic. But if you want to try, that'll be a good exercise in basic logic.

[eleven]

If I am not mistaken, the debates in this thread are about possibility of "UR 1.1" rule's usage in "rigorous" approach. For me, "UR 1.1" rule cannot be used in rigorous approach (similar to other uniqness methods).

You are mistaken. See this first post about the topic from 2006.

[Leren]

denis_berthier wrote : how do you express "rc=n is not a given" in logic?

Well, I just love a challenge, and I' d rather get shot down in flames as a dunce than not try my hand at this one.

I'll assume for this first try that you can limit yourself to valid Sudoku grids which, I believe, are about S = 6,670,903,752,021,072,936,960 in number.

You may want to establish an agreed order for these, (for example, minlex order) so you can assign an integer to each grid. So, the set of all Sudoku grids can be identified with the set of integers 1 to S.

So, if you want to establish that, say, r1,c1 = n1 is a given. You check each grid, and if it has n1 in cell r1c1 you write down its integer, and build up a subset of integers. You call this subset of integers, "r1,c1 = n1 is a given", and you can identify this with the subset of all Sudoku grids that have r1, c1 = n1 as a given.

Now, you can either do this nor not do this for each r1,c1, and n1. If you don't do this for a particular r1, c1 and n1 you can say, of some subset of grids, r1,c1 = n1 is not a given.

So, if you do the check, r2, c2, = n2 on the subset "r1,c1 = n1 is a given" and produce a, (presumably smaller) subset, you would call it "r1c1 = n1, is a given and r2,c2, = n2 is a given".

Now, do we need an axiom such that "r1c1 = n1, is a given and r2,c2, = n2 is a given" is always the same set as "r2c2 = n2, is a given and r1,c1, = n1 is a given" ?

ie, do we need a commutative law of assigning givens, analogous to the commutative law of addition in mathematics ? I think that the answer is no, because we are dealing with finite sets here, and we could, and should, in principle, check each one. In fact I can't think of any axioms that you would need, precisely because we are dealing with finite sets here. I have no doubt that the commutative property is true but claiming that it has the status of an axiom seems to me to be a fudge (in logic).

Finally, to fully specify each particular case, you have to identify, for each ri,ci,ni; i = 1 to 9, whether or not the filtering for ri,c1,ni, has been carried out.

So, you have to say something like " r1c1 = 1 is a given, r1c1 = n2 is not a given ................ r9c9 = 9 is not a given". When you have done all this you will have some set of integers, between 0 and S, which uniquely identifies the set of grids for which all the givens in every cell have been specified or not specified.

I didn't say this was easy or even useful, I'm just trying to answer a question here. I'm fully expecting to get shot down in flames but it was fun having a go at answering the question as best I could.

Leren

[denis_berthier]

denis_berthier wrote : how do you express "rc=n is not a given" in logic?

Well, I just love a challenge, and I' d rather get shot down in flames as a dunce than not try my hand at this one.

It's great to see someone giving it a try while others are typing unrelated random thoughts.

What you're doing is encoding all the possibilities.
I think there's a simpler way to do this, so that non-commutativity is not a problem. We can easily encode all the possible combinations of givens. We can restrict this to valid puzzles or keep it unrestricted; it doesn't matter. We can also restrict this to one puzzle in each isomorphism class or not; it doesn't matter either. (The set SN defined further on will just be different.)
There are 9 numbers, so let q1, ... q9 be the first 9 prime numbers and associate to each number i from 1 to 9 the prime number qi

There are 81 cells on the grid, with 81 possible values. For any puzzle P, replace each given i in any cell by qi (replace a non-given by 0). We get a sequence of integers r1, ..., r81
Now, for a puzzle P, define N(P) as N(P) = p1^r1 * p2^r2 * .... * p81^r81

It is obvious that the function N(P) fully encodes the givens of P. N defines an isomorphism between the chosen set of puzzles and some large but finite set of numbers SN.
Thus, each member of SN uniquely defines a puzzle (valid or unrestricted, depending on your initial choice).

This encoding also allows a straightforward filtering of all the puzzles that have some given subset of givens (that's why I didn't define N(P) merely as p1^n1 * p2^n2 * .... * p81^n81

That's all fine, but now what do we do with all this?
Sure, we can replace "rc=n is given" in P by "N(P) is divisible by px^qn" (where x is the number of cell rc on the grid). And we can also replace "rc=n is not given" by N(P) is not divisible by px^qn

We have transformed a problem statement in logic into a problem statement in arithmetics. But the same question remains: how do we manage this? How do we use this for any inference?

Finally, that was an interesting try, but it doesn't solve the problem. If you want to try again, use my guidelines: try to define logical axioms for predicate not-given(n, r, c). It's not possible, but it's worth trying and understanding why it's not possible. It involves only very basic logic.
Just one more hint. If you had to define an axiom for some predicate given(n, r, c), it could obviously be: given(n, r, c) => rc=n
or, more formally, given(n, r, c) => value(r, c) = n

[StrmCkr]

The 81 grid string is the gives

The 4 cells in question land in the empty un marked cells and do not have canadidate a or b marked via line of sight.

The collorary exolination based on non uniquness asumptions reduce the pm grid ie 729 candidstes that markup the subgrid field
arange to hold the pm ur pattern outline mutiple times above.
The candour is that no subgrid generated will house a mutisolution state on a grid that has 1 solution.

Which means that the generated starting point (81 grid string, arangment of un marked clues cannot contain a uniquness state either which is what the ur1. 1 can identify with out pms ie 729 grid string. (ie it uses the hidden set)
Compared to unique rectangle arguments that rely on the 729 grid string to show mutisolution substates.

The reason this works is that a finalized grid strings subgrids are assumed to finate lock all digits using blr for example into the 1 clue per rcb construction contraints of a sudoku grid.

[Serg]

It's great to see someone giving it a try instead of typing unrelated random thoughts.

Thanks, Denis. You are very kind.

Serg

[Serg]

Hi, eleven!

If I am not mistaken, the debates in this thread are about possibility of "UR 1.1" rule's usage in "rigorous" approach. For me, "UR 1.1" rule cannot be used in rigorous approach (similar to other uniqness methods).

You are mistaken. See this first post about the topic from 2006.

Thank you for the link! It's new for me. RW said interesting idea, but I don't understand at the moment - was that idea proven or no.

Serg

[denis_berthier]

Hi, eleven!

If I am not mistaken, the debates in this thread are about possibility of "UR 1.1" rule's usage in "rigorous" approach. For me, "UR 1.1" rule cannot be used in rigorous approach (similar to other uniqness methods).

You are mistaken. See this first post about the topic from 2006.

Thank you for the link! It's new for me. RW said interesting idea, but I don't understand at the moment - was that idea proven or no.

For me, the most interesting part of RW's post is this, in his summary:

-If you are able to remove a candidate inside a possible deadly pattern by use of numeral logic, the deadly pattern cannot be there, and you may make uniqueness reduction associated to that particular deadly pattern, even if you don't know if the puzzle has an unique solution.

This is quite cryptic, but I understand it as follows:
- if a candidate belonging to a potential deadly pattern can be eliminated by an ordinary resolution rule (i.e. a rule that doesn't assume uniqueness), there cannot really be a deadly pattern.
- The rest is tautological: if there's an ordinary rule that can eliminate a candidate, then there's no need for making any assumption of uniqueness to eliminate it.

[champagne]

Hi, eleven!

If I am not mistaken, the debates in this thread are about possibility of "UR 1.1" rule's usage in "rigorous" approach. For me, "UR 1.1" rule cannot be used in rigorous approach (similar to other uniqness methods).

You are mistaken. See this first post about the topic from 2006.

Thank you for the link! It's new for me. RW said interesting idea, but I don't understand at the moment - was that idea proven or no.

Serg

Hi Serg,

Code: Select all

     *-----------------------------------------------------------*
     | 5     2     9     | 168   18    3     | 7     4     168   |
     | 4     3     6     | 189   7    *159   | 2    *1589  189   |
     | 1     8     7     | 2     4    *569   | 3    *59    69    |
     |-------------------+-------------------+-------------------|
     | 3     14    58    | 189   6     2     | 45    7     189   |
     | 9     46    2     | 5     18    7     | 46    18    3     |
     | 7     16    58    | 4     3     19    | 56    189   2     |
     |-------------------+-------------------+-------------------|
     | 2     9     4     | 16    5     16    | 8     3     7     |
     | 8     7     1     | 3     2     4     | 9     6     5     |
     | 6     5     3     | 7     9     8     | 1     2     4     |
     *-----------------------------------------------------------*

If I got it in the right way, the UR1.1 example is simpler, but the logic is the same.

Here we have an example were the solving path kills the candidate 9 r2c8.

Having now one candidate erased, the potential UR 59r23c68 is not possible (sudoku or rubbish sudoku, it does'nt matter)

Due to the XWing on the digit 5
9r2c6 would force the impossible pattern
9 5
5 9

so, what is said briefly, 9r2c6 is not possible.

The rest is trivial, but the clearing of 9r2c6 is a direct effect of the unavoidable set property.

[eleven]

... but I don't understand at the moment - was that idea proven or no.

Hi Serg,
it is proven in the post. This might not be clear to you, if you are not used to uniqueness arguments. The proof, that a simple uniqueness pattern

Code: Select all

ab . . | ab . .
ab . . | ab . .

is not possible in a puzzle with a single solution is:
The puzzle either solves to

Code: Select all

a . . | b . .
b . . | a . .


or

Code: Select all

b . . | a . .
a . . | b . .


I.e. you have a U4 in the solution grid. As you know, one of the cells must be a given to get a unique solution. Otherwise you can switch the digits to get a second valid solution for the given puzzle.

The same argument is used here. The uniqueness pattern would give 2 solutions. But since one of the candidates had been eliminated, only one is possible. So you can eliminate any candidate, which would lead to a U4 in the solution. In RW's sample this is the 9 in r2c6 (9r2c6->5r3c6->9r3c8->5r2c8 gives the U4).

In other words: with 9r2c6 you would have a U4 with 2 solutions, but only one is possible with the eliminated 9 in r2c8 - a contradiction. Therefore 9r2c6 can be eliminated without any assumption, that the puzzle has only one solution.

Hope this made it clearer.

[Ah, cross-posted with champagne ...]

[Leren]

denis_berthier wrote: .... We have transformed a problem statement in logic into a problem statement in arithmetics. ... How do we use this for any inference.

It wasn't my intention to transform the problem statement into one of arithmetic, but for it to remain in the realm of set theory.

There might be some things that need modifying in my previous post but I'll just give an example to see how I meant this to work. here is a puzzle, yes, it's the same UR1.1 example I used earlier.

Code: Select all

*-----------*
|.5.|...|...|
|.6.|5.4|2..|
|..8|.71|...|
|---+---+---|
|4..|..3|6.8|
|...|...|...|
|89.|1..|7..|
|---+---+---|
|3..|...|...|
|...|2.7|.1.|
|.72|.3.|.9.|
*-----------*
.5........6.5.42....8.71...4....36.8.........89.1..7..3...........2.7.1..72.3..9.

We start with the full catalog of Sudoku grids. We then go through a series of 24 subset formation operations (equivalent to assigning a given in a cell, 24 clues in common parlance).

I'm pretty sure that we will end up with a set with just one integer, just for fun let's call it 5,123,903,864,021,072,936,921.

We look up our catalog of Sudoku grids for this number and find this one. Yes, its the unique solution of the puzzle with the 24 givens, but we already know this because the final subset had just one entry.

Code: Select all

*-----------------------*
| 9 5 4 | 3 8 2 | 1 6 7 |
| 7 6 1 | 5 9 4 | 2 8 3 |
| 2 3 8 | 6 7 1 | 4 5 9 |
|-------+-------+-------|
| 4 1 7 | 9 5 3 | 6 2 8 |
| 6 2 5 | 7 4 8 | 9 3 1 |
| 8 9 3 | 1 2 6 | 7 4 5 |
|-------+-------+-------|
| 3 4 6 | 8 1 9 | 5 7 2 |
| 5 8 9 | 2 6 7 | 3 1 4 |
| 1 7 2 | 4 3 5 | 8 9 6 |
*-----------------------*

So, we can infer the contents of every cell, even the ones for which we did not supply a given.

As to your alternative formulation, perhaps it would be best for you to just explain why it is not possible to characterise a cell with no givens, since, as you say, the answer involves only very basic logic.

Also thanks for the complement, I'll put my dunce cap in the cupboard for the moment.

Leren

[Serg]

Hi, all!
eleven and champagne, thank you for clarification!
I saw formal proof of UR1.1 rule's correctness, provided by Red Ed. Frankly speaking, I thought that proof was some trick, because I didn't know unformal idea of this rule presented by RW. Now I changed my mind and I am sure "UR1.1 rule" can be safely used in "rigorous" approach to Sudoku solving. I am sure too this rule doesn't need puzzle's validity assumption to be true.

Unformal idea is simple. Suppose candidate sets for some 4 empty ("unclued") cells of the puzzle permit one permutation of U4 unavoidable set (based on these 4 cells), but prohibit another (2nd) permutation of U4. We can safely exclude permitted permutation from our consideration, because solution paths with both permutations will be identical. Both solution paths simultaneously either lead to contradictions, or produce puzzle's solutions. Because we proved by some rigorous ("non-uniqness") techniques that the first UA permutation lead to contradiction, we can be sure that the second permutation lead to contradiction too.

Deleted, it's not true:
[But I think, Denis is also right when he say that similar idea should be true for clue cells. Suppose we have a valid puzzle with solution grid, having U4 hitted by one clue cell. We can now change this clue cell to the value from the second U4 permutation. Now we have another valid puzzle, because number of puzzles' solutions must be the same. I need more time to ponder this idea ...]

Serg

[Edited. I deleted "crazy" idea.]

[eleven]

Suppose we have a valid puzzle with solution grid, having U4 hitted by one clue cell. We can now change this clue cell to the value from the second U4 permutation. Now we have another valid puzzle, because number of puzzles' solutions must be the same.

It would not be a valid solution to the given sudoku. So the requirement or condition (not "extra-logical assumption", maybe someone can post a definition for that, i cannot trust Denis, who posted 2 wrong counter-examples, because he did not read the definition of UR1.1) for the rule is, that there are no givens in the 4 cells.

[denis_berthier]

denis_berthier wrote: .... We have transformed a problem statement in logic into a problem statement in arithmetics. ... How do we use this for any inference.

It wasn't my intention to transform the problem statement into one of arithmetic, but for it to remain in the realm of set theory.

I may have misinterpreted your intention. But it suggested me another encoding where everything can be interpreted in terms of division.
Any consistent encoding can be used to check that a grid is a solution of a puzzle.

As to your alternative formulation, perhaps it would be best for you to just explain why it is not possible to characterise a cell with no givens, since, as you say, the answer involves only very basic logic.

Yes, it's very basic and I have already given the main lines.

You need a predicate value(n, r, c) to mean that rc=n is in any solution. You also need a predicate linked(n, r, c, n2, r2, c2) to express that two potential candidates are linked. (predicate linked is structural; it doesn't depend on the grid content)
With these two predicates, you can express the 4 basic rules of Sudoku.
Typically, during resolution, the "value" predicate can be used for eliminating candidates:
value(n, r, c) and linked(n, r, c, n2, r2, c2) => not candidate(n2, r2, c2)
It can also be used to assert other values, using Singles.
With only these two basic resolution rules, you can already solve almost 30% of the puzzles.
For more detail, see HLS or PBCS.

Now, suppose you have a predicate given(n, r, c) with the intended meaning suggested by the name. What can you do with it?
First thing is, you know that every given will be in any solution. So, you'll have the axiom: given(n, r, c) => value(n, r, c). This will be used during resolution to initialise the "value" predicate.
Second thing is, for any puzzle, you can introduce the relevant data as a set of given(ni, ri, ci) assertions.
Now, considering the already defined axioms for value, this expresses everything one can do with "given". It'd be useless to re-write the same axioms for "given", as they would be less general. And "given(n, r, c) itself cannot be deleted or asserted for new candidates. It stays there, overlooking what happens, but never participating in any further inferential event after initialisation.

Now, to the point of introducing a "not-given" predicate. There's no way for doing this in any useful way. Of course, you can always define formally not-given(n, r, c) as the opposite of "given" : not given(n, r , c); but this leads to nothing new.
You can't write an axiom such as not-given(n, r, c) => not value(n, r, c); that'd be false.
You can't use "not-given" either for asserting any candidate. In short, there's nothing you can do with "not-given" at a basic level.

If "not-given" cannot appear in any basic rule of Sudoku, how could it magically appear in complex rules derived from the basic rules only? This can only be possible by using extra-logical arguments.

(*) I omitted the universal quantifiers for clarity

Also thanks for the complement, I'll put my dunce cap in the cupboard for the moment.

I realise the way it was written might have been ambiguous. I modified it.