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.