Grid with programming constraints
I have a mesh network as shown in the picture. Now I am highlighting values to all edges in this mesh. I want to suggest in my program that there are no closed loops in my distribution. For example, the constraint on the top-left most square can be written as -
E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0
, so any of the links must be inactive so as not to form a loop. However, there are many possible loops in such a network.
For example, a loop formed by ribs - E0, E3, E7, E11, E15, E12, E5, E1
.
Now my problem is that I have to describe every possible combination of a loop that can happen on this network. I tried to write the constraints in one possible formula, however I was unable to succeed.
Can anyone throw in any pointers if there is a possible way to code this situation? For information only, I am using the Z3 Sat Solver.
source to share
The following encoding can be used with any graph with N
nodes and M
edges. It uses variables (N+1)*M
and 2*M*M
3-SAT. This ipython notebook demonstrates the encoding by comparing the results of the SAT solution (UNSAT when there is a loop, SAT otherwise) with the results of the forward loop finding algorithm.
Disclaimer: This encoding is my special solution to the problem. I'm sure this is correct, but I don't know how it compares performance to other encodings for this problem. Since my solution works with any graph, it should be expected that there is a better solution that takes advantage of some of the properties of the graph class of interest to the OP.
Variables
I have one variable for each edge. An edge is "active" or "used" if the corresponding variable is set. In my referenced implementation, the edges are indexed 0..(M-1)
, and these variables are indexed 1..M
:
def edge_state_var(edge_idx):
assert 0 <= edge_idx < M
return 1 + edge_idx
Then I have a variable state variable M
for each edge or all of the state bits N*M
(nodes and bits also use zero-based indexing):
def node_state_var(node_idx, bit_idx):
assert 0 <= node_idx < N
assert 0 <= bit_idx < M
return 1 + M + node_idx*M + bit_idx
Articles:
When an edge is active, it binds the state variables of the two nodes it connects to. The status bits with the same index as the node must be different on either side, and the rest of the status bits must be equal to their corresponding partner on the other node. In python code:
# which edge connects which nodes
connectivity = [
( 0, 1), # edge E0
( 1, 2), # edge E1
( 2, 3), # edge E2
( 0, 4), # edge E3
...
]
cnf = list()
for i in range(M):
eb = edge_state_var(i)
p, q = connectivity[i]
for k in range(M):
pb = node_state_var(p, k)
qb = node_state_var(q, k)
if k == i:
# eb -> (pb != qb)
cnf.append([-eb, -pb, -qb])
cnf.append([-eb, +pb, +qb])
else:
# eb -> (pb == qb)
cnf.append([-eb, -pb, +qb])
cnf.append([-eb, +pb, -qb])
So basically every edge is trying to segment the graph, it is a piece of half that is on one side of the edge and has all the status bits corresponding to the edge set to 1 and a half that is on the other side of the edge and has a status bit that matches edge set to 0. This is not possible for a loop where all the nodes in the loop can be reached on both sides of each edge in the loop.
source to share