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?


1 Answer 1


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).

  • $\begingroup$ Thanks. Now I had to solve a dilemma: I decided to vote on the "real answer", at the earlier question. $\endgroup$ Commented Jul 20, 2021 at 8:22
  • $\begingroup$ But, as I could not award the same bounty for two different answers, a bounty goes here. $\endgroup$ Commented Dec 3, 2021 at 0:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.