How puzzles are made › Guide
How We Verify Every Puzzle Has One Solution
Finding one answer does not prove a puzzle is unique. Solvedle searches for a second valid answer, rejects puzzles with zero or multiple solutions, and separately checks that a logical grader can finish the board.
These checks answer different questions. Uniqueness concerns how many full boards satisfy the rules. Logical solvability concerns whether the implemented techniques can derive a complete answer from the clues.
Why search for two solutions?
| Search result | Meaning | Decision |
|---|---|---|
| 0, search complete | No board satisfies all rules and clues. | Reject. |
| 1, search complete | Exactly one board satisfies them. | Pass uniqueness; still check logic. |
| 2 found | At least two boards satisfy them; there may be more. | Reject as ambiguous. |
| Search budget reached | The remaining search is unresolved. | Do not accept as unique. |
The one-star solver searches row-by-row star positions. The binary solver combines rule propagation with branching over unfinished cells. Both count up to two solutions: after finding a second one, further counting cannot change the rejection decision. The two-star solver also reports whether its search finished within the node budget.
Does a unique solution mean no guessing?
No. A puzzle can be unique while the available logical techniques cannot finish it. That is why generation also runs a separate human-style grader. One-star grading uses single candidates, elimination and groups of confined units. Two-star grading compares possible non-touching pairs. Binary grading uses signs, pairs, sandwiches and balanced-line counts; classic Takuzu also uses distinct-line deductions.
Hard Tango grading may test a single-cell hypothesis and reject it when rule propagation proves a contradiction. That is a bounded proof by contradiction, rather than accepting a plausible move. It is more demanding than basic visual deductions. The released classic Takuzu library excludes hypothesis deductions. A grader passing does not imply every player will find the next step obvious.
Four reproducible practice samples
The table was generated on 2026-11-04 from the released practice libraries. Each row checks one sample, not a new audit of the entire site. Source links identify the exact original board; full answers stay out of this report.
| Sample | Solutions | Logical grader |
|---|---|---|
| Tango, 6×6, easy #1 | 1 | Complete |
| Takuzu, 6×6, easy #1 | 1 | Complete |
| One-star Star Battle, 6×6, easy #1 | 1 | Complete |
| Two-star Star Battle, 10×10, classic #1 | 1 | Complete |
Two controls that must fail
- Contradictory Tango: give a 6×6 board three suns in its first three cells. The solver returns 0 solutions because the no-three rule is already broken.
- Ambiguous Tango: give a 6×6 board no symbols and no relationship clues. The solver finds 2 solutions and stops. That means at least two, not exactly two.
These controls check that the pipeline distinguishes an impossible board from one with too little information. They do not prove that every possible solver defect has been ruled out.
Reproduce the report
From a checkout of the repository with its dependencies installed, run node scripts/build-insights.mjs to rebuild the five Tango checkpoints, three counting proofs and the verification samples. Then run npx vitest run tests/insights.test.ts to replay the setup deductions and independently check the counting arguments.
The report builder uses the released boards, the one-star solver and grader, binary solver and grader, and two-star solver and grader. The daily schedule test checks every scheduled board has one solution matching the stored answer. The Takuzu tests include a separate row-enumeration checker, and two-star tests independently validate final placements.
What these checks cannot establish
- Solver results depend on correctly implementing the intended rule set. Tango and classic Takuzu deliberately differ on distinct lines.
- Logical graders cover a defined set of techniques. Failure can mean that those techniques are insufficient, even when a different human proof exists.
- Difficulty labels describe the grader's techniques; they are not calibrated predictions of human solve times.
- A unique original puzzle does not mean a player's current partial board is correct.
- The four report samples do not replace the full library and schedule tests.
For the separate historical study of generation acceptance rates, see the 12,000-seed Star Battle benchmark. Acceptance rate is not the probability that a random grid is unique.
Try the five Tango next-move checkpoints, follow three Star Battle counting proofs, or play today's daily trio.