# SAT formula for connected graphs on the grid

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?

I added a new answer, https://cs.stackexchange.com/a/142450/755, to that question. Applied to your situation, my solution uses $$O(mn \lg(m+n))$$ variables, which is asymptotically better than Yuval's algorithm (which uses $$mn(m+n)$$ variables).

• Thanks. Now I had to solve a dilemma: I decided to vote on the "real answer", at the earlier question. Jul 20 at 8:22