Picat中cp与sat求解最大流时的结果差异问题排查

我基于《A User’s Guide to Picat》修改了最大流建模，实现了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] #< 2，确保X[I,J]和X[J,I]不能同时为正
• flow2：X[I,J]本质代表flow1中X[I,J] - X[J,I]的差值，通过X[I,J] #= -X[J,I]约束保证对称性

求解结果对比 #

• 使用import cp约束求解器时，两个模型结果一致：

  S1: 1 / S2: 1
  

• 使用import sat可满足性求解器时，结果出现差异：

  S1: 1 / S2: 0
  

请问这两个模型实际是否存在逻辑差异，还是CP与SAT求解器处理约束的方式存在细微区别？

内容的提问来源于stack exchange，提问作者Bubbler