Knowledge Representation, Reasoning and Declarative Problem Solving 中给出了一个使用 Answer Set Prolog 编码规划的方法，以下代码是书中给出的一个编码积木世界规划问题。

% domain
block(a;b;c;d).
fluent(on(X,Y)) :- block(X), block(Y).
fluent(ontable(X)) :- block(X).
fluent(clear(X)) :- block(X).
fluent(holding(X)) :- block(X).
fluent(handempty).
action(pick_up(X)) :- block(X).
action(put_down(X)) :- block(X).
action(stack(X,Y)) :- block(X), block(Y).
action(unstack(X,Y)) :- block(X), block(Y).
% executability conditions
exec(pick_up(X), clear(X)) :- block(X).
exec(pick_up(X), ontable(X)) :- block(X).
exec(pick_up(X), handempty) :- block(X).
exec(put_down(X), holding(X)) :- block(X).
exec(stack(X,Y), holding(X)) :- block(X), block(Y).
exec(stack(X,Y), clear(Y)) :- block(X), block(Y).
exec(unstack(X,Y), clear(X)) :- block(X), block(Y).
exec(unstack(X,Y), on(X, Y)) :- block(X), block(Y).
exec(unstack(X,Y), handempty) :- block(X), block(Y).
% dynamic causal laws
causes(pick_up(X), neg(ontable(X))) :- block(X).
causes(pick_up(X), neg(clear(X))) :- block(X).
causes(pick_up(X), holding(X)) :- block(X).
causes(pick_up(X), neg(handempty)) :- block(X).
causes(put_down(X), ontable(X)) :- block(X).
causes(put_down(X), clear(X)) :- block(X).
causes(put_down(X), neg(holding(X))) :- block(X).
causes(put_down(X), handempty) :- block(X).
causes(stack(X, Y), neg(holding(X))) :- block(X), block(Y).
causes(stack(X, Y), neg(clear(Y))) :- block(X), block(Y).
causes(stack(X, Y), clear(X)) :- block(X), block(Y).
causes(stack(X, Y), handempty) :- block(X), block(Y).
causes(stack(X, Y), on(X, Y)) :- block(X), block(Y).
causes(unstack(X, Y), holding(X)) :- block(X), block(Y).
causes(unstack(X, Y), clear(Y)) :- block(X), block(Y).
causes(unstack(X, Y), neg(clear(X))) :- block(X), block(Y).
causes(unstack(X, Y), neg(handempty)) :- block(X), block(Y).
causes(unstack(X, Y), neg(on(X, Y))) :- block(X), block(Y).
% initial state
initially(handempty).
initially(clear(a)).
initially(clear(c)).
initially(ontable(c)).
initially(ontable(b)).
initially(on(a, b)).
initially(yes).
% goal conditions
finally(on(a, c)).
finally(on(c, b)).
% time
time(1..7).
% goal
not_goal(T) :- time(T), finally(X), not holds(X, T).
goal(T) :- time(T), not not_goal(T).
% eliminating plan without given length
:- not goal(7).
% contrary
contrary(F, neg(F)) :- fluent(F).
contrary(neg(F), F) :- fluent(F).
% executability
not_executable(A, T) :- exec(A, F), not holds(F, T), time(T).
executable(A, T) :- T < 7, not not_executable(A, T), action(A), time(T).
% initial fluent values
holds(F, 1) :- initially(F).
% effect axiom
holds(F, T + 1) :- T < 7, executable(A, T), occurs(A, T), causes(A, F).
% inertia
holds(F, T + 1) :- contrary(F, G), T < 7, holds(F, T), not holds(G, T + 1).
% occurrence of actions
occurs(A, T) :- action(A), time(T), not goal(T), not not_occurs(A, T).
not_occurs(A, T) :- action(A), action(AA), time(T), occurs(AA, T), A != AA.
:- action(A), time(T), occurs(A, T), not executable(A, T).

规划的解则是输出的 Answer Set 的一个子集，比如上面这个规划的解是这个：

occurs(unstack(a,b),1) 
occurs(put_down(a),2) 
occurs(pick_up(c),3) 
occurs(stack(c,b),4) 
occurs(pick_up(a),5) 
occurs(stack(a,c),6)

不过，如果只是想要知道规划的话，整个 Answer Set 就太大了。有没有办法去掉一些无用的谓词呢？

去掉可执行性条件

和可执行性相关的谓词是 exec、executable 和 not_executable，而后两者是由前者和 fluent 的成立性 holds 推来的，又用于推出动作的出现 occurs，所以可执行性可以看成同一时刻的 occurs 和 holds 的关系。那这个关系是什么？

如果某个动作 $A$ 需要 fluent $F$ 成立才能执行，那么若 $F$ 在时刻 $T$ 不成立，则 $A$ 在时刻 $T+1$ 不能出现 — 若出现，则有矛盾。

$$\bot\leftarrow occurs(A, T+1),\ \mathbf{not}\ holds(F,T).$$

针对原问题中四个动作的相应编码如下。

% executability conditions
:- occurs(pick_up(X), T), not holds(clear(X), T).
:- occurs(pick_up(X), T), not holds(ontable(X), T).
:- occurs(pick_up(X), T), not holds(handempty, T).
:- occurs(put_down(X), T), not holds(holding(X), T).
:- occurs(stack(X, Y), T), not holds(holding(X), T).
:- occurs(stack(X, Y), T), not holds(clear(Y), T).
:- occurs(unstack(X, Y), T), not holds(clear(X), T).
:- occurs(unstack(X, Y), T), not holds(on(X, Y), T).
:- occurs(unstack(X, Y), T), not holds(handempty, T).

很好！只要找到方法推出 occurs 和 holds 就可以了。

去掉动态因果律

和动态因果律有关的谓词是 causes，它是用在效果公理里的，删除了它的话效果公理也可以删除了。效果公理是从一个动作的出现 occurs 得到下一时刻成立的 fluents holds，所以动态因果律可以看成下一时刻的 holds 由 occurs 推出的关系。

这个关系比上面的就简单多了。如果执行某个动作 $A$ 会使得某个 fluent $F$ 成立，那么若 $A$ 在时刻 $T$ 出现，则 $F$ 在时刻 $T+1$ 成立。

holds(neg(ontable(X)), T + 1) :- occurs(pick_up(X), T).
holds(neg(clear(X)), T + 1) :- occurs(pick_up(X), T).
holds(holding(X), T + 1) :- occurs(pick_up(X), T).
holds(neg(handempty), T + 1) :- occurs(pick_up(X), T).
holds(ontable(X), T + 1) :- occurs(put_down(X), T).
holds(clear(X), T + 1) :- occurs(put_down(X), T).
holds(neg(holding(X)), T + 1) :- occurs(put_down(X), T).
holds(handempty, T + 1) :- occurs(put_down(X), T).
holds(neg(holding(X)), T + 1) :- occurs(stack(X, Y), T).
holds(neg(clear(Y)), T + 1) :- occurs(stack(X, Y), T).
holds(clear(X), T + 1) :- occurs(stack(X, Y), T).
holds(handempty, T + 1) :- occurs(stack(X, Y), T).
holds(on(X, Y), T + 1) :- occurs(stack(X, Y), T).
holds(holding(X), T + 1) :- occurs(unstack(X, Y), T).
holds(clear(Y), T + 1) :- occurs(unstack(X, Y), T).
holds(neg(clear(X)), T + 1) :- occurs(unstack(X, Y), T).
holds(neg(handempty), T + 1) :- occurs(unstack(X, Y), T).
holds(neg(on(X, Y)), T + 1) :- occurs(unstack(X, Y), T).

只要能推出 occurs，一切都会好起来的。

会吗？

很遗憾，我没有找到使用纯非单调推理但不使用无用谓词 not_occurs 来满足推出谓词 occurs 的要求：每个时刻 $T$ 有且仅有一个动作 $A$ 满足 occurs．也就是说，它的规则类似：

$$occurs(A,T)\leftarrow action(A),\ time(T),\ \forall AA\{action(AA),\ AA\neq A,\ \mathbf{not}\ occurs(AA)\}.$$

然而 ASP 中对变量均是存在量化的。在这里，not_occurs 对于实现 occurs 的唯一性是必要的：在对某个动作推出 occurs 后，对其它动作只会推出 not_occurs，也就推不出 occurs 了。

可能正是为了编码唯一性，clingo 给出了集合计数的方法。

1 { occurs(A, T) : action(A) } 1 :- time(T), not goal(T).

左右两边的 1 表示即使考虑所有 A，occurs 也只会出现一次。

既然都用 clingo 了，为什么不用 incmode？

是啊！为什么呢？

最主要的是，为什么不用 show 来实现只输出 occurs 呢？？

确实。

附录

我改过的代码在这里。我又去掉了 contrary，不过这样编码形式就和作者给出的代码有一些差别。