Kiểm tra Prolog luôn đúng sai số var (tổng)

Question

Tôi đang cố gắng biên dịch chương trình SWI-Prolog nhưng vẫn giữ được test is always true, var (sum) error on line 7. Tôi không thể hiểu được điều này có nghĩa là gì. Ai đó có thể giúp đỡ? Đây là một chương trình tôi hy vọng cuối cùng sẽ giải quyết các ô vuông Latin. Cảm ơn bạn.

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

Answer 1

Đó là cảnh báo chứ không phải là lỗi.

Tôi đã đăng một lần nữa một yêu cầu về danh sách gửi thư SWI-Prolog cho vấn đề này, vì một số mã hiện tại bắt đầu tăng cảnh báo này sau khi sàng lọc thư. Here là câu trả lời từ Jan

Tôi nghĩ bạn có thể bỏ qua cảnh báo hoặc vô hiệu hóa cảnh báo, nhưng điều này có vẻ không được khuyến khích.

Answer 2

Nếu một hàng bao gồm ba số nguyên giữa 1 và 3, và những số nguyên phải phân biệt, sau đó tổng của một hàng như vậy phải 6 (theo định nghĩa). Nói rằng tổng của một hàng như vậy bằng 6 do đó là một ràng buộc nhàn rỗi. Cùng một lý do áp dụng cho các 'cột' mà bạn khẳng định những ràng buộc rời rạc tương tự.

Chỉnh sửa: Mặc dù các lý do trên là đúng, đây không phải là nguồn gốc của cảnh báo. Carlo là đúng về điều này, nó chỉ đơn giản phụ thuộc vào cách thức mà thư viện ràng buộc viết lại các ràng buộc.

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

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

test1/0 đưa ra cảnh báo, test2/0 không. Tuy nhiên, tôi thấy khó có thể hiểu tại sao cảnh báo lại được đưa ra ngay từ đầu, nghĩa là lý do đằng sau nó là hợp lý. Ví dụ: dưới đây là việc mở rộng test1/0 (thông báo ý kiến ​​của tôi):

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