Solving and Generating Hashi Puzzles using SAT Solvers

At the core of our Hashi game is the algorithm that solves and generates the puzzles. The logical nature of the puzzles make them both fun to solve for humans but also difficult to solve (and especially generate) for computers. We use techniques based on the Boolean Satisfiability Problem (SAT) to efficiently solve and generate Hashi puzzles of varying difficulty.

This article describes the technical approach, including the encoding of puzzle constraints as Boolean clauses, the lazy connectivity optimization, and the WebAssembly implementation that enables efficient client-side computation.

What are Hashi Puzzles?

Hashi (橋, meaning "bridge") or Hashiwokakero (橋をかけろ, "build bridges") is a Japanese logic puzzle where players connect numbered islands with bridges according to specific rules. Each island's number indicates how many bridges must connect to it (only horizontal and vertical bridges are allowed), and the final configuration must form a single connected graph without crossing bridges. For example, a simple solved Hashi puzzle might look like this:

The Challenge: Why Hashi is Computationally Hard

Hashi puzzles are NP-complete, belonging to the same computational complexity class as the traveling salesman problem and circuit satisfiability. No known polynomial-time algorithm can solve all possible Hashi instances.

Most of the complexity arises from the connectivity requirement and the requirement to prevent bridge crossings. Beyond satisfying the bridge count constraints for each island, the solution must form a connected graph. Each bridge placement affects the global network structure, and removing a single bridge can isolate entire sections of the puzzle or make it impossible to satisfy other islands' constraints.

While NP-complete problems lack efficient general solutions, practical instances can often be solved efficiently using specialized techniques and modern algorithms.

Approach: Reduction to Boolean Satisfiability

The implementation transforms Hashi puzzles into Boolean satisfiability (SAT) problems, leveraging decades of research in efficient SAT solving algorithms.

The transformation encodes all puzzle constraints as Boolean clauses. A SAT solver then searches for a variable assignment satisfying all clauses simultaneously, which corresponds to a valid puzzle solution.

Encoding Bridges as Boolean Variables

Here's how we translate bridges into logic. Each potential bridge between two adjacent islands gets two Boolean variables: $v_{i,1}$ and $v_{i,2}$. This lets us encode three possible states:

• No bridge: $¬v_{i,1} ∧ ¬v_{i,2}$ (both variables false)
• One bridge: $v_{i,1} ∧ ¬v_{i,2}$ (first true, second false)
• Two bridges: $v_{i,1} ∧ v_{i,2}$ (both variables true)

We also add a constraint ensuring the second bridge can only exist if the first one does. this eliminates redundant solutions and improves solver performance significantly.

Bridge Count Constraints

For each island that needs exactly $c_i$ bridges, we generate clauses that eliminate all configurations not summing to $c_i$. If island 5 needs exactly 3 bridges, we create Boolean clauses that rule out having 1 bridge, 2 bridges, 4 bridges, etc.

Mathematically, for each node $n_i$ with bridge set $b(n_i)$, we add:

$\bigwedge_{s \subseteq b(n_i), |s| \neq c_i} \left(\bigvee_{x \in s} \overline{x}\right) \lor \left(\bigvee_{x \in b(n_i) \setminus s} x \right)$

This creates a constraint system ensuring every island has exactly the required number of bridges.

Preventing Bridge Crossings

All possible bridge intersections are precomputed. For each pair of intersecting bridges, a clause prevents both from existing:

$\bigwedge_{\forall b_i, b_j \text{ intersect}} (\overline{v_{i,1}} \lor \overline{v_{j,1}})$

If two bridges would cross, at most one can exist in the solution.

Lazy Connectivity Optimization

The traditional approach to ensure connectivity encodes the reachability relation directly, requiring O(n³) clauses. This becomes impractical for large puzzles.

Thus, we use a lazy connectivity approach inspiried by incremental SAT solving:

1. Solve without connectivity: First, generate a solution satisfying only bridge counts and non-crossing constraints
2. Check connectivity: Use a simple and fast graph traversal to see if all islands are connected
3. Add targeted constraints: If disconnected, add minimal clauses to eliminate that specific disconnected configuration
4. Iterate: Repeat until finding a connected solution

Most puzzle instances require only one or two iterations. Instead of O(n³) clauses upfront, constraints are added incrementally as needed.

For each disconnected island group $I$, the following clause is added: $\bigvee_{b_i \in E} v_{i,1}$ where $E$ contains all bridges connecting the isolated group to the rest of the puzzle.

Performance Analysis

Benchmarks on an Apple M1 Max processor demonstrate the following performance characteristics:

• Traditional approach: Performance degrades significantly beyond 50 islands
• Lazy connectivity: Solves 1000+ island puzzles in under a second

The lazy connectivity approach scales substantially better than traditional methods for large problem instances.

WebAssembly Implementation

The core implementation is written in Rust for performance and safety. The SPLR SAT solver, also written in Rust, provides the Boolean satisfiability engine.

To make it feasible to play both on mobile and the web, the entire solver compiles to WebAssembly (WASM), enabling near-native performance in web browsers. The solving process follows this sequence:

1. JavaScript sends the puzzle string to our Web Worker
2. WebAssembly initializes the Rust-compiled solver
3. Rust code parses the puzzle and generates Boolean clauses
4. SPLR solver finds a satisfying assignment using CDCL algorithms
5. Connectivity checker verifies the solution connects all islands
6. Results are serialized back to JavaScript for display

The Web Worker architecture maintains UI responsiveness during solving operations.

SAT Solver Options

SAT solvers use a standard interface called DIMACS for clause and variable input. Thus, the Hashi solver can switch between different backends:

• Splr: Pure Rust SAT solver that can be compiled to WebAssembly
• CaDiCalSolver: High-performance external solver used through its CLI
• MinisatSolver: Alternative external solver option that is widely available

The web version runs entirely client-side. Puzzle data remains in the browser, and the application functions offline after initial loading.

Puzzle Generation

Generating Hashi puzzles presents additional challenges beyond solving. The generator begins with a minimal two-island puzzle and iteratively adds islands while maintaining unique solvability.

The primary challenge involves detecting non-unique cycles—bridge configurations that allow multiple solutions. Depth-first search identifies these patterns, and the generator modifies the puzzle to eliminate ambiguity while preserving the overall structure.

The generator produces puzzles with:

• Guaranteed unique solutions: Verified through multiple SAT solver runs
• Calibrated difficulty: Based on clause propagation complexity
• Balanced distribution: Even spatial distribution of islands and constraints

Technical Significance

This implementation demonstrates the practical application of several computational techniques:

• Boolean satisfiability theory
• Constraint satisfaction problems
• Graph connectivity analysis
• WebAssembly compilation technology

These techniques have applications in circuit verification, software model checking, automated planning, and scheduling optimization.

Conclusion

Modern SAT solvers can solve complex logical problems in milliseconds that would have been computationally intractable decades ago, representing significant progress in automated reasoning.

The puzzle solver and generator demonstrate how theoretical advances in computational complexity and SAT solving translate into practical applications. The lazy connectivity optimization illustrates how domain-specific insights can substantially improve general algorithmic approaches.

The WebAssembly implementation enables efficient client-side solving of NP-complete problems at near-native speeds, making advanced computational techniques accessible in standard web browsers.