Sudoku Players' Forum (clone)

re'born wrote:Is it true that the existence of a solution implies that the puzzle is solvable using backtracking?

Hi re'born. It's been so long.
Yes, obviously, if by backtracking you mean full structured search, including the acceptance of positive results (what's usually called guessing).

re'born wrote:If so, it seems the only assumption Ed's proof uses is that the puzzle has a solution.

No. Re-read my post about constructiveness, you'll see that his "basic fact" refers to two solutions, one of which has no chance of being built constructively.

re'born wrote: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?

Can you give any example of such a rule?

Allan Barker wrote: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.

Unless I'm missing your point, it seems obvious to me.
Consider the logical theory ST+P consisting of the Sudoku axioms plus the specific entries of the puzzle. Then, from the completeness and consistency theorems of FOL, being provable from ST+P (I guess this is what you mean by a "combination of Sudoku logic " and being true in all the models of ST+P, i.e. in all the solutions of P, is equivalent.
If you suppose non uniqueness, as the cells with multiple candidates in the UR will have different values in different models, these values can't be proven from ST+P - which is equivalent to saying the other candidates can't be deleted by any "combination of Sudoku logic".

Allan Barker wrote:My interest is not specific to UR1.1 rather, the principle has far reaching implications, not limited to--

Can you mention some of these implications?

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

Each of my resolution rules can straightforwadly be proved constructively, its validity doesn't depend on this principle.
All my rules work on puzzles with any number of solutions: 0, 1 or more.
I've given examples of how they can prove that a puzzle has no solution.
For a puzzle that has several solution, they can find only what is common to all the solutions.

denis_berthier wrote:

re'born wrote:If so, it seems the only assumption Ed's proof uses is that the puzzle has a solution.

No. Re-read my post about constructiveness, you'll see that his "basic fact" refers to two solutions, one of which has no chance of being built constructively.

Adam, yes, I agree with you.

I think Denis is only banging on about "constructive" proofs because this discussion is taking part in his RR thread. The rest of us who prefer to solve using other tricks can ignore the constructivist caveats to my proof and just enjoy using UR1.1 as a fact.

denis_berthier wrote:

re'born wrote:Is it true that the existence of a solution implies that the puzzle is solvable using backtracking?

Hi re'born. It's been so long.
Yes, obviously, if by backtracking you mean full structured search, including the acceptance of positive results (what's usually called guessing).

re'born wrote:If so, it seems the only assumption Ed's proof uses is that the puzzle has a solution.

No. Re-read my post about constructiveness, you'll see that his "basic fact" refers to two solutions, one of which has no chance of being built constructively.

No offense, Denis, but your notion of constructiveness is the extra assumption. As far as I can tell, you're the only one around here using it. But put constructiveness aside for a moment. Please tell me you see the qualitative difference in using a rule (like UR1.1) that relies on the theoretical ability to solve the puzzle using backtracking and actually performing backtracking.

Red Ed wrote:I think Denis is only banging on about "constructive" proofs because this discussion is taking part in his RR thread. The rest of us who prefer to solve using other tricks can ignore the constructivist caveats to my proof and just enjoy using UR1.1 as a fact.

Thanks for the "banging on" and for your interpretation of my motivations. This shows how open you are to others' ideas.

When one formalises things in first order logic, one has to introduce a predicate candidate(n, r, c) and this predicate appears to mean that "n is not known to be false in cell rc".
The logic of candidates is thus intrinsically epistemic logic, and I've shown that it uses indeed a subset of formulæ in this logic for which it is equivalent to constructivist logic (or intuitionnistic if you prefer, these are just different names for the same variant of first order logic).

Anyone is free to solve puzzles using any rules he wants or even backtracking - I've never said otherwise.
But you needn't talk down the work of those of us who are interested in the logical foundations of the rules they use.

re'born wrote:your notion of constructiveness is the extra assumption.

Constructive logic is weaker than classical logic. How could it be an extra assumption?
Classical logic is the default assumption, but not necessarily always the best one. See my last answer to RedEd.

re'born wrote:As far as I can tell, you're the only one around here using it.

And AFAIK, I'm also the only one around here to have developed a formal framework based on first order logic. Or do you have any other reference?

Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?
"Intuistionnistic" logic has not been named so by mere chance.

re'born wrote:But put constructiveness aside for a moment. Please tell me you see the qualitative difference in using a rule (like UR1.1) that relies on the theoretical ability to solve the puzzle using backtracking and actually performing backtracking.

A precision. I didn't say RedEd's proof relied on backtracking.

But to answer your question, I'd say, yes, there is some nuance.

Ok, i already was gone here, but this is really great, Denis.

As we saw, you have serious problems with contradiction proofs and a bit abstract thinking. So its an ingenious idea to ban anything from your rules, which needs such things. Puuh, how narrow it becomes here now ! And now you claim, we should be open for that.
[edit: should be ingenious]

I suspect, Denis, that we are talking about different things...

denis_berthier wrote:

re'born wrote:your notion of constructiveness is the extra assumption.

Constructive logic is weaker than classical logic. How could it be an extra assumption?
Classical logic is the default assumption, but not necessarily always the best one. See my last answer to RedEd.

Your extra assumption is that one needs to find a solution path using resolution rules (as you define them). That is a matter of taste on your part. The rules of sudoku do not mandate that a solution be found using 'pure logic' (and you really need to stop using that phrase as it is needlessly inflammatory and offensive to people who solve puzzles using ideas that fail to meet your standards). To require such is fine, but it changes the game.

Denis wrote:

re'born wrote:As far as I can tell, you're the only one around here using it.

And AFAIK, I'm also the only one around here to have developed a formal framework based on first order logic. Or do you have any other reference?

LOL. Oh, that's a good one. For a second, I thought you were trying to pull rank on me. Phew...thank goodness you would never try something so asinine.

Denis wrote:Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?

I'm sorry Denis, I don't understand your question. Who is asking me to suppose there might be another solution?

Denis wrote:"Intuistionnistic" logic has not been named so by mere chance.

That's true...and that goes as well for the spelling of intuitionistic.

re'born wrote:

denis_berthier wrote:

re'born wrote:your notion of constructiveness is the extra assumption.

Constructive logic is weaker than classical logic. How could it be an extra assumption?
Classical logic is the default assumption, but not necessarily always the best one. See my last answer to RedEd.

Your extra assumption is that one needs to find a solution path using resolution rules (as you define them). That is a matter of taste on your part. The rules of sudoku do not mandate that a solution be found using 'pure logic' (and you really need to stop using that phrase as it is needlessly inflammatory and offensive to people who solve puzzles using ideas that fail to meet your standards). To require such is fine, but it changes the game.

I've always been clear and I've always said that my framework is an interpretation and a formalisation of the undefined expression "pure logic solution".
Requiring a "pure logic solution" changes the game, whatever is meant by this.
I think few players would accept backtracking. So doing, they change the game.
What I'm doing is developing a consistent conceptual framework. You may accept it or not, but you can't deny it allows to define powerful resolution rules.

re'born wrote:

denis_berthier wrote:Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?

I'm sorry Denis, I don't understand your question. Who is asking me to suppose there might be another solution?

RedEd's proof

denis_berthier wrote:

re'born wrote:

denis_berthier wrote:

re'born"]your notion of constructiveness is the extra assumption.

Constructive logic is weaker than classical logic. How could it be an extra assumption?
Classical logic is the default assumption, but not necessarily always the best one. See my last answer to RedEd.

Your extra assumption is that one needs to find a solution path using resolution rules (as you define them). That is a matter of taste on your part. The rules of sudoku do not mandate that a solution be found using 'pure logic' (and you really need to stop using that phrase as it is needlessly inflammatory and offensive to people who solve puzzles using ideas that fail to meet your standards). To require such is fine, but it changes the game.

I've always been clear and I've always said that my framework is an interpretation and a formalisation of the undefined expression "pure logic solution".
[/quote]
Yes, but you've never accepted that using that phrase, at best, seems like a PR move, and, at worst, is insulting to a large number of players. If I used an expression similar to a racial slur for a resolution rule, it wouldn't matter how many times I explained the exact meaning or protested that it was merely 'a formalization of an undefined expression', I would still get my <expletive deleted> kicked.

[quote="Denis wrote:Requiring a "pure logic solution" changes the game, whatever is meant by this.

I completely agree.

Denis wrote:I think few players would accept backtracking. So doing, they change the game.

If you are talking about players on the forum, yes. If you are talking about the millions around the world who play, I suspect (with good reason) a whole lot of backtracking goes on.

Denis wrote:What I'm doing is developing a consistent conceptual framework. You may accept it or not, but you can't deny it allows to define powerful resolution rules.

The problem isn't me (or anyone else) accepting your 'consistent conceptual framework' and I won't deny your 'powerful resolution rules'. As a player, I find the framework almost useless, but as a mathematician, I very much appreciate the point of view. The problem is

Denis wrote: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.

You are confusing the issues by suggesting that RedEd's proof is hiding an assumption, when the reality is that it is your conceptual framework that requires a different standard of proof for a deduction. The default is always anything goes.

Denis wrote:

re'born wrote:

denis_berthier wrote:Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?

I'm sorry Denis, I don't understand your question. Who is asking me to suppose there might be another solution?

RedEd's proof

In that case, no I'm not intuitively (or otherwise) shocked; I've seen a proof by contradiction before.

Denis, way back when you made the claim that no one could logically (without T&E) identify the multiple solutions of a multi-solution puzzle, I called you on it. Your personal logical framework cannot even represent the multiple solutions of a multi-solution puzzle. Therefore it is not surprising that first, you don't care about such things; and second, your framework can't tell you anything about such things. The best you will ever be able to do with your framework is solve the cells that solve to the same digit in all the multiple solutions. Your framework is blind to anything outside of that and so you really can't use it to say anything about what happens or what might be logically possible on the other side of your self-imposed logical event horizon.

re'born wrote:

Denis wrote:I think few players would accept backtracking. So doing, they change the game.

If you are talking about players on the forum, yes. If you are talking about the millions around the world who play, I suspect (with good reason) a whole lot of backtracking goes on.

I completely agree with this. And I can see no problem if they are happy with it. And I'm aware I have nothing interesting to tell them about backtracking.

re'born wrote:as a mathematician, I very much appreciate the point of view.

Thanks. Compliments are not so frequent here.

re'born wrote:

Denis wrote: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.

You are confusing the issues by suggesting that RedEd's proof is hiding an assumption, when the reality is that it is your conceptual framework that requires a different standard of proof for a deduction. The default is always anything goes.

You are probably right. But it is well known that our default beliefs have always lots of hidden assumptions. Expliciting them is even a main motor for progress in any science.
Now I can't see how the idea of a resolution path consisting of a sequence of steps, each of them being the application of a resolution rule, would be so alien to Sudoku solving practice.

re'born wrote:

Denis wrote:

re'born wrote:[quote="denis_berthier"]Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?

I'm sorry Denis, I don't understand your question. Who is asking me to suppose there might be another solution?

RedEd's proof

In that case, no I'm not intuitively (or otherwise) shocked; I've seen a proof by contradiction before.[/quote]
I had never seen a proof by contradiction before.

To tell the whole truth, I had never been very interested by constructive logic. My framework naturally led me to it but as all my resolution rules can be proven in a straightforward constructive way, I had not attached much attention to this formal aspect of things.
UR1.1 has been a very exciting thing for me, because it provides a very clear and elementary example of a difference between constructive logic and classical logic.

Myth Jellies wrote:Denis, way back when you made the claim that no one could logically (without T&E) identify the multiple solutions of a multi-solution puzzle, I called you on it. Your personal logical framework cannot even represent the multiple solutions of a multi-solution puzzle. Therefore it is not surprising that first, you don't care about such things; and second, your framework can't tell you anything about such things. The best you will ever be able to do with your framework is solve the cells that solve to the same digit in all the multiple solutions. Your framework is blind to anything outside of that and so you really can't use it to say anything about what happens or what might be logically possible on the other side of your self-imposed logical event horizon.

All this is perfectly true. And I can only give you the same answer as previously.

Firstly, we should notice that it is irrelevant in practice, as valid puzzles are supposed to have one and only one solution.

Secondly, this is not a specificty of my framework but of first order logic.
There are two fundamental theorems of first order logic: completeness and consistency. They make the link between the two complementary aspects of logic: proof theory and model theory. They imply that a logical theory can only prove what is valid in all its models.
Any framework relying only on FOL will have these same characteristics.

As a result, to solve a cell that may have different values in different solution grids, some form of trying every possibility is needed. In an implementation, this will inevitably involve some form of guessing. Allan has reached the same conclusion.

Allan Barker wrote:

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.

I've already told you several times how much I appreciate your framework.
I'm not considering "pure logic" as a label one should obtain to be respected. And I'm not considering myself as the dispatcher of any labels.
As "pure logic" appears to be a controversial expression, I think we'd better avoid it in the future.

There is some ambiguity in the name you are using: "set-logic". In maths, I know two sub-disciplines directly related to this: set theory and logic.

We've previously reached the conclusion that your framework is based on second order logic. In the standard interpretation of second order logic (subsets of a model are its natural subsets) there is no completeness and consistency theorem, which makes this logic very hard to use. The reason for this absence is that this logic includes implicitly a large part of set theory, which is generally considered too powerful by logicians for being used easily. When we speak of logic with no precision, we understand first order logic by default.

Now there's also another possible, probaly simpler, formal interpretation that I'ven't examined: finite set theory. What do you think of it?

denis_berthier wrote:As a result, to solve a cell that may have different values in different solution grids, some form of trying every possibility is needed.

No, not always. Some time i had fun with solving some multisolution puzzles manually, at least when at the end i got a nice deadly pattern with 10 or 12 cells. Of course its kind of poor, when mighty resolution rules cant solve this one without guessing:

Code: Select all

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