初识ASP（Answer Set Programming）

第一印象

ASP（回答集编程）是基于逻辑程序和它们的回答集的声明式编程范式，它提供了一种简单且强大的建模语言来解决组合问题，而Potsdam Answer Set Solving Collection（Potassco）则把包括gringo、clasp的多种用于ASP的工具组合起来，成为一个集成的ASP系统clingo。

用途

主要用于快速解决计算困难的问题，如full-fledged SAT, MaxSAT, PB。集成于一个系统则可以让使用者更加关注实际的问题本身，而不是实现的方法。

初识语法

用一个例子直观地认识ASP的语法。汉诺塔问题由3根柱子和4个盘子组成，初始状态和目标状态如图1所示。每次能且只能移动一个位于最顶层的盘子，且编号小的盘子不能放在编号大的盘子上面。

图1 汉诺塔问题的初始状态和目标状态

于是问题可以抽象为，给定一个初始状态、一个目标状态、一个数字n，判断是否存在一个移动序列满足在n步之内从初始状态到目标状态。在ASP中，我们通常给出一个问题的正规定义，分别对实例和编码（应用到每一个实例）详细说明。

问题实例

问题涉及以下谓词：

• peg/1：描述柱子。/后面的数字表示接收参数的个数。
• disk/1：描述盘子。
• init_on/2：描述初始状态。
• goal_on/2：描述目标状态。
• moves/1：描述在多少步以内必须到达目标状态。

当最多允许15步时，图1中的汉诺塔问题实例可由图2中的事实描述。

图2

语法糖：第1行的“;”，可以扩展为peg（a）.，peg（b）.，peg（c）.。第2行的“..”，指一个区间，即1,2,3,4。

问题编码

我们通过描述一些包含着独立于某一实例的变量的规则，来对汉诺塔问题进行编码。逻辑上把编码阶段分为四部分：Generate, Define, Test, Display。如图3所示。

图3

变量的含义：

• D：表示盘子
• P：表示柱子
• T：某次移动的序号，某个时间点
• M：移动的总长度

Generate部分包含了一条规则，其含义为在某个时间点T，有且只有一次把盘子D移到柱子P的操作能被执行。规则的头部（即:-的左边部分）由一组文字和guard（“=1”）组成，文字用“:”后面的条件来扩展。头部被称为基数约束，当真元素的数量等于guard说明的那样（即为1），基数约束满足。

在规则的体（:-的右边部分）定义了移动序号T从1递增到M。在Generate部分我们仍未定义编号小的盘子不能放在编号大的盘子上面的规则。

Define部分包含了辅助性的谓词。以下是4-9行中每条规则的含义：

• 把一次移动投影到盘子D和时间点T上。也就是说，当目标柱子P可忽略时，可以用move（D,T）代替move（D，P，T）
• 谓词on描述了某个时间点中的一个状态。初始状态中，若D在P上，则on（D,P,0）成立
• 如果在时间点T把D移动到P上，那么在时间点T盘子D在柱子P上
• 如果在时间点T盘子D在柱子P上，在T+1时未移动D，且T不是最后的时间点，那么在T+1时D仍然在P上
• 如果在时间点T盘子D在柱子P上，且T不是最后的时间点，那么在T+1时D-1不能移动到P上（谓词blocked“不能移动”的含义在Test部分定义）
• 如果在时间点T盘子D不能移动到柱子P上，那么在时间点T盘子D-1不能移动到柱子P上。递归定义。

Test部分由一系列完整性约束组成：

• 在时间点T，若盘子D-1不能移动到P上，那么盘子D也不能移动到P上。这排除了把大盘子放在小盘子上的情况和把盘子放回它之前的位置的情况。（D-1不能移动到P，是因为P上存在盘子X，X>D-1。由于D是整数，[D-1,D]没有其他整数，所以X >= D。X>D时，D自然不能放到P上；X=D时，杜绝了把D从P移动到P上的操作。）
• 在时间点T，若D被某个同样在P上的更小的盘子阻塞，那么D将不能被移动（block是指在T时刻P上存在比D大的盘子，所以D不能移动到P上。若T-1时刻D在P上，且在T时刻被block了，就意味着此时D上面有比它小的盘子，不在顶端的盘子不能被移动。）
• 当最多移动M次，目标状态为D在P上，且在时间点M，D不在P上，那么目标没有完成
• 对于每个盘子D和每个时间点T，只有一个柱子使on（D,P,T）为真。

最后在Display部分规定只有move/3的原子能被打印。

问题求解

为了求解回答集，使用下面其中一个命令：

打印输出如下：

相关定义

一个nomal logic program有如下形式：

图4

fact中包含的命题无条件地为真。fact或rule的头部A0是atom，可以为常量或函数。rule或完整性约束的体Lj为一个文字，具有形式A或者not A，分别代表正文字和负文字，其中A也是atom。

一条rule的解读：如果rule的体中所有正文字都为真，且所有负文字都被满足，那么可以推出rule的头部为真。

一条完整性约束的解读：完整性约束的体中所有文字不能同时满足。

当一个nomal logic program中所有atom满足所有的facts, rules和完整性约束，那么把这些atom的集合称为一个model。在ASP中，当model中的每个atom都可以被无环地推导时，那么这个model就是一个answer set（回答集）。

以下可以说明上述规则是如何应用的。

例1

有如下逻辑程序：

当a，b同时为假时，两条rule的体也为假，因此rule被满足，此时没有真的atom被推导出来，因此回答集为空集。

当a真b假时，对于第一条rule，体为假不能推导出头为真，因此违反了第一条rule。当a假b真时同理。

当a，b同时为真时，两条rule的体也为真，然而a、b的推导形成了环，即a依赖于b，b也依赖于a，所以这不形成一个回答集。

综上，空集是该逻辑程序唯一的回答集。

例2

有如下逻辑程序：

当a，b同时为假时，两条rule的体为真，不满足，因此不形成一个回答集。

当a真b假时，a可以在第一条rule被推导出，第二条rule也满足，a依赖于b，但不能推导出b依赖于a，因此这形成一个回答集。当a假b真时同理。

当a，b同时为真时，体为假不能推导出头为真，不满足，因此不形成一个回答集。

综上，回答集为{a}，{b}。

当我们给这个逻辑程序加上完整性约束后：

由于c是一个fact，所以它无条件为真。于是为了使完整性约束的体不满足，在这个程序中b必须为真。

例3

有如下逻辑程序：

已知企鹅不会飞，需要推导出一只黄色的鸟会不会飞。第一条rule说明一般情况下鸟会飞，第二条说明特殊情况下鸟不会飞，第三条说明了企鹅不会飞。

给黄色的鸟取名叫“tweety”，给一只企鹅取名叫“tux”，则形成了如下facts：

当我们用facts实例化变量X以后，可获得如下rules：

对以上规则进行简化后获得：

由此可知，tweety可能会飞也可能不会飞，tux不会飞，形成了两个回答集。

Classical Negation

若A是一个原子，那么-A表示A的补，也就是classical negation。 与not A不同，not A为真当且仅当A为假，但A与-A之间仅要求不能同时为真。取决于逻辑程序，-A和A可能都不存在与回答集中，因此表达了不知道A为真或为假的一种状态。-A可以出现在头部。

Disjunction（析取）

析取的逻辑程序用“;”来分隔规则头部的原子。

上面规则的头部为真当其中至少有一个原子为真。

双重否定

即not not A，not not A满足当且仅当A满足。可用于解决一些有环问题，如：

对于前者，当not not b为真，a可被推导；当not not a为真，b可被推导，因此不存在环。后者则存在环，因为a、b相互依赖。

布尔常量

布尔常量包括#true，#false，它们分别总为真和假。

内建的算术函数与内建的比较谓词

内建的算术函数包括+加，-减，*乘，/除，\取模，**指数，| |绝对值，&按位与，？按位或，^按位异或，~按位取反。使用的范例：

内建的比较谓词包括：=，!=，<，<=，>，>=。通过这些谓词连接后，表达式又可看作一个文字。使用的范例：

除了整数，比较还可以应用在常量和函数上。整数的比较使用的是常规的方法，常量的比较使用字典序，而函数的比较既是结构性的也是字典序的（？）。所有整数小于常量，常量小于函数。

除此以外，“=”还有赋值的用法。在下例中：

规则的体定义了4个用“=”连接的比较谓词，他们都直接或间接地依赖于X、Y，X、Y的值由num/1给出。XX = X*X给出了XX的值，同理Y*Y = YY给出了YY的值。在Y’-1 = Y中，由于其中包含的是简单的算术运算，所以Y’的值也能由Y+1得出。由于现在Y’*Y’ = XX+YY每个变量的值都已得出，所以它只是在比较左右两边是否相等。

区间

整数区间[i, j]可以用i..j表示，例如1..3表示整数1,2,3。

Pooling

用“;”分割参数，以提供不同选择。(... ,X;Y,... )即相当于（...，X），（Y,...）。Pools的展开跟区间一样。事实上，1..3就相当于（1；2；3）。

条件与条件文字

条件文字的形式：，其中每个Li都是文字，L1，...，Ln称为条件。在下例中：

当c为假或者b、c同时为真时，a能被推导。（所以条件文字b : c的真值就跟蕴含式c => b一样）

由于在条件的体中，各文字也是用“,”相连的，所以当条件出现在规则的体时，容易与后续文字产生混淆。为了进行区分，条件结束时使用的是“;”，如下例所示：

下例说明了条件在头部和体部时，实例化后分别如何展开：

第5、6行的规则实例化为：

在第5行中，X通过person/1实例化后，有了meet :- avaliable（jane）和meet :- avaliable（john）两条规则。它们由同一条规则实例化而来，且头部包含相同的原子，因此可以合成为meet :- available(jane), available(john)。

在第6行中，X通过day/1实例化后，有了5条规则。它们由同一条规则实例化而来，但是头部的原子不同，因此不能合并，而是不同的5条规则。

聚合

聚合用来计算一组项的某些值。正式地，聚合是使用条件的一组元组上的函数。通过比较聚合值和给定值，我们可以得出聚合原子的真值。

例如：

G-L规约

Gelfond和Lifschitz(1988)提出了稳定模型语义，稳定模型语义解决了非单调推理无法解释失败即否定的问题，此外他们还给出了一个规约方法(G-L规约)，以化简一个ASP逻辑程序中的失败即否定。

G-L规约的定义：给定原子集S和不含约束的ASP逻辑程序P，P基于S的G-L规约结果记为PS。P通过以下两个化简规则得到PS：

• 若一个规则的体部中有not p，且p∈S，则删掉该规则；
• 对剩下的所有规则，删除体部中的not p，p为Atoms(P)中任意一个原子。

所以进行G-L规约的步骤就是：首先找出给定的原子集；然后找逻辑程序中所有包含not p文字的规则；如果p∈S，则删掉该规则，否则只删除not p。

根据G-L规约的规则，P中第二条规则的负文字中包含S里的原子，所以直接删掉；P中第三条规则的负文字中包含S以外的原子，所以只把负文字删掉。所以PS为：

显然，通过G-L规约进行化简后得到的PS是一个不包含任何失败即否定的ASP逻辑程序。这样的ASP逻辑程序只有一个唯一的极小模型，这个模型被称为稳定模型，并记为Cons(PS)。对于包含有约束的ASP逻辑程序，我们可以通过G-L规约来定义其回答集，通过对程序中的约束和一般规则分离判断即可。

运用G-L规约的过程体现了一种求解回答集的思路，即不断测试。