用命题逻辑描述规划问题

11.5.1 用命题逻辑描述规划问题

我们把STRIPS问题转化成命题逻辑的过程（可谓）是知识表示圈的教科书样例：我们将从那些看似合理的公理集出发，我们会发现这些公理考虑到了谬误的非预期模型，然后我们将写出更多的公理。

让我们从十分简单的航空运输问题开始。在初始状态（时刻0），飞机P1在SFO，而飞机P2在JFK。目标是让P1在JFK并且P2在SFO，也就是，飞机互换位置。首先，我们需要对每个时间步进行断言的独特命题符号。如同第七章中一样，我们用上标表示时间步。因此，初始状态可以写成

At(P1, SFO)0∧At(P2, JFK)0

（记住 At(P1, SFO)0是一个原子符号。）因为命题逻辑没有封闭世界的假设，我们还必须指定在初始状态中不为真的命题。如果某些命题在初始状态中是未知的，那么它们可以保留不被指定（开放世界假设）。在这个例子中我们指定：

¬At(P1,JFK)0∧¬At(P2,SFO)0

目标自身必须同一个特定的时间步相关联。既然我们不知道获得目标要多少步骤的先验值，我们可以试着断言在初始状态，时刻T=0，目标为真。也就是，我们可以断言At(P1, JFK)0∧At(P2, SFO)0。如果这个失败，我们再尝试T = 1，依此类推，直到我们达到最小可行规划长度。对T的每个值，知识库只包含覆盖时间步骤从0到T的语句。为了确保终止，强加一个任意上限Tmax。这个算法如图11.15所示。一个避免多重解尝试的替换算法将在习题11.17中讨论。

接下来的问题是如何把行动描述编码到命题逻辑中。最直接的方法是给每个发生的行动一个命题符号。例如，如果在时刻0飞机P1从SFO飞往JFK，那么Fly(P1, SFO, JFK)0为真。像第七章中那样，我们写出第十章中为情景演算而发展出来的后继状态公理的命题版本。例如，我们有

图11.15 SATPLAN算法。规划问题被转换成一个CNF语句，在该语句中目标被断言在固定的时间步T是成立的，而且包含每个时间步一直到T的公理。（转换细节在正文中给出。）如果可满足性算法找到一个模型，然后通过查看那些指代行动且在模型中赋值为真的命题符号来抽取规划。如果没有模型存在，那么把目标向后移动一步，重复这个过程

也就是，如果飞机P1在时刻0位于JFK并且没有飞走，或者它在时刻0位于SFO并且飞往JFK，那么它在时刻1将在JFK。对每个飞机、机场和时间步我们都需要一条这样的公理。此外，每个附加的机场会添加旅行往返给定机场的其它途径，因此更多的析取子句将被添加到每条公理的右边。

适当运用这些规则，我们可以运行可满足性算法找到一个规划。应该有一个规划能够在时间T = 1时获得目标，即使两架飞机交换位置的规划。现在，假设知识库是

初始状态∧ 后继状态公理∧ 目标[6]　　　　　　　　　　　　　　　　　 （11.2）

这断言目标在时间T = 1为真。对于一个赋值，使得下列命题为真

Fly(P1, SFO, JFK)0和Fly(P2, JFK, SFO)0

并使所有其它行动符号为假，你可以检查该赋值是知识库的一个模型。到目前为止一切顺利。可满足性算法可能返回其它可能的模型吗？唉，不可能。考虑用下列行动符号制定的相当笨拙的规划

Fly(P1, SFO, JFK)0和Fly(P1, JFK, SFO)0和Fly(P2, JFK, SFO)0

这个规划是愚蠢的，因为飞机P1从SFO出发，所以行动Fly(P1, JFK, SFO)0是不可行的。然而，这个规划是公式（11.2）中的语句的一个模型！也就是，它与我们迄今为止所说关于问题的所有事物都一致。为了理解为什么，我们需要更仔细地看看后继状态公理（如公式（11.1））所说的前提未满足的行动。公理的确正确地预言了当这样一个行动被执行时不会发生任何事情（参见习题11.15），但是它们的确没有说行动不能被执行！为了避免用非法行动产生规划，我们必须添加前提公理来规定发生的行动要求前提得到满足1。例如，我们需要

因为At(P1, JFK)0在初始状态中被声明为假，这条公理确保每个模型也把Fly(P1, JFK, SFO)0设为假。通过添加前提公理，当在时刻1获得目标时，只有一个模型满足所有的公理，即飞机P1飞往JFK和飞机P2飞往SFO的模型。注意此解有两个并行的行动，正如用GRAPHPLAN或POP那样。

当我们增加第三个机场LAX时会有更多意外出现。现在，每架飞机在每个状态都有两个合法的行动。当我们运行可满足性算法时，我们发现拥有Fly(P1,SFO,JFK)0和Fly(P2,JFK,SFO)0和Fly(P2,JFK,LAX)0的模型满足所有公理。也就是说，后继状态和前提公理允许一架飞机同时飞往两个目的地！P2两次飞行的前提在初始状态中都得到了满足；后继状态公理表明在时刻1，P2将位于SFO和LAX；所以目标得到满足。很明显，我们需要添加更多的公理来消除这类虚假的解。一种方法是添加行动排斥公理来防止同时发生的行动。例如，我们可以通过添加形如

¬(Fly(P2,JFK,SFO)0∧ Fly(P2,JFK,LAX)0)

的所有可能公理来坚持完全排斥。这些公理确保没有两个行动能够同时发生。它们消除了所有虚假的规划，但是同时强制每个规划是完全有序的。这丧失了偏序规划的灵活性；同时，由于增加了规划中时间步的数目，计算时间也可能被延长。

我们可以用只要求部分排斥来替代完全排斥——即只有当它们互相干扰时，才排除同时发生的行动。它们的条件跟互斥行动的条件一样：如果一个行动否定了另一个行动的前提或效果，这两个行动不能同时发生。例如，Fly(P2, JFK, SFO)0和Fly(P2, JFK, LAX)0不能同时发生，因为每一个都会否定另一个的前提；另一方面，Fly(P1, SFO, JFK)0和Fly(P2, JFK, SFO)0可以同时发生，因为这两架飞机不互相干扰。部分排斥不用强制进行完全排序就排除了虚假的规划。

排斥公理有时看上去是相当生硬的方法。我们只是强调没有对象能够同时在两个地方，而不是说一架飞机不能同时飞到两个机场：

这个事实，与后继状态公理相结合，暗示一架飞机不能同时飞往两个机场。诸如此类的事实称为状态约束。当然在命题逻辑中，我们不得不写出每个状态约束的全部基例（不包含变量的——译者注）。对机场问题，状态约束足以消除所有虚假规划。通常状态约束比行动排斥公理简洁得多，但是它们并不总是能从问题的原始STRIPS描述中容易地得到。

概括而言，作为可满足性问题的规划涉及为分别包含初始状态、目标、后继状态公理、前提公理及行动排斥公理或状态约束的语句寻找模型。可以证明这个公理集是充分的，在不再有任何虚假的“解”的意义上。任何满足命题语句的模型都将是原始问题的一个有效规划——也就是，规划的每个线性化是一个能到达目标的合法行动序列。