Finding a path through vertices in a graph with SAT Solving in Python

Question

Essentially what I am trying to do is find a path from v1 to v2 on a graph but some nodes are coloured and we can't visit them.

I understand the constraints but the part I am really having a problem with is understanding how to add the possible moves to the constraints.

If I set up the booleans in this way

nodes = [Int('"n%i_%i" % (i, j)) for i in range(len(G))]

moves = []
for i in range(len(G)):
     moves += ?

The condition would be that the nodes are beside each other so i = i and j = j +1 (or i = i +1 and j = j) and that the node is allowed to be visited so path=True, which is a feature of the graph. So for example G[i][j] == True.

Would I use something like (or(And(nodes are beside each other), (G[i][j] == True))) And how can I express the nodes are beside each other?

Thank you!!

Answer 1

As I do not understand what you mean with colored nodes, here would be a preliminary solution:

Predicates

First, we define some predicates and what they intuitively mean for us:

p(X, Y, n) denotes that we visit the node at the coordinates X, Y at time point n, where time point starts at 0 and goes up to length of G.

go(right, n) denotes that we go to right at time point n.

go(down, n) denotes that we go down at time point n.

Encoding

Initial State

Initially, we know that p(Start_X, Start_Y, 0) is true. Consequently, we add the unit clause [p(Start_X, Start_Y, 0)]

Movement

At each time point, we have to move. Therefore, for every time point t, add the clauses [go(right, t), go(down, t)] and [not go(right, t), not go(down, t)] This is also known as the exactly once constraint, i.e. we can either move right or down.

Now, we need to relate the p predicate and the go predicate: If p(X, Y, T) is true, and go(right, T), then p(X+1, Y, T+1) is true. Consequently, add the clauses [not p(X, Y, T), not go(right, T), p(X+1, Y, T+1)].

In a similar way you can encode the "go down" action.

Final State

Now, we have to ensure that we finally reach the node v2. Please note that it is not enough to add that p(v2_x, v2_y, t) is true for some time point. Instead, we have to ensure that models violating this condition are excluded: As we can only move down or right, we know that we cannot visit nodes that are below of v2 or right to it. Consequently, we add unit clauses of the form [not p(X, Y, t)], where t is the distance from v1 and v2.

Auxiliary

Now, a solution can be read off from your model, but your model may looks a bit strange in the sense that multiple p-predicates are true at the same time point. In general, this does not hurt, but can be excluded if you say so: [not p(X1, Y1, t), not p(X2, Y2, t)] for every t and distinct coordinates.