Clingo：在测试规则内进行计算时操作未定义

Question

我是 ASP 编程的新手，发现有点难以理解 ASP 的工作原理。我正在使用 cligo 工具进行 ASP 编码。目前，我正在研究座位安排问题。最初的问题有点复杂，因为它涉及很多变量和约束。我已经开始使用它的基本版本，如下所示：

需要 4 人排成一排，有 4 个座位。这些人之间没有限制。每个人都可以向左/向右移动到任何其他人。最终目标很简单

“只要有空位，任何人都可以坐在任何位置”

唯一的条件是保存有关如何达到目标的各个步骤。

为了解决这个问题，我使用了谓词

seated(A,B,Shift,Dir,t) 表示在“t”时间，A 已将“Dir”中的“Shift”单位从 B 转移

例子

seated(A,B,left,2,t) 表示 A 在时间 t 向 B 左侧移动了 2 个单位

我用了两个文件

init.lp 描述初始位置和最终目标

person(a).

person(b).

person(c).

person(d).

init(pos(a,0)).

init(pos(b,0)).

init(pos(c,0)).

init(pos(d,0)).


goal(pos(a,1)).

goal(pos(b,2)).

goal(pos(c,3)).

goal(pos(d,4)).

写规则的rules.lp

#include<incmode>.

#program base.
% Define
holds(F,0) :- init(F).
%{possible_location(X,Y,1) : person(X),Y = 1..4}.
%%possible_location(X,Y,1) : person(X),Y = 1..4.



#program step(t).
% Generate any seating arrangement

1{seated(X,Z,Shift,Dir,t) : person(X),person(Z),X != Z,Shift = 1..3, Dir = (left;right)}1.


% Test
% Remove the seated predicates which the shift is not possible
:- seated(X,Z,Shift,right,t),holds(pos(Z,Pos),t-1), Shift + Pos > 4.
:- seated(X,Z,Shift,left,t),holds(pos(Z,Pos),t-1), Pos - Shift < 1.

% Remove the seated predicates if the final position after shifting is already occupied
:- seated(X,Z,Shift,right,t),holds(pos(Z,Pos),t-1), Pos >0,holds(pos(A,Shift + Pos),t-1), A !=X.
:- seated(X,Z,Shift,left,t),holds(pos(Z,Pos1),t-1),  Pos1 >0, holds(pos(A,Pos1 - Shift),t-1), A !=X.



% Define
seateded(X,t) :- seated(X,Z,Shift,Dir,t).

% Relating the current move to the current state %
holds(pos(X,Y),t) :- seated(X,Y,Shift,Dir,t).

% This is for shifting the state to the next time %
holds(pos(X,Z),t) :- holds(pos(X,Z),t-1), not seateded(X,t).

#program check(t).
% Test
:- query(t), goal(F), not holds(F,t).

% Display
#show seated/5.
#show query/1.

在运行上述文件时，它给出了一个错误

rule_new.lp:21:75-87：信息：操作未定义： (Pos1-Shift)

我用谷歌搜索了它，发现当我没有处理任何边缘情况（如 X/Y 和 Y =0 未处理）时会出现此错误。在这种情况下，我看不到任何边缘情况。因此，我无法纠正错误。

我已经记录了规则，以便我可以解释编写规则背后的思考过程。我花了几个小时解决它，但仍然无法找出解决方案。如果我的想法没有朝着正确的方向前进，那么如果我能找到解决上述问题的其他方法，我将不胜感激。

Answer 1

恐怕我没能理解您的解决方案（或问题），但使用选项--text 可以帮助您找出这个错误。 根据错误信息，问题出在这条规则上：

seated(X,Z,Shift,left,t),holds(pos(Z,Pos1),t-1),  Pos1 >0, holds(pos(A,Pos1 - Shift),t-1), A !=X.

您尝试从Pos1 中减去Shift。两个变量都应该用整数替换才能完成这项工作。

Shift 来自座位谓词，可以在1..3 之间取值，很好。 Pos1 来自 holds(pos(_,Pos1),_) 谓词。

在你的规则中：

holds(pos(X,Y),t) :- seated(X,Y,Shift,Dir,t).

您清楚地得出holds 谓词，其中Y 是一个人，又名。 a、b、c 或 d。

因此，您尝试计算 cligo 拒绝执行的 3-a 并放弃相应的规则，从而引发此警告。