Sudoku Players' Forum (clone)

As my last contribution to this thread let me tell a joke (hopefully my English does it):
In a classical concert a man in the audience stands up and asks:
"Is a doctor here ?"
People make "shshsh" and he sits down.
A while later he again stands up:
"Is a doctor here ?"
Finally another man behind stands up:
"Yes, what is it ?"
The man shouts:
"Isnt this a wonderfull music, colleague ?"

Constructiveness and the hidden hypothesis

What do we call a solution? What kind of solutions do we accept? E.g. do we accept a solution obtained via recursive search with guessing - backtracking as it is also called?
I have developed the resolution rules perspective in order to formalise the distinction between a "pure logic" solution and a solution obtained by unrestricted means such as the above mentioned ones. In this perspective, a solution is one that can be obtained by repeated application of the resolution rules. It is a constructive solution.

Now, RedEd's "basic fact"

RedEd wrote:Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.

on which his whole proof rests, becomes obviously false if we accept only constructive solutions: how could r1c1 = 2 be constructively proved from the axioms of Sudoku and the entries when r1c1 = 1 has already been constructively proved at the time the UR1.1 pattern is detected? (or, to put it differently, how could two contradictory values be constructively proved if the puzzle is consistent?)

Conclusion: RedEd's proof has an implicit assumption: we must accept any kind of solution, including non constructive ones, e.g. those obtained by recursive backtracking with guessing.

One could now say: OK, but merely accept UR1.1 as being a resolution rule and you can use it to get constructive solutions.
But this doesn't work: a solution obtained by a rule that can't be proved constructively can't really be called a constructive solution.


As is the case for uniqueness, accepting such rules is a matter of personal choice and of how ambitious we are about our solutions.
After all, using backtracking, a beginner in programming can write a program that outputs the solution of any puzzle in a few milli-seconds. If we don't put some restrictions on what we accept, why don't we just use backtracking?
But, as for everything, different people will have different ideas of what is acceptable and what is not.


I planned to explain another aspect of UR1.1 in another post but I've no time to finish it now.

*sigh*

My definition of "solution grid" is any valid Sudoku grid, with all cells filled-in, that contains the puzzle.

Suggesting other definitions seems pointless to me.

Red Ed wrote:My definition of "solution grid" is any valid Sudoku grid, with all cells filled-in, that contains the puzzle.
Suggesting other definitions seems pointless to me.

*sigh*
You're merely forgetting that having the solution grid is the goal and that it has to be found by some methods.
Definitions of "solution" (not only the final result, a "solution grid", but the whole process to obtain it) consistent with these methods are pointless to you because you are not concerned with Sudoku solving and with the desire of most players to avoid guessing, backtracking and so on.

My proof talks about solution grids. You're interested in solution paths. Your discussion of validity of the latter is of no relevance to my proof. I would've thought it obvious that I was talking about grids, not paths.

"Solution grid", without a caveat, means just what I said previously. If you wish to distinguish solution grids that can be found using some prescribed set of rules from those that cannot, then may I suggest you talk of "reachable solution grids" or similar?

Red Ed wrote:My proof talks about solution grids. You're interested in solution paths. Your discussion of validity of the latter is of no relevance to my proof. I would've thought it obvious that I was talking about grids, not paths.

I think you're misinterpreting me.
It IS obvious you were talking of grids and not of paths.
And I said your proof is very smart. After lots of sterile posts from "believers", you came with a real mathematical proof.

But it is also a fact that most players want to consider only solutions obtained through "pure logic" - whatever they mean by this.
What I've done is build a conceptual framework based on first order logic that gives a precise meaning to this expression. In particular, in this framework, a solution has to be built constructively (the framework is thus based on constructive logic), each candidate being deleted and each value being added by repeated applications of resolution rules. AFAIK, no other proposal has ever been made of any alternative interpretation of "pure logic" solution.
In this framework, UR1.1 can't be proved.
To say it more technically, your proof is not valid in constructive (or intuitionnistic) logic.

denis berthier wrote:Sudoku is a logic game. I'm dismayed to see how easily some players with no logical or mathematical background get stucked in incantations based on undefined notions.

So apart from the casual insult, this implies that all DB's incantations are based on defined notions.

denis_berthier wrote:
Now, RedEd's "basic fact"

RedEd wrote:Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.

on which his whole proof rests, becomes obviously false if we accept only constructive solutions: how could r1c1 = 2 be constructively proved from the axioms of Sudoku and the entries when r1c1 = 1 has already been constructively proved at the time the UR1.1 pattern is detected? (or, to put it differently, how could two contradictory values be constructively proved if the puzzle is consistent?)

Conclusion: [b]RedEd's proof has an implicit assumption: we must accept any kind of solution, including non constructive ones, e.g. those obtained by recursive backtracking with guessing.

So where has the notion of only "constructive" solutions being acceptable ever been defined let alone discussed and generally accepted? From what's written I still have little clue about what this term accepts and rejects. (Or perhaps the Sudoku "logic game" is only really meant for the entertainment of mathematicians with higher degrees.)

How do we eliminate any candidate? On the basis that it can't exist in the valid final solution (or solutions) we expect to derive. The same is true for a "resolvable rectangle" elimination.

If we find that in our anticipated solution that (9)r1c1 and (9)1c9 can't both be false we cheerfully eliminate any other 9s in row 1 despite not having assigned values in either of these cells. How can this prevention of an upcoming contradiction be considered acceptable but not the same form of logic applied to the resolvable rectangle?

removed

Is it true that the existence of a solution implies that the puzzle is solvable using backtracking? If so, it seems the only assumption Ed's proof uses is that the puzzle has a solution.

Denis, please tell me I'm misinterpreting you. Are you suggesting that when solving a puzzle using a rule whose proof relies on the fact that any sudoku with at least one solution is solvable via backtracking is comparable to actually backtracking?

Wow this is still running.

There is no integer multiple of 2 equal to unity. There is an integer multiple of 2 equal to zero.

denis_berthier wrote:What do we call a solution? What kind of solutions do we accept? E.g. do we accept a solution obtained via recursive search with guessing - backtracking as it is also called?
I have developed the resolution rules perspective in order to formalise the distinction between a "pure logic" solution and a solution obtained by unrestricted means such as the above mentioned ones. In this perspective, a solution is one that can be obtained by repeated application of the resolution rules. It is a constructive solution.

Now, RedEd's "basic fact"

RedEd wrote:Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.

on which his whole proof rests, becomes obviously false if we accept only constructive solutions: how could r1c1 = 2 be constructively proved from the axioms of Sudoku and the entries when r1c1 = 1 has already been constructively proved at the time the UR1.1 pattern is detected? (or, to put it differently, how could two contradictory values be constructively proved if the puzzle is consistent?)

Conclusion: RedEd's proof has an implicit assumption: we must accept any kind of solution, including non constructive ones, e.g. those obtained by recursive backtracking with guessing.

Denis, sorry, I was away. It seems we now arrive at the same point, that which I referred to as the Missing Oracle of Uniqueness. Given a multiple solution puzzle where no candidates have yet been removed from the multiple solutions, no combination of Sudoku logic can eliminate any candidate in the multiple solutions and thus force one of the solutions. My interest is not specific to UR1.1 rather, the principle has far reaching implications, not limited to--

Allan Barker wrote:Proving the missing oracle principle would be very useful ...... If correct, it could indicate the presence of unknown or unintended trial and error in a set of rules or a solver, when the rules or solver is able to eliminate candidates from a UR or isolate any of the puzzle's solutions.

Can you provide a logical proof that this principle is true for problems of all complexity, and is therefore true for your resolution rules.
.
.

denis_berthier wrote:What I've done is build a conceptual framework based on first order logic that gives a precise meaning to this expression. In particular, in this framework, a solution has to be built constructively (the framework is thus based on constructive logic), each candidate being deleted and each value being added by repeated applications of resolution rules. AFAIK, no other proposal has ever been made of any alternative interpretation of "pure logic" solution.

I'm not quite sure why you have skipped over my set-logic but it has always produced only pure logic solutions, as I have often stated. It has also been able to provide pure logic solutions for all of the most difficult puzzles.

It also uses natural logic, where I define natural to mean any possible configuration of pure Sudoku logic without imposed restrictions, i.e., requiring bi-value sets, chains, etc.
.

ronk wrote:

denis_berthier wrote:Thanks, RedEd, for this very smart proof.

Thanks Denis, for finally seeing the light of day.

Alas It was only a flickering candle.

Glyn wrote:Wow this is still running.

Yes, but we're no longer discussing uniqueness and we're now back to the topic of this thread.
My whole approach, described in the first posts of this thread (resolution rules, resolution paths, ...) leads to constructive solutions of puzzles. I hadn't insisted on this aspect of the underlying formal logic, although this was already in the first edition of my book, because you can see the reactions when we get too formal, but UR1.1 is a very good illustration of this point.

BTW, as it is no longer related to uniqeness, it should be given another name.

ronk wrote:Alas It was only a flickering candle.

I love you too.