如何消除条件 Clingo 规则中的不安全性？答案

【问题标题】：How to remove unsafety in a conditional Clingo rule?如何消除条件 Clingo 规则中的不安全性？
【发布时间】：2021-12-23 07:03:25
【问题描述】：

我想在有向图中定义一组节点，该有向图中可从 Clingo 中给定起始节点集中的所有节点访问。据我了解，这可以通过规则主体中的条件来完成：在规则中

p(X) :- q(X) : r(X).

规则q(a) 的组合在p/1 的主体中动态生成，用于基础事实a，规则r(a) 也适用。现在由于某种原因，以下规则集导致在最后一行发现“不安全”变量X：

% Test case

arc(1,4). arc(2,4). arc(3,5). arc(4,1). arc(4,2). arc(4,3).
start(1). start(4). start(5).

% Define a path inductively, with the base case being path of length 1:

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

% A node X is simply reachable/1, if there is a possibly empty path to it
% from a start node or reachable/2 from A, if there is a path to it from A:

reachable(X) :- start(X).
reachable(X) :- start(A), path(A, X).
reachable(X, A) :- path(A, X).

% Predicate all_reach defined by the reachable relation:

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

我想问一下，“不安全”变量是什么意思，我该如何修改这种情况？一个消息来源声称不安全变量是一个变量，它出现在规则的头部而不是规则主体，这是有道理的，因为符号:- 表示相反的含义。但是，这里似乎不是这样，所以我很困惑。

是否可能没有一个有根据的事实a 支持start(a)，因此暗示或规则的主体变为空，导致不安全。是这样吗？有避免这种情况的标准方法吗？

【问题讨论】：

标签： conditional-statements clingo

【解决方案1】：

问题在于all_reach/1 的正文中没有一个肯定的规则至少满足X 的一些接地实例。添加行

% Project nodes from arcs

node(X) :- arc(X,Y).
node(Y) :- arc(X,Y).

并将all_reach/1 规则重新表述为

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

解决了这个问题。想要的连词

∧[i=1 → ∞] reachable(d, s[i])

对于所有起始节点 s[i] 和目标节点 d 然后生成为 allreach/1 的正文。

换句话说，当在规则 r/n 的主体 b/m 中使用条件时，在b 中仍然必须有一个谓词p 是无条件 接地的对于规则头部中存在的任何变量。否则我们可能会结束在接地期间具有模糊性或不断扩展的规则，这是不安全的。

【讨论】：