Stardew Valley is a well known game that probably does not require introducton.

In Stardew Valley there is a tile Scarecrow that protects the crops around it from crows. It does so in the following limited range:

There is also another tile: a sprinkler, waters its own tile and the 4 tiles that share an edge with it (up, down, left and right). Diagonal tiles are not watered. A tile under a sprinkler cannot hold a crop, but it needs no water either.

Ever wondered how many crops is it possible to tuck in into a scarecrow range, such that each is covered by at least 1 sprinkler?

Lets find out!

SAT

A SAT solver receives a list of rules over true/false variables, written in conjunctive normal form (CNF). Each rule (a clause) says "at least one of these variables is true", where a variable can also appear negated, as in "x is false". The solver returns one of two answers:

• SAT: a true/false value for every variable that satisfies all clauses. Here that is a valid field layout.
• UNSAT: a proof that no such values exist. Here that means no valid layout exists.

An optimization question becomes a series of yes/no questions. "Is there a layout with at most K sprinklers?" is asked for different values of K.

Sprinklers: encoding

One variable per tile: x[r,c] is true if tile (r, c) holds a sprinkler and false if it holds a crop.

Water rule. Every tile must be a sprinkler or share an edge with a sprinkler. For each tile p this is one clause:

x[p] ∨ x[up of p] ∨ x[down of p] ∨ x[left of p] ∨ x[right of p]

Neighbors outside the field, and the scarecrow, are left out of the clause (or equivalently, set to False).

Count rule. At most K of the 248 variables may be true. A rule like this is called a cardinality constraint. It is turned into clauses with the totalizer encoding. That encoding adds helper variables that count the true variables in a binary tree and forbids any count above K.

Optional constraint - symmetry:

For a layout that is the same when mirrored left to right, each pair of mirrored tiles must match: 

x[r,c] ↔ x[r,20-c]     written as two clauses: (¬x[r,c] ∨ x[r,20-c]) and (x[r,c] ∨ ¬x[r,20-c])

Feed it all to a SAT solver

The solver was run to find the boundary where solution starts to exist:

K (at most)	Answer	Time (s)
58	UNSAT	79.1
59	SAT	21.3

59 is optimal. K = 59 is SAT, so a layout with 59 sprinklers exists. K = 58 is UNSAT, so no layout with 58 or fewer sprinklers exists. The rule says "at most", so this UNSAT answer covers every smaller number too.

Together, the two answers prove that 59 is the optimal result

How does it look like?

Light blue: sprinkler (59). Green: crop (189). Pink: scarecrow.

But it looks ugly...

Let's try to constraint horizontal symmetry and check if we still can get 59 with it (yes we can):

The hops problem

The hops crop has an issue: player cannot pass through it.

Moreover: the scarecrow tile is not walkable and sprinklers are not walkable.

So even if one tries to use tiling such as the above, the player will simply be not able to collect the crops!

Another approach is required:

Variables. x[p] is true if tile p is a sprinkler. h[p] is true if tile p is a hop. If both are false, the tile is a crop.

Type rule. A tile cannot be both: ¬x[p] ∨ ¬h[p].

Water rule. The same rule as in section 3.

Reachability rule. Whether a tile can be reached on foot depends on the whole layout, so it cannot be written as one short clause. It is built step by step, as in dynamic programming. A helper variable reach[p,d] means "tile p is a crop that the player can reach from outside in at most d steps".

Essentially the DP formulas are: reach[p,d] = reach[p,d-1] or reach[any neighbor of p,d-1] (where reach[boundary,0]=true):

• Step 0. reach[p,0] may be true only for crops that share an edge with the outside: ¬reach[p,0] ∨ ¬x[p] and ¬reach[p,0] ∨ ¬h[p].
• Step d. reach[p,d] may be true only if p is a crop, and p or one of its neighbors was reached at step d−1: ¬reach[p,d] ∨ reach[p,d-1] ∨ reach[up of p,d-1] ∨ … ∨ reach[right of p,d-1].
• Depth. The last step is D = 248, the number of tiles. A walking path inside the field can never be longer than that, so no valid layout is cut off.
• Fewer variables. reach[p,d] is created only if d is at least the walking distance from the outside to p on an empty field. A tile can never be reached in fewer steps than that.

Hop rule. A hop that does not touch the outside must share an edge with a reachable crop:

¬h[p] ∨ reach[up of p, D] ∨ reach[down of p, D] ∨ reach[left of p, D] ∨ reach[right of p, D]

After doing a run for a while a solution emerges - It's possible to have 98 hops:

Here green tiles can be filled with any walkable crop because they are covered by sprinklers

Note however that 98 hops is therefore the best known result but not proven to be optimal. No run proved that 99 hops is impossible (the UNSAT), so 98 is a lower bound, not a proven maximum. The step-by-step reachability rule makes these problems much harder than the sprinkler problem. Proving that a hop count is impossible did not finish in practice. If you can do better, let me know!

Code

All the code is packaged for inspection, python-sat and matplotlib must be installed

Run the following commands:

python.exe sprinklers_sat.py 59
python.exe sprinklers_sat.py 58
python.exe sprinklers_sat.py 59 hsym
python.exe hops_sat.py
python.exe hops_sat.py hsym
python.exe hops_min_sprinklers.py

TODO: Similar code can be ran for improved 8 tile and iridum sprinklers, I wonder how the optimal result may look for those?

Opinion

It's quite awe-inspiring that computer can produce answers with beautiful structure. In the 59-sprinkler layouts, sprinklers line up along diagonals in a near-perfect lattice, close to the knight's move tiling that waters an endless field with no overlap. At the curved edge of the field that lattice cannot fit, and the solver bends it, shifting rows and inserting pairs so that the round boundary closes cleanly. In the 98-hop layout, hops crowd around narrow green corridors. These walkways reach from the outer edge almost to the scarecrow and leave just enough room to reach every hop. The corridors were designed by a computer.

The amazing thing here that a general-purpose reasoning engine such as SAT solvers exist and find the hidden structure in the problem.