Yes, this is the major challenge with solving them with SAT. You can make your solver check and reject these horseless pockets (incrementally rejecting solutions with new clauses), which might be the easiest method, since you might need iteration for maximizing anyways (bare SAT doesn't do "maximize"). To correctly track the flood-fill flow from the horse, you generally need a constraint like reachable(x,y,t) = reachable(nx,ny,t-1) ^ walkable(x,y), and reachable(x,y,0)=is_horse_cell, which adds N^2 additional variables to each cell.

You can more precisely track flows and do maximization with ILP, but that often loses conflict-driven clause learning advantages.

Good point. I don't think the puzzles do this and if they would, I would run a pre-solve pass over the puzzle first to flood fill such horseless pockets up with water, no?