Can this Arrow-Ring puzzle be encoded as an integer programming problem?

Question

I would like to write a solver for these kind of Arrow-Ring puzzles. However, I can't encode all the constraints correctly.

I noticed that Sudoku can be solved using integer programming and I am hoping it can be done for this kind of puzzle as well. Let's take a look at the rules:

• Draw a line to make a single loop. Lines pass through the centers of cells, horizontally, vertically, or turning.
• The loop never crosses itself, branches off, or goes through the same cell twice.
• The numbers show how many black cells there are in the direction of the arrow.
• The loop does not pass through the black cells or the cells with numbers, and black cells cannot touch horizontally or vertically.

The first constrant seem the most difficult, that we should require a single closed loop. And I wonder if integer programming is even the best way to solve these, but it's a start.

The third constraint (with numerical hints) is the most clear and for simplicity, they could also be replaced by black squares. However, if you already know how to encode these as integer programming problems, go for it.

Lastly, are there other algorithms that are efficient for finding loops in graphs with constrants? Wikipedia suggests this could be a Hamiltonian Path or an SAT problem.

Answer 1

You can encode this problem using a SMT solver like z3, which translates it to a SAT instance.

Let each $c_{x, y}$ be a free variable for a cell that isn't an arrow. A cell can be one of the following (encode them as integer states or as one-hot states).

1. Black.
2. Horizontal.
3. Vertical.
4. Top-right turn.
5. Right-bottom turn.
6. Bottom-left turn.
7. Left-top turn.

If you can find an assignment of the above for each $c_{x, y}$ variable, you've found a solution.

Obviously we still need to encode all requirements. First introduce four helper variables for each $c_{x, y}$ to see if it is connected to its top/left/bottom/right neighbour. This is a bit laborious, but it comes down to logic statements such as "I'm vertical and bottom neighbour is either vertical, top-right turn or left-top turn".

Introduce a requirement that each cell $c_{x, y}$ must be connected to at least one neighbour.

Introduce a requirement for each arrow block to say that the number of cells equal to black in the direction it's pointing in must match its number.

Introduce a requirement that no two adjacent $c_{x,y}$ are black.

With all these requirements you know that each free cell is either black, or part of a connected loop. The final struggle is to ensure that there is a single connected loop. This can be done by assigning a single free variable to denote a leader cell, and then using the previous established connections to ensure that each cell is either black or the leader cell, or connected to the leader cell, or connected to a cell connected to the leader cell.

---

All in all this is quite a tricky and laborious translation into an SMT solver. If you intend to implement this I strongly suggest reading through some example problems from this excellent z3 guide. It has a ton of translations of various problems into a format a SMT solver can understand.