53x15

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.

> 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

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)

I think neel_k was referring to the fact that when a DPLL or CDCL solver concludes UNSAT you can take the trace its backtracking activity and rewrite it from the bottom up as a resolution refutation. So in this sense the solvers are finding resolution proofs.

Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem.

Since specialized solvers do thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) that the author mentions in part 1 of the series:

For 17-clue puzzles (which are generally very easy), JCZSolve is 50x as fast as Minisat, and it makes on average ~1.9 decisions per puzzle compared to Minisat's ~3.0. But if you look at the hardest dataset JCZSolve is only 10x as fast as Minisat, and it makes on average ~365 decisions per puzzle compared to Minisat's ~121. I'm not aware of a highly specialized and optimized Solver for 16x16 clue or larger Sudoku, but given this trend my guess is that it would take a lot of effort to write one that's faster than what you get with Minisat for free.

[1] https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE...

Bear in mind that JSolve was 5x faster than the fastest DLX solver in the attractivechaos 2011 benchmarks, and today there are several solvers that are 2x faster than JSolve (https://github.com/t-dillon/tdoku/tree/master/benchmarks). If the difference is really an order of magnitude, that's pretty non-competitive.

I certainly don't mean do disparage DLX. It's a powerful and general algorithm. But if you need a fast Sudoku solver (for puzzle mining or studying Sudoku research questions) then it's not the tool I'd reach for. The backtracking solvers just get a lot of mileage out of tuning their representation to play nicely with hardware. They also blow general purpose CDCL SAT solvers out of the water, at least for 9x9 Sudoku.

This sounds like Crook's Algorithm (https://www.ams.org/notices/200904/tx090400460p.pdf), which is a perfectly reasonable thing to do, especially for pencil-and-paper puzzle solving since pigeonhole inferences are easy for people to spot. But this inference rule does not suffice on its own for many hard puzzles. Crook's algorithm still requires backtracking.

It's easy to see why this puzzle has no solution. Looking at columns 4-6 we see that none of the digits 1,5,6 can occur in cells G4,H4,I4 or G6,H6,I6. So some permutation of these digits occupies G5,H5,I5 and all digits other than 1,5,6 can be eliminated from these cells. But we also see that all the digits 1,5,6 have already been placed in row G, leaving no candidates for G5.

It's also easy to see why this presents a problem for the Norvig solver (and many solvers like it). If you squint at the algorithm you'll see that it behaves like DPLL (https://en.wikipedia.org/wiki/DPLL_algorithm) given a CNF encoding of the Sudoku exactly-one constraints. In this scheme constraint propagation only occurs via unit resolution. i.e., when a positive clause is reduced to a single literal because the domain of a cell is reduced to a single digit or a unit/group is reduced to having a single place for a given digit. In Sudoku land these are known as naked and hidden singles.

Unfortunately, the conclusion that none of 2,4,7,8,9 can occupy G5 arises from the interaction of multiple non-unit clauses. It is simply not reachable by unit resolution. As a result, the conflict won't be discovered until the algorithm actually attempts to assign G5, and, since there are many cells that initially have fewer possibilities than G5, this is not likely to happen early in the search.

Some of the faster solvers can handle this by adding checks for "locked candidates", or by representing the logic in a way that's equisatisfiable, but that makes these inferences available to unit resolution. In such cases this puzzle is recognized as unsatisfiable in microseconds.

It can be done with just depth first search, but if you want it to be fast you can go pretty far down the rabbit hole. The details of your representation, your heuristics, and the kinds of constraint propagation you support all matter a lot.

Here's a long walk through these issues in developing a fast solver: https://t-dillon.github.io/tdoku

I'm the author of Tdoku and maintainer of those benchmarks.

If anyone has a well optimized DLX implementation I'd love to add it to the comparison. The few I've sampled from github were not competitive, but I have no idea how much effort when into them.

This page from 2011 has some comparisons of backtracking and DLX solvers from that era, but it would be interesting to update: https://attractivechaos.wordpress.com/2011/06/19/an-incomple...