A seeming cp/sat discrepancy in Picat (maximum flow)

Question

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?

Answer 1

This strange behavior is caused by a bug in the Picat SAT compiler. This is a nice catch! While the XCSP and MiniZinc competitions in 2023 couldn't catch this bug, this short program reveals it. A bug-fixed version, 3.6#4, has been released. Thank you for reporting!