ASP回答集编程gringo指导
ANSWER SET PROGRAMMING
Section 1 前⾔
这个教程主要是介绍gringo、clasp、clingo和iclingo。..
第⼆节，通过⼀个例⼦达到介绍使⽤逻辑程序建模和gringo这种建模语⾔。
第三节，通过介绍我们整合了gringo和clingo的⼯具的输⼊语⾔。并在第四节中会阐释三个著名的例⼦。第五第六节则会介绍⼀些⽐较特殊的⽅⾯，并给出⼩提⽰和有⽤的相关错误以及警告的命令⾏选项。
这个教程中不会做过多的理论背景介绍。1153 8008203588
如果你熟悉lpar（⼀种经典的smodels前端执⾏器，反正我是不知道），那么附录A中会列出它跟我们这个⼯具的主要区别。。。。。。。。balabala
后⾯有很多例程，⼤部分都是能运⾏的，‘\’这个符号意味着后⾯要接⼀段字符。OK，现在要开始了哦。
Section 2 ⼩例程
这节，我们会通过⼀个简单的hanoi puzzle来展⽰gringo的强⼤之处。这有三个⽊杆和⼀些不同⼤⼩的能放置在⽊杆上的盘⼦。⽬标是把最左边那个⽊杆的所有盘⼦移动到最右边，盘⼦只能放置⽐他⾃⼰⼤的盘⼦上。这⾥暂且不讨论最优⽅案，⽽仅仅关注如何解决。
在ASP中，习惯于⼀种统⼀的问题描述。从这个⽅法论出发，我们把编码从下⾯这个问题中分割出来：给定了初始位置的盘⼦，⼀个⽬标，⼀个数字n，问是否有⼀个长度是n的序列满⾜给定的条件。我们可以看出这个问题就很优雅的被简化为⼀个能够⽤ASP解决的描述性问题
2.1 例⼦
⽤谓词peg/1和disk/1来表⽰⽊杆和盘⼦。⽤正整数来表⽰盘⼦，越⼩的数字表⽰越⼤的盘⼦。⽊杆呢就有⾃⼰的名字，谓词init_on/2 和goal_on/2 表⽰的是初始和⽬标状态。第⼀个参数是盘⼦的数量，第⼆个参数是盘⼦被放置在初始和⽬标状态上的⽊杆。最后，谓词moves/1 表⽰达到⽬标状态的步数。注意，这个问题的条件是三个⽊杆和固定的初始与⽬标状态。通过ASP 我们可以很简单的转变这个要求和编码，下⾯会结合特定数量的⽊杆和某种初始与⽬标状态来介绍。Figure 1是⼀种可能的例⼦，虚线那个就是⽬标状态，⽤ASP编程的话就是：
1中的“;”是⼀种拓展了的语法糖（ction 3.1.9），代指peg(a) , peg(b) , peg(c)这三个⽊杆。同理，2中的也是⼀种语法糖（3.1.7），代指disc(1),disc(2), disc(3) , disc(4) ，这四个盘⼦。4、5是初始与⽬
标状态。最后⼀⾏给出了解决这个问题的步数。
2.2 问题编码
现在可以⽤ non-ground 规则（3.1.1）处理hanoi的编码了。规则中的变量在各个实例中是独⽴的。通常⼀个编码会包括⼀个 Generate，⼀个Define和⼀个Test。我们也遵从这个范例，并⽤%作为⾏注释的开头。变量D,P,T和M分别指代disks盘⼦，pegs⽊杆，步数序列中的第T 步，和这个序列的长度。
Generate部分只有⼀⾏，即第2⾏。⼀步的意思即把任意的⼀个盘⼦放到任意的⼀个⽊杆中。规则的头部被称为cardinality
constraint（3.1.10），包含⼀个⽤谓词扩展冒号的集合（3.1.8），并且是⽤下限与上界范围的。这个constraint是真的，当且仅当这个范围⾥的所有⼦集满⾜时。另外这个constraint被⽤在规则的头部，除了测试（不解）还可以引导出⼀个新的原⼦，在我们这个例⼦中就是指盘⼦的步数。注意到，我们现在并没有限制步数。当⽬前为⽌，任何盘⼦都可以被移动到任何⽊杆上，⽽不必考虑任何限制条件。
接下来，我们给出新的辅助谓词，它并不直接满⾜问题但是被⽤于后⾯的Test测试部分。第4⾏的规则指出⼀步的⽬标⽊杆，谓词move/2 ⽤在我们移动⼀步时的盘⼦，但是并不介意放在哪。⽤谓词on/3来
表⽰hanoi问题每⼀步的状态。前⾯两个参数给出盘⼦在第三个参数时的位置，第3个参数是执⾏到第⼏步的意思。下⼀⾏，第5⾏指出在初始状态（0 步时）时的每个盘⼦的位置。我们⽤规则6和7来描述状态的转移。6⾏的意思很明确。注意⼀下not moves(T)的⽤法，由于最后⼀步之后就不会再改变了所以是有限的步骤。7⾏的规则确保盘⼦的每⼀步都是会移动的。
如果下次⼀次没有移动这个盘⼦，那么这个盘⼦仍然在原来的位置。（不过我不理解后⾯的not moves(T)是啥意思）。。。。
最后我们来定义⼀下辅助谓词blocked/3
这是⽤来记录不能放盘⼦的⽊杆的位置w.r.t。第8⾏说明⼀些盘⼦在⼀些⽊杆上是blocked的，即下⼀步的时候不能把编号较⼩的（也就是⾯积较⼤的）盘⼦放上来。9⾏如果盘⼦是在blocked阻塞的位置上就意味着这个盘⼦blocked阻塞了。Blocked阻塞的位置被标记为0，这对断⾔⼀个多余的步骤很⽅便。
最后，test部分构建了Generate和Define部分不能全部满⾜的条件。第⼀个完整的限制条件是11⾏，倘若在某个⽊杆上的编号⼩点的盘⼦在第T步时是blocked的，说明已经有⼩盘⼦在那⾥了。如果是恰好⼩⼀个单位的盘⼦已经在那⾥了，则此时也不能重复放置；如果是⼩2个以上单位的盘⼦在那⾥，那这个⼩⼀个单位的盘⼦也放不上。看看D-1这个的⽤法，盘⼦是不能被重复放到同⼀位置的。12的
限制条件，盘⼦只能被放在⽐他⼤的盘⼦上，如果她的下⼀步是blocked的，则下⼀步不能移动了。13⾏，是⽬标状态。为了让编码更有效率，14⾏添加了⼀个冗余条件：每个盘⼦在任何时刻都只能被放置在⼀个⽊杆上。尽管上⾯的条件已经暗含这个了，但添加这个额外的领域知识能够提⾼解题速度。后⾯的两⾏在解出时控制谓词的打印。15隐藏了所有谓词⽽只展⽰了move/3
不理解之处：not moves(T)，13⾏
2.3 题解
终于到解题的时候了（先确定你是否安装了clingo、gringo、clasp，最好是能添加进系统变量的path中）。
除了SATISFIABLE之外，还有UNSATISFIABLE,UNKNOW.。那个1+是只⽬前找到了⼀个，但其实搜索空间中还没找完，也许还有解答。蛋糕口味
3 输⼊语⾔
这节简要阐释gringo所⽤的语⾔，结合clingo、以及递增（翻译执⾏器。。。这个翻译不靠谱，我实在搞不清楚incremental grounder and solver是神马意思）iclingo，solver clasp。3.1节会介绍gringo和clingo的输⼊语⾔。3.2则会⽤⼀些指令拓展iclingo。最后在3.3节则主要是clasp的操作。
3.1 gringo和clingo的输⼊语⾔
Gringo是把逻辑语⾔翻译成等价的ground 语⾔。Gringo的输出可以通过管道输⼊到clasp，然后计算出回答集。Clingo的内部包含了gringo 和clasp，也即两只功能都有。
通常⽂本⽂档中明确的逻辑语⾔被gringo或者clingo通过命令⾏调⽤。下⾯我们将描述gringo和clingo的输⼊语⾔。
3.1.1常规语⾔与完整性约束
每种逻辑语⾔都是⽤术语构成的（应该得先做词法分析吧）。Figure 2 简易阐释了gringo的术语。最基本的术语就是整数、常量和变量。除此之外，还有⼀些特殊变量和常量。匿名变量⽤’_’（下划线）表⽰，它近似于普通的变量只不过任何⼀次‘_’的出现都被认为是另⼀个变量（那种没有重复利⽤价值的变量就可以⽤这个啦）。额外的，还有两种特殊常量’ #supremum’ 和’ #infimum’，上确界和下确界。最后，⽤其他术语构成函数标⽰。更复杂的术语将在以后介绍。
规则的构造：
规则或者事实的头部A0是⼀个原⼦，类似函数标⽰或者常量。关于这些语法的解释，可以参照⼀⽚博客
/2012/04/answer-t-programming/。。
引⽤“
⼀个ASP程序包括两样重要的部分：事实，⽤于描述现实世界的状态。还有规则，⽤于进⾏推理，并且他们都由英⽂句号'.'结尾。⽽规则⼜分为在符号':-'左边的结论和右边的条件。结论成⽴，如果右边的条件被满⾜。另外事实也可以看做是省略了符号':-'和右边所有条件的规则。更细分⼀点，每⼀个ASP程序⾥还包括了⼀些常量（在这⾥就是城市名），谓词（这⾥的road，arrive什么的），每个谓词有若⼲个参数，并且为了简化起见，我们把带有n个参数的谓词p写作p/n。最后当然还有变量（在这⾥就是⼤写字母X和Y），需要注意的是本质上ASP程序是不⽀持变量的，这⾥的变量仅仅是为了⽅便书写，在实际的求解中这些变量会被替换为程序中出现的所有常量，这也是我们为什么需要先运⾏gringo程序的原因，它的作⽤就是将程序⾥所有变量挨个替换成程序⾥出现的所有常量，你可以⽤：
gringo --text road
手表测血压准吗来看看程序被替换后的样⼦。
现在让我们来定义⼀下ASP程序⾥各种规则的样⼦，有了这些，我们就可以⽤它来解决问题了。
1. 约束规则
所有在符号':-'左边什么都没有的规则就是约束规则，它表⽰右边的条件不能同时被全部满⾜。
学播音主持2. 选择规则
所有在符号':-'左边形如 {a1,a2,...,am} 的规则就是选择规则，其含义是如果右边条件成⽴，那么左边的任意⼀个⼦集也成⽴。
下⾯我们来考虑⼀下对于选择规则的扩展，⾸先我们不限制{a1,a2,...,am}这样的元素只能出现在规则左边，⽽是也可以出现在规则右边。其次，任意⼦集的说法也未免太简单了，我们给它加上个数限制，像l{a1,a2,...,am}u，这个元素表明花括号中的m个元素最少有l个最多有u个成⽴。所以形如
a :- 2 {b, c, d, e} 3.
这样的式⼦就表明如果b, c, d, e中最少有两个最多有三个元素成⽴，那么a也成⽴。当然，这⾥的l或者u并⾮必须同时出现，只写⼀个也是可以的，含义也很好理解。
3. 条件元素
数学⾥⼤家想必遇见过诸如 {a|a∈A} 这样的东西，它表⽰了所有满⾜ a 属于 A 的元素 a 的集合，这⾥我们也有类似的东西。⽐如说顶点着⾊问题，假设我们有诸如 vertex_color(X, Y) 这样的元素，我们想
让它代表顶点X被染了颜⾊Y，并以此得到某⼀顶点v1所有的染⾊可能性。但是我们之前也说了，gringo会将程序⾥的所有变量拿所有常量替换⼀遍，这样Y不仅会被拿颜⾊替换，同时也会被拿顶点替换，这显然不是我们想要的，这时我们就需要条件元素了：
vertex_color(v1, Y)：color(Y) :- vertex(v1).
看到了么？只需要⽤冒号':'就可以将变量Y限定在颜⾊的范围内，这样我们得到的就是顶点v1所有的着⾊可能了。需要说明的是条件并⾮只能加⼀个，如果你有多个变量需要做限制的话，可以将冒号⼀直连下去。
那么冗长⽆聊的语法介绍就先到此为⽌吧，我们来⽤⼀个例⼦来介绍如何来撰写⼀个ASP程序。我们所⽤的例⼦就是著名的，如何在8*8的国际象棋棋盘上摆放8个皇后⽽使他们⽆法相互攻击。
⾸先是事实，我们的棋盘有8⾏8列：
早春呈水部张十八员外1 row(1..8).
2 col(1..8).
这⾥我们⽤1..8来代表从1到8的简写，这样的式⼦会被展开为row(1). row(2).等等直到row(8).
之后就是各个规则了，⾸先我们需要在 I ⾏ J 列上放置皇后：
queen(I, J) : row(I) : col(J).
这还不够，因为我们放且只能放8个皇后，所以我们把这个规则改写⼀下：
8 {queen(I, J) : row(I) : col(J) } 8
好了，到此为⽌如果你好奇的话可以像上⾯的例⼦那样先执⾏⼀下看看结果是什么，不过千万要记得把clasp后⾯的0换成5来表⽰只计算5种满⾜条件的结果，毕竟我们现在可以说什么限制都没有加，所有结果的数量多的可怕。另外，因为我们只关⼼queen的情况，⽽你会发现程序把row和col的结果都打印出来了，所以我们可以⽤
1 #hide.
2 #show queen/2.
来将结果显⽰限定在谓词queen上⽽隐藏其他的谓词。好了，到现在你会发现得到的结果只是随便把8个皇后放到棋盘上，根本没有考虑他们之间有没有攻击的问题，那么之后我们就来添加这些限制，⾸先是每⾏每列上不能同时有两个皇后：
1 :- queen(I, J1), queen(I, J2), J1 != J2.
2 :- queen(I1, J), queen(I2, J), I1 != I2.
最后，对⾓线上也不能同时有两个皇后：
1 :- queen(I1, J1), queen(I2, J2), I1 != I2,
2 J1 != J2, I1 - J1 == I2 - J2.
3 :- queen(I1, J1), queen(I2, J2), I1 != I2,
4 J1 != J2, I1 + J1 == I2 + J2.
到现在为⽌我们的程序就完成了，运⾏来看看结果吧。很有趣不是么，我们没有教计算机如何计算，只是描述了整个问题，计算机就把结果告诉了我们。当然这⾥介绍的只是冰⼭⼀⾓，限于篇幅和我的⽔平也没法更加详细的介绍了，如果你有兴趣的话，有不少⽂档可以供参考，如果能把你拉下⽔，那么我的⽬的也达到了。
注：也许很多⼈在这⾥的第⼀反应是⽤否定的 ¬block(X,Y). ⽽不是什么奇怪的not，这其实牵扯到推理的问题，不过限于篇幅这个就不扯了，⼤家可以⾃⼰去找找资料。
”
Gringo期望规则是安全的，即所有的出现在规则中的变量会被⼀些正的短语所替换。⼀个谓词中包含变量，则称这个谓词绑定了这个变量。另外，这些推到必须是⾮循环的。⼀个简单的例⼦， a :- b . B :- a . 这个程序的回答集是空集。Finally, note that default negation is ignored when checking for acyclic derivations (we do not need a reason for an atom being fal)。默认的否定被⽤来表⽰选择。例如，a :- not b . b :- not a，有两个回答集{a} {b}。只不过⼀般我们不⽤这个来表⽰选择，像是第2节中的例⼦，我们⽤cardinality constraint，因为它更具有可读性。
3.1.2 经典否定
逻辑程序中，not表达的是默认否定，即短语 not A是指不需要A来推导。相反，在⼀些命题的经典的否定中，指命题的补集能够推导出。经典否定中是⽤原⼦前的标⽰’-’符号。如果A是原⼦，那么-A就是A的补集。从语义上理解，-A只是⼀个简单的新原⼦，A与-A不能同时满⾜。经典否定只是⼀个语法特性，能通过完整性约束实现。
Example 3.1
下⾯⽤完整性约束来实现经典否定
这个程序有两个回答集，{ files(tweety)} {-flies(tweety)}。为什么？？？？
我执⾏过后回答集是{files(tweety)} {-files(tux)}
现在我们添加⼀个新的事
实：
8 files ( tux ) .
此时，通过经典否定这个新程序就不再有回答集了。可能的回答集同时包含files(tux) 和 -flies(tux)，这便和完整性约束的第6⾏冲突了。
3.1.3 disjunction析取
规则头部的原⼦之间可以⽤ ‘ | ’连接。额外的，逻辑程序必须满⾜的最低限度标准（这篇教程不会细讲）。⼀个简单的程序 a | b 。有2个回答集 {a} 和{b}，但是却不允许a,b因为这不是最⼩的模型。
通常，disjunction析取会增加计算的复杂性。这也就是为什么clingo、assat、clasp、nomore++、smodels、等不想解决disjunctive programs。claspD，cmodels或者gnt需要被⽤来解决disjunct progr
am。我们建议使⽤“choice construct”选择结构（3.1.10）⽽不是disjunction，除⾮这⾮常有必要。
3.1.4 内建算数函数
Gringo和clingo⽀持不少算术函数。下⾯的标⽰就是这些函数：+ 加，- 减，* 乘，/ 或者 #div 整数除，\ 或者#mod 求余，** 或者#pow 次⽅，|·| 或者 #abs 绝对值, & 与，？或，^ 或⾮，‐补。
Example3.2
变量L和R是7 和2的实例，‘（’前的那些空格是可以⽆视的，⽽#div和#mod后⾯的空格则是强制性的，还有那些需要⽤括号包起来的。
提醒⼀点，算术函数作⽤域内的变量并不受相关原⼦的约束。例如，规则 P(X) :- P(X+1) 这是不安全，但是 P(X-1） :- P(X)是安全的。尽管后⾯这种会产⽣⽆尽量的式⼦，但是gringo⾃⼰会避开这种输⼊
3.1.5 内建⽐较谓词
下⾯的内建谓词在规则体内包含⽐较词： == 相等， != 不等， < ⼩于 <=。。。。。。。
苏格兰口音Example 3.3 ⽤法
最后2⾏指出，事实上，算术函数在⽐较谓词之前被估算，然后在⽐较那2个整数。所有的⽐较谓词能够⽤在任意的词法中。
整数是⽤普通的⽐较⽅式，⽽常量采⽤字典序。函数标⽰⾸先⽤他们的参数数量来⽐较。如果参数数量不同，函数标⽰的名称⽤⽤字典序⽐较。如果名称也不同，then the arguments are compared component wi(不理解)。最后，整数总是被常量⼩，⽽常量则⽐函数标⽰⼩。
需要明确，内建⽐较谓词不能绑定变量。当检测哪个规则是安全的时，⽐较谓词不会被考虑。
3.1.6 赋值
内建谓词 := 和 = 被⽤在规则体中，类似赋值吧
韩国护肤品牌Example 3.4 这个例⼦讲述如何将变量赋值给术语。
第3⾏包含4个赋值，右侧的那些直接或者间接依赖于X和Y。这2个变量在第5⾏中⽤谓词的原⼦ num/1 绑定。同时也看到了内建⽐较谓词==的另⼀种⽤法。
num(X),num(Y)，限定了X和Y是1-5.同时⼜X < Y，且 Y1=Y+1.。。。这根本就是解⽅程，只不过这是⽤描述⽅程的⽅式。
Example 3.5 这次我们换成在左边来⽤ :=
注意⼀下 f (a,X,X+1)。X+1会被推迟，稍后再检查。所以，第4⾏等价于：
赋值语句也是可以绑定变量的，但是循环赋值就不⾏了。有⼀个限制是，右边的赋值语句需要绑定到⼀些谓词中（不理解）。
3.1.7 区间
在例⼦3.4中，有5个事实， num(k)表⽰连续的整数k。Gringo和clingo⽀持i..j的整数区间，也即 i <= k <= j，会在类似编译的时候扩展处理。
Example 3.6
很简单。。。
举个例⼦，X是9则第4⾏：
拓展出来
3.1.8 条件
这点我在上⾯的引⽤的博客中也指出了。 :
Example 3.7 在规则体和规则的头部应⽤了条件语句
5、6相当于
这个容易理解。。。。。。
也可以⽤复合条件，⽐如加上 not
条件语句有三个要点：
由零开始
1，右侧的原⼦谓词需是domain 谓词
2，条件语句中出现的变量被视为local的，也即在条件之外不能⽤绑定变量。条件语句之外的变量是全局变量，条件语句前端原⼦钟的变量必须是在右侧的或者全局的。
3，全局变量的优先级⽐较⾼。
3.1.9 pooling汇总
符号“；”，这使得程序更加简洁。例如⼀开始的例⼦中
peg ( a ; b ; c ). 相当于 peg( a). peg( b). peg( c).
位于规则体中的“；”是⽤连接符扩展，⽽规则头的则是扩展成多个规则
Example 3.8
把规则3扩展⼀下可得
rocher另外，还有符号“；；”，⽤于分割谓词的参数。它并不在⼀个术语中使⽤⽽是⽤来列出谓词的参数，具体的扩展⽅式与“；”⼀样。Example 3.9 “；”与“；；”的区别
2与3相应的扩展成：
3.1.10 聚合
在⼀个词法集合中估算正确性。其形式为：
有上界u，下界l。操作符 op，集合 Li,，每个元素有权重 Wi。如果⽤这个操作符操作每个元素其权重介于区间之内就为真。Gringo⽀持聚合#sum (所有权重之和)， #min （最⼩权重），#max （最⼤权重） #avg （平均权重）。还有3个句法不同的聚合，
#count 等价于所有权重为1时的#sum
还有
如果Li为真的数量是偶数则式⼦为真。反之
通常权重都默认为1 。操作符也被默认为 #sum。
