Algorithm for a 2D path-finding puzzle

Question

I am trying to find an algorithm for finding an optimal solution to a puzzle of a given format. The 7 by 6 puzzle board is made out of the following pieces:

The tears are as follows:

Tears and grommets can be rotated and moved around the board, but spools, tie-offs and blockers cannot.

A simple example of the puzzle in it's starting state is:

While a more complicated version and a possible solution is:

The puzzle is scored by how many pieces are used in the solution (more is better) and how quickly the puzzle is solved.

I have so far written functions to detect and read in the board, as well as a function to check that the board is valid.

In order to solve the board, I have so far tried a brute force method, which randomly shuffled and rotated the movable pieces in the puzzle and then checked if the result was a valid solution, but this was fairly slow even for the simple boards, and extremely slow for more complex boards, and of course, did not come up with an optimal solution.

I then refined it a bit by excluding obvious wrong piece placements, but this was still over a second for small boards, and anywhere from 5 to 30 seconds for larger boards, and was also not an optimal solution.

I have heard about possibly using various path finding algorithms such as Djikstra's or A* but I'm struggling to see how these algorithms can be used to find the longest valid path, especially when branching pieces such as the 'T' and '+' pieces come into play.

Any help would be much appreciated!

Answer 1

One approach would be to bring out the big hammer and try using a SAT solver. You introduce boolean variables $x_{\ell,p,o}$, which is true if piece $p$ is placed in orientation $o$ in location $\ell$ on the grid. Then, you write down boolean clauses to encode the conditions for a grid to be valid. Finally, you do binary search: given $k$, you try to find a placement that has score at least $k$ (by writing boolean clauses to force the score to be at least $k$ and then using a SAT solver to test whether there exists an assignment to the variables that satisfies all of the clauses), and then do binary search on $k$. This might be effective, or it might be slow; it's hard to predict, so the only way to find out is to try it.

The trickiest part of encoding into SAT will probably be calculating the score. I suspect it will be useful to introduce extra boolean variables $y_{\ell}$, which is true if the piece at location $\ell$ is connected to the spool. Then, write constraints that capture the relationship between the $x$'s and $y$'s.