Lately I've been toying with an automatic solver for the Android/iPhone game Flow.

In this game, you start with several pairs of squares on a grid, and you have to connect each pair, without crossing the paths, and by using every square on the grid. Here's a simple 7x7 example (the hardest boards in the game are 11x13).


Beginning layout


Finished board

In most cases, a few simple rules can all but solve the problem. For example, if a node only has one uncovered exit, it must extend that way, and if extending in a direction would make a part of the board unreachable, then that move is forbidden. But is there a more general way? I've been trying to figure out if it is a specific case of a general graph algorithm, perhaps some kind of Path Coloring.

Note that the game presents other variants of the problem, such as a hexagonal grid, and 'warps' that connect squares on opposite sides of the board. Also, as far as I can tell, there is only ever one correct solution. I'd also be interested in how they can generate the starting positions.

  • 1
    $\begingroup$ related: ​ ​ ​ my question ​ and ​ domotorp's question ​ ​ ​ ​ ​ ​ ​ ​ $\endgroup$
    – user12859
    Jan 13, 2018 at 11:51
  • $\begingroup$ @RickyDemer Thank you, you're right, my cursory searches didn't turn those up. I'll have to investigate those papers. $\endgroup$
    – Widjet
    Jan 14, 2018 at 11:48

1 Answer 1


I suggest formulating this as an instance of SAT.

You can formulate this as an instance of SAT by thinking of it as trying to color each square in the grid with a color. For each color, arbitrarily designate one of the two endpoints as the "starting position" for that color, and the other endpoint as the "ending position". Define boolean variables $x_{i,j,c,k}$, with the intended meaning that $x_{i,j,c,k}$ is true if grid square $(i,j)$ is colored $c$ and is the $k$th square along the path from the starting position for $c$ to the ending position for $c$.

You can write down a boolean formula representing the constraints on the variables $x_{i,j,c,k}$ that must hold, for this to be a valid solution to the puzzle. For instance:

  • If $x_{i,j,c,k}$ is true, then either $(i,j)$ must be the end position for color $c$, or else $x_{i',j',c,k+1}$ must be true for some square $(i',j')$ that is adjacent to $(i,j)$. Moreover, this is true for exactly two squares (not more, not less), unless $(i,j)$ is the starting position, in which case it is true for exactly one square.

  • For each square $(i,j)$, exactly one of the $x_{i,j,c,k}$ is true.

  • If $(i,j)$ is the starting position for color $c$, $x_{i,j,c,0}$ is true. If $(i,j)$ is the ending position for color $c$, one of $x_{i,j,c,k}$ must be true.

And so on. This ensures that the solution to the formula contains a path that starts at the starting position for color $c$ and ends at the ending position.

Then, feel this boolean formula to an off-the-shelf SAT solver and ask it to find a solution.

This may be an effective solution for the puzzle sizes you mention. I expect it may be more effective than trying to write your own custom rules, as SAT solvers embody many clever strategies built up over decades of research to try to find solutions for these kinds of combinatorial questions. At least, it should be pretty easy to implement in just a few hours and see how well it works.

Apparently, this puzzle is NP-hard, so you should not expect to find a polynomial-time solution. This suggests to me that a SAT solver might be a reasonable approach.

  • $\begingroup$ How could he write down such a formula? ​ (I don't see how to force the $\hspace{1.91 in}$ non-existence of disconnected cycles.) ​ ​ ​ ​ $\endgroup$
    – user12859
    Jan 13, 2018 at 11:47
  • $\begingroup$ @RickyDemer, oops, you're right. When I get a chance I'll update my answer with a correct construction. $\endgroup$
    – D.W.
    Jan 13, 2018 at 19:13
  • $\begingroup$ @RickyDemer, see updated answer. I think this should do it. Widjet, see updated answer. I think this should now provide a reasonable algorithm for your problem. $\endgroup$
    – D.W.
    Jan 15, 2018 at 18:33
  • $\begingroup$ I should have accepted this months ago, I'm sorry. It appears this is approximately the approach used by the papers mentioned by @RickyDemer in the comment on the question. I don't know if I'll ever get around to trying to implement it myself, but it's probably the right answer. $\endgroup$
    – Widjet
    Oct 17, 2018 at 7:13
  • 1
    $\begingroup$ @tgm1024, you could try cs.stackexchange.com/q/30790/755, en.wikipedia.org/wiki/Tseytin_transformation, cs.stackexchange.com/q/12087/755. $\endgroup$
    – D.W.
    Nov 4, 2018 at 7:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.