Originally published at https://arling.sk/notes/how-a-logic-puzzle-is-proved-to-have-exactly-one-solution/

How a logic puzzle is proved to have exactly one solution

Every puzzle book in the world says its puzzles have one solution. Almost none of them say how that was established, and the difference between the books is entirely in that missing sentence. There are two separate claims hiding in the promise, and a book can pass the first and fail the second. The first is that the grid has exactly one filling that satisfies the rules. The second is that a person can reach that filling by reasoning, without ever guessing and backtracking. This note explains how both are checked by machine, what our files actually record about each puzzle, and where the claim stops, because a claim with no stated edge is not a claim. None of it requires you to trust us: the checks are ordinary programs doing ordinary searches, and their results are written into the files themselves.

The first claim: exactly one filling

A puzzle is not designed and then trusted. It is generated, then handed to a solver that is asked to find solutions, and it survives only if the solver returns exactly one. Everything else is thrown away.

The important word is exactly. A solver that stops at the first solution it finds proves that at least one exists, which is a weaker statement and the one most generators settle for. Ours keeps searching to establish that there is no second solution, and a candidate is discarded when that search finds one. In the daily games this runs as a second, independent search after the generator is done, so the check is not the same code that made the puzzle believing its own work.

The second claim: no guessing

A grid can have a unique answer that no human can find without trial and error, and such a puzzle is technically correct and miserable to solve. So the generator also runs a solver that is restricted to the rules a person can actually use, and it accepts a puzzle only when that restricted solver finishes without guessing.

This is also how difficulty stops being a marketing word. The solver counts how many deduction steps of each kind a finished puzzle needs, and candidates for a date are ranked by that count, so easy and hard mean measured amounts of work rather than a label chosen by hand.

There is one deliberate exception, and it is written down: in the daily logic grid puzzle, the Sunday level has one square that only gives way when you test an assumption until a clue breaks. That is a choice about one day of the week, not a slip.

Where the proof is written down

In the public puzzle files, each puzzle carries its own record: the static puzzle interface holds 6000 puzzles, ten kinds in three levels with 200 per kind and level, and every one is a file with the puzzle, the solution and a verified block holding uniqueSolution and the measured solver time in milliseconds. The proof is not a promise in a listing, it is a field in the file.

The browser generator does the same thing in front of you: every puzzle it makes is handed back to the solver of its own kind and shown only when that solver finds exactly one solution without guessing, with the measured time of the check printed under the puzzle. In the books the rule is the same, and the solution printed at the back is the one the solver found. The printed bulletin sheet says it in one line on the page: exactly one solution, found by the program that made this puzzle.

What the claim does not cover

Uniqueness is a statement about one grid, not about the history of the world. Our puzzles are excluded from each other, so a puzzle that has already appeared in a book, in the daily archive, in the planner or in a monthly issue does not appear again, and the scope of that statement is our own archive and our own editions rather than worldwide novelty.

Nor is generation random in the sense of being unrepeatable: the seed is a fixed string with the kind, the level and the index, never a date, and an accepted attempt is stored, so a second build produces the same files. And while you are solving, nothing turns red; an error is only shown by Check, in two steps, and both Check and Hint are free and unlimited.

FAQ

Does one solution mean the puzzle is fair?

Not on its own, which is why there are two checks. A puzzle is kept only when a solver limited to human reasoning finishes it without guessing, as well as when the search shows there is no second answer.

Can I check a puzzle myself?

If it comes from the puzzle interface, yes: the file carries the solution and a verified block with the uniqueness flag and the measured solver time. In the browser generator the measured time of the same check is printed under each puzzle.

Are these puzzles unique in the world?

No, and we do not claim it. The exclusion covers our own archive and our own editions, not worldwide novelty.

Where to look next

The eleven daily logic games are free, run in the browser without an account, and every daily puzzle goes through the checks above. The same puzzles as files, 6000 of them with the proof recorded in each one, are at https://arling.sk/api/, free for personal and non-commercial use with the credit line, with commercial use part of the Bulletin Pro subscription. If you would rather make your own, https://arling.sk/puzzle-studio/ runs the generator and the solver in your browser, two puzzles a day free.

ARLing also makes free daily logic puzzles.