Can this Arrow-Ring puzzle be encoded as an integer programming problem?
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).


Black.
Horizontal.
Vertical.
Top-right turn.
Right-bottom turn.
Bottom-left turn.
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.