Picat 中的 cp/sat 似乎存在差异（最大流量）

Question

我正在尝试修改

maxflow

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]

不能同时为正。

在

flow2

中，

X[I,J]

本质上代表了

X[I,J] - X[J,I]

中

flow1

的值。

我很确定这两个模型是等效的，并且当我

import cp

时，我确实得到了相同的结果。但是，如果使用

import sat

，则对于给定的图形实例，两个结果是不同的。

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

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

这些模型实际上是否不同，或者

cp

和

sat

处理给定约束的方式是否存在细微差别？

Answer 1

这种奇怪的行为是由 Picat SAT 编译器中的错误引起的。这是一个很好的收获！虽然 2023 年的 XCSP 和 MiniZinc 比赛无法发现这个错误，但这个简短的程序揭示了它。已发布错误修复版本 3.6#4。感谢您的举报！