HackerTrans
TopNewTrendsCommentsPastAskShowJobs

53x15

no profile record

comments

53x15
·4 ปีที่แล้ว·discuss
If the solution is unique then there is a logical path to it, though maybe not one feasible to discover for an agent with bounded time and (especially for humans) bounded working memory.

Consider the search tree of a backtracking algorithm operating on a SAT-based representation of a puzzle. A leaf of the tree corresponds to some clause that becomes empty after eliminating literals assigned on the path to that node. If you flip the tree upside down and start from the clauses at the leaves, then two leaves with a common parent represent two clauses with complementary literals that can be resolved upon. So any branch of the algorithm's search tree can be viewed as a tree-structured resolution-refutation proof eliminating some value given a set of prior assignments on the path to the branch, and the tree as a whole can be decomposed into an ordered set of proofs for each elimination in the path to an overall solution.

Or, if you prefer, start again from the SAT-based representation and run a prime implicates algorithm like Tison's. Such an algorithm never advances a "guess" or generates a clause that is not entailed. It simply finds one logical consequence after another until it has found all of them, throwing away subsumed clauses along the way until all that's left is the unique solution.

Either way you will always produce a path to a solution and proof that the solution is unique using elementary rules of propositional logic that anyone can recognize. That, I think, is what your parent means.

Of course, the existence of a proof doesn't mean that a human can find that proof, and that's what we usually mean when we say there's no logical solution. That is, nothing new can be proven by scanning the puzzle looking for pattern matches against a fixed library of known proof templates taken to be the universe of logical techniques, and nothing can be proven from less structured heuristic search within the limits of human working memory and patience.
53x15
·4 ปีที่แล้ว·discuss
> A more reasonable question would be, how many partially completed sudoku grids are there which have a unique solution. We don't know the answer to that.

The number of minimal Sudoku puzzles is estimated (with 0.065% relative error) to be 3.1055e+37 (or 2.5477e+25 for non-isomorphic minimal puzzles). See Bethier https://arxiv.org/pdf/1111.4083.pdf
53x15
·4 ปีที่แล้ว·discuss
For a casual effort this solver is quite fast. On most datasets it's significantly faster than a C++ port of the Norvig solver and it's often in the same league as well-tuned DLX solvers (though still not in the major league).

Relative to DLX it's faster on the easiest puzzles and slower on hard ones, though its performance degrades significantly in two specific still-easy cases: (1) 17-clue puzzles since these punish solvers that don't propagate hidden singles, (2) 0-solution puzzles since the solver doesn't check for consistency during initialization (something the author acknowledges in a comment).

For context see these benchmarks from a modern laptop (https://github.com/t-dillon/tdoku/blob/master/benchmarks/res...) and compare lhl_sudoku to the other simple solvers tdev_basic_heuristic, zerodoku, fast_solv_9r2, kudoku, and norvig.

For details on the solvers and datasets used in these benchmarks see here (https://github.com/t-dillon/tdoku/tree/master/other) and here (https://github.com/t-dillon/tdoku/tree/master/benchmarks)