如何解决Clingo条件规则中的unsafe变量不安全问题

1. unsafe变量的定义 #

你查到的基础定义是成立的，不过ASP（回答集编程）的ground阶段对「变量出现在规则体」有更严格的约束：

所有出现在规则头的变量，必须被规则体中的正的、非条件、非聚合的普通外延/内涵原子绑定可枚举的取值范围，否则就会被判定为unsafe变量。

你当前的场景正好踩了这个约束的边界：你规则头的变量X只出现在了条件式reachable(X, A) : start(A)里，而条件式属于全称量化的特殊规则元素，Clingo的grounder不会从条件式中提取头变量的取值范围，因此无法确定X的合法取值集合，就会报unsafe错误，和start集合是否为空没有关系。

2. 修复方案 #

规避这类问题的标准方案就是：给规则头的变量加一个非条件的取值范围约束。
首先你需要先定义图中所有节点的集合：

% 定义所有节点
node(X) :- arc(X, _).
node(X) :- arc(_, X).
node(X) :- start(X).

然后修改你最后一行的all_reach规则，加上node(X)的约束：

all_reach(X) :- node(X), reachable(X, A) : start(A).

修改后X的取值范围被node(X)明确限定为图中存在的节点，grounder可以正常枚举所有可能的X取值，就不会再报unsafe错误。

3. 额外优化建议 #

你当前的path定义只能覆盖长度为1、2、3的路径，无法处理更长的路径，建议替换为标准的传递闭包写法，支持任意长度的有向路径推导：

path(A, B) :- arc(A, B).
path(A, B) :- arc(A, X), path(X, B).

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