How to encode reachability in a graph with walls as a SAT problem

Question

Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we may only move to adjacent cells (diagonal movements are not allowed).

My question is how would one encode this problem in CNF to be solved by a SAT solver?

For example, let the graph represent the following 2 x 3 grid:

0 1 0
0 0 0

where 0-cells are cells we may be in or move to and 1-cells are walls. Suppose we start in (0, 0) and want to move to (0, 2). Then there is a path.

On the contrary, consider another 2 x 3 grid with the same start and destination positions:

0 1 0
0 1 0

Then this graph does not have a path from start to destination.

Clearly we may run BFS on the graph and if there's a path we can encode it as a trivially satisfiable CNF, or if there isn't then encode it as a trivially unsatisfiable CNF. For example, $A$, or, $A \land \neg A$. However, the point of my exercise is to encode the path existence in CNF.

This is indeed part of my homework. I have been stuck for a while now. Some help on this problem would be greatly appreciated.

Answer 1

The point of my exercise is to encode the path existence in CNF

Well, a trivial way to do this is by reducing the problem to 2-SAT, following this set of rules:

1. Assing a literal to every edge of your graph, for example first element in first row become $a$, second element in first row become $b$ etc.

2. Put in OR relation the literal in the "start" position with each adjacent literal ( thus obtaining the clauses of your formula). If one or more adjacent literal has value 1, omit the clause in which it appears. Note that, when they are both 0, you dont need to repeat them: if you have an adjacency between $a$ and $b$, you do not have to repeat the clause between $b$ and $a$.Furthermore you must not consider the diagonal adjacencies.

3. Perform the same procedure for all the literals adjacent to the starting one and for those in turn, until you reach the destination literal.
4. Connects all the obtained clauses with an AND

To better adapt to your example, in which a 0 value means "you can pass" and a 1 value means "you cannot pass", you can negate all the literals in the formula.

So for the matrix in the first above example the corresponding path existence encoded into 2-SAT instance will be:

$(\not a \lor\not d) \land (\not d \lor\not e) \land (\not e \lor\not f) \land (\not f \lor\not c)$

By replacing the matrix values in the first example, the formula evaluates to 1, which means that this formula encodes a valid path. However, for the secon matrix in the example, you never obtain a true formula in which the ending literal is present, so there is no valid path.