Scryer-Prolog中CLPZ模块的不完备性问题分析

问题背景

在Scryer-Prolog的CLPZ（约束逻辑编程整数模块）中，用户发现了一个关于约束传播和标记(labeling)的不完备性问题。这个问题涉及到复杂的算术约束表达式在特定执行顺序下会产生不一致的结果。

问题现象

核心问题表现为约束求解在不同查询顺序下产生矛盾的结果。例如以下两个看似等价的查询：

?- C=1,C in 0..1,#\A*max(-1,A^C)#>0,labeling([],[C]),A in -1..1,labeling([],[A]).
% 返回 C = 1, A = 0

?- C in 0..1,#\A*max(-1,A^C)#>0,labeling([],[C]),A in -1..1,labeling([],[A]),C=1.
% 返回 false

这两个查询在逻辑上应该是等价的，只是约束条件的顺序不同，但却产生了完全不同的结果，这表明CLPZ模块在处理复杂约束时存在不一致性。

技术分析

约束传播机制的问题

深入分析发现，这个问题与CLPZ模块中pexp传播器的实现有关。具体来说，传播器在计算边界值时使用了旧的边界值，而没有获取最新的边界值更新。这导致约束传播不完整，在某些情况下会错误地排除有效解。

更简单的重现案例

开发者进一步简化了重现问题的案例：

?- A=1,A in 1..2,A#=sign(A)/B/A.
% 返回 A = 1, B = 1

?- A in 1..2,A#=sign(A)/B/A.
% 返回 false

这个简化案例同样展示了约束传播的不一致性：当变量A先被实例化时，系统能找到解；但当A仅受区间约束时，系统错误地认为无解。

相关算术运算问题

在调查过程中，还发现了其他相关的基础算术运算问题：

?- Z #= max(X, Y).
% 意外返回 false

?- A #>= B.
% 意外返回 false

这些问题表明CLPZ模块在基础算术约束处理上也存在缺陷，特别是在处理最大值函数和比较运算时。

问题根源

经过代码审查，发现问题主要出在fd_get/5谓词的实现上。该谓词在获取变量边界时没有正确获取最新的边界值，导致后续的约束传播基于不完整或不正确的信息进行推理。

具体来说，在计算如max(-1,A^C)这样的表达式时，系统没有正确跟踪变量A和C的当前约束状态，导致在某些情况下过早地排除了可能的解。

解决方案

项目贡献者notoria提出了修复方案：在相关代码位置使用NZL和NZU来替代原有的边界获取方式，确保总是使用最新的边界值进行计算。

这个修复不仅解决了原始报告的问题，也一并解决了相关的简化案例和基础算术运算问题。

经验教训

1. 约束传播的完整性：约束逻辑编程系统必须确保约束传播的完整性，特别是在处理复合表达式时，需要正确跟踪所有相关变量的最新约束状态。

2. 测试覆盖的重要性：这个问题暴露出测试用例覆盖不足的问题，特别是对于复杂约束表达式在不同求解顺序下的行为测试。

3. 基础运算的稳定性：即使是基础的算术比较和函数运算，也需要有严格的测试保证，因为它们构成了更复杂约束的基础。

结论

Scryer-Prolog的CLPZ模块在处理特定类型的复合约束时存在传播不完整的问题。通过修正边界值的获取机制，可以恢复约束传播的正确性和完整性。这一案例也提醒我们，在实现约束逻辑编程系统时，需要特别注意约束传播的顺序依赖性和边界条件的正确处理。

未来，增加全面的测试用例，特别是针对约束表达式在不同求解顺序下的行为测试，将有助于预防类似问题的发生。