Constructiveness and the hidden hypothesisWhat 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.