How the solver works

The solver at /solve/ does two jobs. It reads a picture of a board, and it finds paths that connect every pair of dots and fill every cell. Both jobs run inside your browser, so the image, the board and the answer never leave your device. This page walks through each step, then shows how the same ideas check this site's own puzzles.

Reading the picture

Image work runs in a background worker, a separate thread that keeps the page responsive and stops at once when you press Cancel.

Loading and finding the grid

The solver accepts JPEG and PNG files up to 20 MB and 40 megapixels. It checks the file header before decoding anything, then scales the image so its longest side is at most 1,600 pixels.

For a screenshot, the solver looks for the board's grid lines. It scans each row of pixels and counts how many look like part of a thin gray line. Such a pixel is neither black nor bright, is nearly colorless, and is a little lighter than the pixels a few rows above and below. The solver then looks for the longest run of these lines with even spacing, between 3 and 21 lines, which means 2 to 20 cells. It repeats the search for columns and accepts the result only if the cells come out close to square.

The outer lines give the four corners, and the line count gives the rows and columns. The test is cautious on purpose. When it isn't sure, it asks you to drag four corner handles onto the board and enter the size yourself. Photos of another screen often end up there, because perspective and glare make the lines uneven. Photographing another screen has tips.

Flattening the board

From the four corners, the solver calculates a perspective correction that maps a tilted board onto a flat square. It redraws the board at 48 pixels per cell, blending the nearest source pixels for each new one. After this step every cell is the same size, whether the source was a straight screenshot or a photo taken at an angle.

Spotting dots and grouping colors

For each cell, the solver samples only the middle 30 percent of its width and height, which keeps grid lines and borders out of the way. A pixel counts as part of a dot if it is bright and either strongly colored or very light. When at least 65 percent of that window passes, the cell holds a dot. This is why the solver wants an unplayed board. A drawn path runs straight through cell centers and can look like a dot.

Each dot's average color is then scaled so its strongest channel matches every other dot's. A dim red and a bright red look alike after that, which helps with uneven lighting. Dots with close colors form a group, and each group gets a letter. A group without exactly two dots is circled on the board and blocks solving until you fix it.

The one mistake the solver can't catch is a pair that is missing entirely. A board with one pair fewer still looks consistent, so you always check the dots before solving. Fixing detection mistakes shows how.

Turning the board into rules

Z3, the engine that does the solving, never sees a picture. It sees a long list of yes-or-no questions and rules that tie them together. There are two kinds of question:

• For every cell and every color, "is this cell that color?"
• For every pair of side-by-side cells and every color, "does that color's path use the link between them?"

A 10 × 10 board with 8 colors has 800 cell questions. It has 180 links between neighboring cells, so there are 1,440 link questions. Four rules connect them:

1. Every cell gets exactly one color. Holes get none.
2. A cell with a dot is the dot's color.
3. A dot's cell uses exactly one link of its color. Every other cell of that color uses exactly two.
4. A link can belong to a color only if both of its cells are that color.

Rule 3 carries most of the weight. A path leaves its dot in one direction, and every cell along the way has one way in and one way out. Two paths can't share a cell, because a cell has only one color. A path can't run through another color's dot, because rule 2 fixes that cell's color. In the board above, Blue's dot at row 1, column 4 uses only the link to row 1, column 5, and the Blue cell at row 3, column 4 uses two.

The loop problem

Those rules look at one cell at a time, and that leaves a gap. A color can satisfy them with a real path plus a separate closed loop, because every cell in a loop also has exactly two links.

Ruling out every possible loop in advance would take a rule for every region of the board, far too many to write down. So the solver checks each answer Z3 returns. It traces every color from one dot to the other, and any cells of that color left over must form loops. For each loop it adds one rule. If this color uses any cell in that region, its path must cross the region's border at least twice, which ties the region to the rest of the path. Then it asks Z3 again, and repeats until no loops remain. The result screen reports how many of these rules were added as "connectivity cuts".

When an answer comes back with no loops, separate code walks every path again. It confirms that each path runs between its own two dots, steps only between neighbors, never repeats a cell or enters a hole, and that the board is filled. Only then does the screen say Solved.

Z3 in your browser

Z3 is an open-source solver from Microsoft Research. It makes a tentative choice, follows the consequences through the rules, and when it reaches a contradiction it records a new rule so it never tries that combination again. Those learned rules let it skip huge parts of the search.

The browser edition runs Z3 compiled to WebAssembly. It is about 8 MB to download and 35 MB unpacked, so the solver fetches it only when a solve starts and checks its SHA-256 fingerprint before running it. Z3 runs in its own worker, so Cancel stops it at once. It needs memory shared between threads, which browsers allow only on specially isolated pages, so the solver has a page of its own. Browser support and privacy lists the requirements.

Each solve has a time limit of 10, 30 or 60 seconds (30 by default). Out of time means Z3 hadn't finished, and says nothing about whether the board can be solved. No solution means Z3 proved that no answer satisfies the rules for the board as entered, usually because of a missed or extra dot. Timeouts and "no solution" covers both.

Proving a puzzle has one answer

The browser solver stops at the first solution it finds. The site's puzzles and lesson diagrams go further, using the project's Python toolkit, which builds the same model of cells, links and rules. After it finds one solution, it adds a rule that at least one link must differ from that solution, and asks again. If no second solution exists, the first was the only one. If a second turns up, the puzzle generator discards the board.

This is the exact version of the uniqueness trick. A player assumes the puzzle has one answer and uses that to rule out certain shapes. The solver proves it.

Cheap checks before solving

The Python toolkit runs quick tests before it builds any rules. It limits each color to cells it can reach without passing through another color's dot, and removes a color from any cell where it couldn't have two usable neighbors. Another test uses checkerboard coloring.

Shade the cells like a checkerboard, with row 1, column 1 dark. Every step along a path moves to the other shade. A path whose dots are both dark covers one more dark cell than light. A path with one dot on each shade covers equal numbers. So on a board that must be filled, the pairs with both dots dark, minus the pairs with both dots light, must equal the dark cells minus the light cells.

Blue's dots at row 1, column 1 and row 4, column 1 are on opposite shades. Orange's dots at row 1, column 3 and row 4, column 4 are both dark. The paths would need one more dark cell than light, and the board has eight of each. The toolkit rejects this board without searching. The browser solver skips the test, but Z3 reaches the same verdict and reports No solution. Checkerboard parity shows how to use the idea by hand.

Bridges, cells and channels

The browser solver reads only plain square and rectangular boards. The Python toolkit also handles bridges, hex grids, warps and other shapes, and to do that it separates two ideas. A cell is a place on the board. A channel is room for one path to pass through. On an ordinary board each cell has one channel.

A bridge cell has two channels, one across and one up and down, so two colors can cross there. The rules are written for channels. Each channel holds at most one color, and by default one color can't use both channels of the same bridge. A bridge counts as filled when at least one of its channels is used. The parity test applies only when every cell has exactly one channel, so boards with bridges skip it. Bridges covers solving them by hand.

A second solver that thinks like a player

The exact solver produces an answer but no reasons. Puzzle walkthroughs come from a second solver that works the way a careful player does. It grows paths from their dots and only makes a move it can justify:

• Forced move. A path end has only one open cell to go to.
• Squeeze. An empty cell has exactly two usable neighbors, so the path through it must use both.
• Looking ahead. For a path end with several options, it tries each one and follows the forced moves it causes. It rejects the option if that leaves a cell nothing can fill, boxes a path in, cuts a color off from its partner, or seals a pocket no color can reach. If exactly one option survives, that becomes the move.

When one level of trying isn't enough, it looks one level deeper, checking inside a trial whether some path end has no option left that survives. It never goes further than that, and it never guesses.

A generated board is published only when both solvers agree. The exact solver proves there is one answer, and the player-style solver finishes without guessing. Its moves become the walkthrough, which an editor rewrites in plain language, and the amount of looking ahead it needed sets the difficulty. Boards that only the exact solver can finish would force a person to guess, so they never reach the puzzle list.