Note that traditional SAT and SMT solvers are quite inefficient at computing flood-fills.
The ASP specifications it uses to compute optimal solutions are surprisingly short and readable, and look like:
#const budget=11.
horse(4,4).
cell(0,0).
boundary(0,0).
cell(0,1).
boundary(0,1).
% ...truncated for brevity...
cell(3,1).
water(3,1).
% ...
% Adjacent cells (4-way connectivity)
adj(R,C, R+1,C) :- cell(R,C), cell(R+1,C).
adj(R,C, R-1,C) :- cell(R,C), cell(R-1,C).
adj(R,C, R,C+1) :- cell(R,C), cell(R,C+1).
adj(R,C, R,C-1) :- cell(R,C), cell(R,C-1).
% Walkable = not water
walkable(R,C) :- cell(R,C), not water(R,C).
% Choice: place wall on any walkable cell except horse and cherries
{ wall(R,C) } :- walkable(R,C), not horse(R,C), not cherry(R,C).
% Budget constraint (native counting - no bit-blasting!)
:- #count { R,C : wall(R,C) } > budget.
% Reachability from horse (z = enclosed/reachable cells)
z(R,C) :- horse(R,C).
z(R2,C2) :- z(R1,C1), adj(R1,C1, R2,C2), walkable(R2,C2), not wall( R2,C2).
% Horse cannot reach boundary (would escape)
:- z(R,C), boundary(R,C).
% Maximize enclosed area (cherries worth +3 bonus = 4 total)
#maximize { 4,R,C : z(R,C), cherry(R,C) ; 1,R,C : z(R,C), not cherry( R,C) }.
% Only output wall positions
#show wall/2.