In the answer to an earlier question "SAT algorithm for determining if a graph is disjoint" a formula is constructed that is satisfiable iff a given graph is connected.
The formula uses a lot of variables, as basically a breadth first search is performed and the variables code the number of steps needed to reach a vertex from the origin (which is an arbitrary, fixed vertex).
Here I want to specialise this to graphs that are actually embedded on the grid. The vertices are the points of a $m\times n$ grid, and edges are only between the east/north/west/south neighbours in the grid.
Is there a solution that is more variable-efficient, using the restricted topology?