You can try representing graphical adjacencies in a propositional formula, and then squeeze out redundancies by using some species of canonical form.

I don't recall trying this for arbitrary graphs, but I do recall solving graph coloring problems this way. Here's one link I was able to find right away, an example from Wilf's Algorithms and Complexity (1986).

Graph Coloring Example

What you need to know is that a parenthetical form like $(x_1, \ldots, x_k)$ means that exactly one of the boolean variables $x_1, \ldots, x_k$ is false.

You can try representing graphical adjacencies in a propositional formula, and then squeeze out redundancies by using some species of canonical form.

I don't recall trying this for arbitrary graphs, but I do recall solving graph coloring problems this way. Here's one link I was able to find right away, an example from Wilf's Algorithms and Complexity (1986).

Graph Coloring Example

What you need to know is that a parenthetical form like $(x_1, \ldots, x_k)$ means that exactly one of the boolean variables $x_1, \ldots, x_k$ is false.

Here's a propositional constraint representation of the 5 queens problem, which may be more suggestive of a way to proceed with your square grid domain.

Five Queens Problem

And here's an exposition of the language and program that I was using to do these examples:

Zeroth Order Logic