SWI-Prolog中codeword谓词带约束查询返回错误结果问题咨询

这不是Prolog的bug，是你的代码实现存在关键问题，导致反向查询时无法得到正确结果：

1. addbinvecs的if-then-else结构阻止回溯 #

原addbinvecs使用(A = B -> C = 0; C = 1)的if-then-else逻辑，当处理未绑定变量时，Prolog会优先尝试统一A = B（比如X=1）并执行then分支，不会回溯到else分支尝试A \= B的情况。这导致反向查询时无法生成所有可能的异或结果，自然找不到[0,1,1]这个解。

2. allzero实现的通用性不足（非核心问题） #

原allzero仅能处理长度≥1的零向量，修改后可支持任意长度的零向量（包括空向量）。

修正后的代码 #

% 模2向量加法（异或）：用子句实现，支持回溯生成所有可能结果
addbinvecs([], [], []).
addbinvecs([A|As], [B|Bs], [0|Cs]) :- A = B, addbinvecs(As, Bs, Cs).
addbinvecs([A|As], [B|Bs], [1|Cs]) :- A \= B, addbinvecs(As, Bs, Cs).

% 判断是否为全零向量，支持任意长度
allzero([]).
allzero([0|Rest]) :- allzero(Rest).

% 判断是否为生成矩阵的码字
codeword(X, _) :- allzero(X).
codeword(C, [C|_]).
codeword(C, [_|Gt]) :- codeword(C, Gt).
codeword(C, [Gh|Gt]) :- addbinvecs(C, Gh, C1), codeword(C1, Gt).

测试验证 #

运行查询：

codeword([X,Y,Z], [[1,1,1],[1,0,0]]), X+Y+Z =:= 2.

会返回正确结果：

X = 0, Y = 1, Z = 1.

补充说明 #

生成矩阵的码字本质是行向量的模2线性组合，修正后的addbinvecs通过子句实现异或逻辑，允许Prolog回溯尝试所有可能的组合，从而在反向查询时能正确生成所有符合条件的码字。

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