Clingo递归提前终止问题：为何未生成p(2,c,d)相关组合？

问题场景 #

使用单一谓词递归时，无法生成p(2,c,d) p(1,b,c) p(0,a,b)这一预期组合，但拆分谓词为多个层级后可以正常生成对应解。

单一谓词递归代码 #

move( a, b).
move( b, c).
move( c, d).

{ p( 0, A, B) : move( A, B) } = 1 .

0 { p( N+1, B, C) : p( N, A, B), move( B, C) } 1.

对应求解结果 #

Solving...
Answer: 1
p(0,c,d)
Answer: 2
p(0,a,b)
Answer: 3
p(1,b,c) p(0,a,b)
Answer: 4
p(0,b,c)
Answer: 5
p(1,c,d) p(0,b,c)
SATISFIABLE

拆分谓词后的代码 #

move( a, b).
move( b, c).
move( c, d).

{ p( 0, A, B) : move( A, B) } = 1 .

0 { p2( N+1, B, C) : p( N, A, B), move( B, C) } 1.

0 { p3( N+1, B, C) : p2( N, A, B), move( B, C) } 1.

该代码的求解结果包含p3(2,c,d) p2(1,b,c) p(0,a,b)这一预期组合。

原因解析 #

核心在于Clingo的接地（grounding）机制对两种写法的处理差异：

• 单一谓词递归时，规则0 { p(N+1,...) } 1是可选约束（允许选择0个实例）。接地器初始仅能确定N=0的p实例，处理N=0后生成p(1,_,_)的可能实例，但没有强制要求必须基于p(1,_,_)继续生成p(2,_,_)的约束，因此接地器不会主动扩展N到2的层级。
• 拆分谓词后，p2依赖p、p3依赖p2，形成明确的单向依赖链。接地器会依次处理每个规则：先基于p(0,_,_)生成p2(1,_,_)，再基于p2(1,_,_)生成p3(2,_,_)，自然覆盖到更深的层级。

单一谓词的修复方案 #

如果想用单一谓词实现预期效果，只需将可选约束改为强制约束，确保每个层级必须生成一个实例：

move( a, b).
move( b, c).
move( c, d).

{ p( 0, A, B) : move( A, B) } = 1 .

1 { p( N+1, B, C) : p( N, A, B), move( B, C) } 1.

修改后，规则强制每个存在的p(N,_,_)必须生成对应的p(N+1,_,_)实例，接地器会自动扩展N直到无法生成新实例，最终就能得到包含p(2,c,d) p(1,b,c) p(0,a,b)的解。

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