I’m trying to modify `maxflow` modeling from A User’s Guide to Picat. I have two versions, `flow1` and `flow2`, as follows:

``````import cp,util.
main =>
V = [1, 2, 3, 4, 5, 6, 7, 8],
E = [{1, 2}, {1, 3}, {3, 4}, {2, 4}, {3, 5}, {5, 6}, {6, 7}, {7, 8}, {8, 5}],
M = to_mat(V, E),
foreach(Row in M) println(Row) end,
flow1(M, 4, 7, S1),
flow2(M, 4, 7, S2),
printf("S1: %d / S2: %d", S1, S2).

to_mat(V, E) = M =>
N = len(V),
M = new_array(N, N),
foreach(I in 1..N, J in 1..N)
if membchk({I,J}, E) || membchk({J,I}, E) then M[I,J] = 1 else M[I,J] = 0 end
end.

flow1(M, A, B, S) =>
N = M.len,
X = new_array(N, N),
Y = X.transpose,
foreach(I in 1..N, J in 1..N)
X[I,J] :: 0..M[I,J]
end,
foreach(I in 1..N, J in 1..N)
X[I,J] + X[J,I] #< 2
end,
foreach(I in 1..N, I!=A, I!=B)
sum(Y[I]) #= sum(X[I])
end,
S #= sum(X[A]) - sum(Y[A]),
solve([\$max(S)], X).

flow2(M, A, B, S) =>
N = M.len,
X = new_array(N, N),
foreach(I in 1..N, J in 1..N)
X[I,J] :: -M[I,J]..M[I,J]
end,
foreach(I in 1..N, J in 1..N)
X[I,J] #= -X[J,I]
end,
foreach(I in 1..N, I!=A, I!=B)
sum(X[I]) #= 0
end,
S #= sum(X[A]),
solve([\$max(S)], X).
``````

In `flow1`, Since the given graph is undirected and of unit capacity, I added a condition that both `X[I,J]` and `X[J,I]` cannot be positive at once.

In `flow2`, `X[I,J]` essentially represents the value of `X[I,J] - X[J,I]` in `flow1`.

I’m pretty sure the two models are equivalent, and indeed I get the same result when I `import cp`. However, with `import sat` instead, the two results are different for the graph instance given.

``````% with `import cp`
S1: 1 / S2: 1

% with `import sat`
S1: 1 / S2: 0
``````

Are the models actually different, or is there any subtle difference in how `cp` and `sat` handle the given constraints?