Кажущееся несоответствие cp/sat в Пикате (максимальный поток)

Я пытаюсь изменить maxflow моделирование из «Руководства пользователя по Пикату». У меня есть две версии, flow1 и flow2, а именно:

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).

В flow1, поскольку данный граф неориентированный и имеет единичную емкость, я добавил условие, что оба X[I,J] и X[J,I] не могут быть положительными одновременно.

В flow2X[I,J] по существу представляет значение X[I,J] - X[J,I] в flow1.

Я почти уверен, что эти две модели эквивалентны, и действительно, я получаю одинаковый результат, когда import cp. Однако вместо этого два результата будут разными для данного экземпляра графа.

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

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

Действительно ли модели разные, или есть какая-то тонкая разница в том, как import sat и cp справляются с заданными ограничениями?