Solving and Generating Hashi Puzzles with a SAT Solver

Niels Glodny · 3 November 2026

The game has to do two things with puzzles that are hard for a computer. It has to solve them, for the Show solution button and for hints. And it has to generate new ones that have exactly one solution: the custom boards on your device and the daily puzzle on the server. Both go through a SAT solver. This article explains how a Hashi puzzle becomes a SAT problem, the one trick that makes it fast, and how the generator uses it.

The code is written in Rust. In the browser and in the apps it runs as WebAssembly inside a web worker, so the board stays responsive while the solver works.

Hashi as a SAT problem

A SAT solver takes a formula made of Boolean variables and finds values for them that make the whole formula true, or reports that there are none. The formula is a list of clauses, and every clause has to hold. Each clause is an OR of variables or their negations. Modern solvers handle millions of clauses.

To use one, every rule of Hashi has to be written as clauses.

Variables

Each pair of islands that could be joined gets two variables, x₁ and x₂. x₁ means “there is at least one bridge”, x₂ means “there is a second bridge”. The clause ¬x₂ ∨ x₁ says the second bridge needs the first. That leaves three states: no bridge, one bridge, two bridges.

No crossings

For every two connections that would cross, one clause says they cannot both exist:

Only the first variables are needed, because a double bridge always has its first variable set.

The numbers

An island has at most four possible connections, so at most eight variables. We forbid every combination of those variables whose count is not the island’s number, one clause per combination. For a set s of variables that should not be the true ones:

where b(i) are the variables of island i. With eight variables there are at most 256 combinations, so this simple encoding is small enough.

Connectivity, added only when needed

The rule that all islands connect is the expensive one. The standard way to encode it is reachability: for each island and each step, a variable saying whether the island can be reached from a fixed start island in that many steps. That needs on the order of n² variables and clauses for n islands.

We measured it. For a 30×30 board with 156 islands, the full encoding has 198,000 clauses. Without the connectivity part, the same board has about 18,000. For a 60×60 board with 616 islands, it is 3.2 million clauses against about 100,000.

So the solver does not get the connectivity rule up front:

1. Solve with only the variables, crossings and numbers.
2. Check the result with a depth-first search. If all islands are connected, it is the solution.
3. Otherwise, for each separate group of islands, add one clause: at least one of the possible bridges leaving this group must exist.
4. Solve again, and repeat.

The added clauses are always true in a real solution, since a connected network must have a bridge leaving every group that is not the whole board. So they never remove the right answer, and each round rules out the wrong one the solver just found. In practice it takes one to five rounds.

The same idea, adding connectivity constraints only once a candidate breaks them, is the core of the branch-and-cut solver by Coelho, Laporte, Lindbeck and Vidal (2019), which uses integer programming instead of SAT.

How fast it is

Five generated puzzles per size, native release build on a laptop with an AMD Ryzen 7 5700U, using the Splr solver. Clauses are counted without the connectivity clauses.

As WebAssembly in a browser the same code is slower, which is why a 60×60 custom board can take a while to appear.

Checking that a solution is unique

To check a puzzle, solve it once. Then add a clause that forbids exactly that assignment of bridge variables, and solve again with the same connectivity rounds. If no connected solution comes back, the first one was the only one.

Generating puzzles

The generator builds the solution and the puzzle together, so every puzzle has at least one solution by construction. The work is in making sure it has only one.

1. Start with two islands next to each other in the middle of the board, joined by one or two bridges.
2. Pick a random island and a free spot in a straight line from it. The spot may not touch another island or lie across an existing bridge. Short distances are strongly preferred, since long bridges look odd.
3. Put a new island there with a single bridge back, and add one to the old island’s number.
4. Repeat until at least 17% of the cells are islands: 17 on a 10×10 board, 612 on 60×60.

A new island can make the solution ambiguous. The typical case is a cycle of islands where you could add a bridge on every other connection and remove one on the others: every number stays the same, so there are now two solutions. After each new island, a depth-first search looks for such a cycle through it. When it finds one, two neighbouring connections in the cycle become double bridges, and the numbers are raised to match. A double bridge cannot take another bridge, so the swap no longer works.

That local check does not catch everything, for example a second solution that differs in connectivity. So islands are added in batches, and after each batch the full uniqueness check runs. If it passes, the next batch is twice as large. If it fails, the batch is thrown away and the next one is half as large.

The generator does not rate difficulty, and it does not check that a puzzle can be solved without trial and error. What it guarantees is one solution.

Solvers

Splr is written in Rust and compiles to WebAssembly, which is why the game uses it. The rules go into the solver in DIMACS, the standard input format for SAT solvers, so the command-line version can also hand them to CaDiCaL or MiniSat instead.