Prolog测试总是真的var(sum)错误。

Question

我正在尝试编译一个SWI-Prolog程序，但是一直收到“test is always true, var (sum) error on line 7”的错误提示。我不知道这是什么意思。请问有人可以帮忙吗？这是一个我希望最终能解决拉丁方阵问题的程序。谢谢。

:- use_module(library(clpfd)).

magic_counter(Count) :-
    findall(a, magic_1(_Soln), As),
    length(As, Count).

magic_1(Soln) :-
    Row1 = [W1, W2, W3],
    Row2 = [X1, X2, X3],
    Row3 = [Y1, Y2, Y3],

    Row1 ins 1..3,
    Row2 ins 1..3,
    Row3 ins 1..3,

    Sum #= 6,

    all_different(Row1),
    all_different(Row2),
    all_different(Row3),

    all_different([W1,X1,Y1]),
    all_different([W2,X2,Y2]),
    all_different([W3,X3,Y3]),

    W1 + W2 + W3 #= Sum,
    X1 + X2 + X3 #= Sum,
    Y1 + Y2 + Y3 #= Sum,

    W1 + X1 + Y1 #= Sum,
    W2 + X2 + Y2 #= Sum,
    W3 + X3 + Y3 #= Sum,

    append(Row1,Row2,Row12),
    append(Row12,Row3,Soln),

    labeling([], Soln).

- CompilerSaysNo

Answer 1

如果一行由介于1和3之间的三个整数组成，并且这些整数必须不同，则该行的总和必须为6（根据定义）。因此，声明这样一行的总和等于6是一个无用的限制。相同的推理适用于“列”，您需要断言类似的不相交约束条件。

编辑：尽管上述推理是正确的，但这并不是警告的起源。在这一点上，Carlo是正确的，它只取决于约束库重写约束的方式。

test1:-
  L = [X],
  L ins 1..2,
  Y #= 2,
  X #= Y.

test2:-
  L = [X],
  L ins 1..2,
  X #= 2.

test1/0会出现警告，但test2/0不会。然而，我发现很难理解为什么首先会出现这个警告，即其背后的原理是什么。例如，这是test1/0的扩展（请注意我的注释）：

:- use_module(library(clpfd)).

test1:-
  A=[D],
  A ins 1..2,
  (
    integer(B)
  ->
    (
      var(2)
    ->
      2 is B
    ;
      true
    ->
      B=:=2
    ;
      C is B,
      clpfd:clpfd_equal(C, 2)
    )
  ;
    true
  ->
    (
      var(B) % This does not throw a warning.
    ->
      B is 2
    ;
      C is 2,
      clpfd:clpfd_equal(B, C)
    )
  ;
    clpfd:clpfd_equal(B, 2)
  ),
  (
    integer(D)
  ->
    (
      var(B) % This throws a "Test is always true" warning.
    ->
      B is D
    ;
      integer(B)
    ->
      D=:=B
    ;
      E is D,
      clpfd:clpfd_equal(E, B)
    )
  ;
    integer(B)
  ->
    (
      var(D)
    ->
      D is B
    ;
      E is B,
      clpfd:clpfd_equal(D, E)
    )
  ;
    clpfd:clpfd_equal(D, B)
  ).

- Wouter Beek

---

你好，谢谢。我对Prolog非常陌生。如果我注释掉Sum #=6，我仍然会得到相同的错误。（也许我不应该注释掉它？）我想解决n阶拉丁方问题，所以我不确定我的约束条件应该是什么。再次感谢。 - CompilerSaysNo

Answer 2

这只是一个警告，而不是错误。

我之前在SWI-Prolog邮件列表上发布了一个请求，因为一些现有的代码在对消息进行细化后开始引发此警告。这里是Jan的答复。

我认为您可以忽略这个警告或禁用它，但似乎不太明智。

- CapelliC