归结演绎的归结策略课件

,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,归结反演系统面临着大子句集而引起的演绎效率问题。,若盲目地随机选择子句对进行归结，不仅要耗费许多时间，而且还会因为归结出了许多无用的归结式而过分扩张了子句集，从而浪费了时空，并降低了效率。,解决问题的关键在于,选择有利于导致快速产生空子句,的子句对进行归结,。,归结反演系统面临着大子句集而引起的演绎效率问题。若盲目地随,1,归结策略,删除策略,：,限制策略：,通过,删除,某些,无用,的子句来,缩小,归结的范围,通过设置,选用条件,对参与归结的子句进行种种,限制,，,减少,归结的盲目性,，,如,支持集、线性输入、单文字子句优先、祖先过滤,等策略。,归结策略删除策略：限制策略：通过删除某些无用的子句来缩小归结,2,广度优先策略,广度优先是一种穷尽子句比较的复杂搜索方法,广度优先策略广度优先是一种穷尽子句比较的复杂搜索方法,3,广度优先的归结过程：,设初始子句集为,S,0,归结过程如下：,从,S,0,出发，对,S,0,中的全部子句作所有可能的归结，,得到第一层归结式，把这些归结式的集合记为,S,1,。,2.,用,S,0,中的子句与,S,1,中的子句作所有可能的归结，,得到第二层归结式，把这些归结式的集合记为,S,2,。,3.,用,S,0,和,S,1,中的子句与,S,2,中的子句作所有可能的归,结，得到第三层归结式，把这些归结式的集合记为,S,3,。,如此继续,直到得到空子句。,广度优先的归结过程：设初始子句集为S0,归结过程如下：从S0,4,例：子句集,S=,I(x)R(x),I(a),R(x)L(y),L(a),S,:,S,0,:,R(a),I(x)L(x),I(x)R(x),I(a),R(x)L(y),L(a),R(a),S,1,:,L(a),L(a),I(a),I(a),NIL,广度优先策略归结出了许多无用的子句，既浪费时间，有浪费空间。容易引起组合爆炸。,P(A),例：子句集S=I(x)R(x),I(a),R(x),5,当问题有解时，用广度优先策略归结能保证找到最短路径。因此，它是一种完备的归结策略。,当问题有解时，用广度优先策略归结能保证找到最短路径。因此，它,6,支持集策略,要求每依次参加归结的两个亲本子句中，至少应该有一个是由目标公式的否定所得到的子句或它们的后裔。,支持集策略要求每依次参加归结的两个亲本子句中，至少应该有一个,7,支持集策略是完备的，即当子句集不可满足时，由支持集策略一定能够归结出一个空子句。,支持集策略是完备的，即当子句集不可满足时，由支持集策略一定能,8,例：子句集,S=,I(x)R(x),I(a),R(x)L(y),L(a),S,:,S,0,:,R(a),I(x)L(x),I(x)R(x),I(a),R(x)L(y),L(a),S,1,:,L(a),L(a),I(a),NIL,S,3,:,例：子句集S=I(x)R(x),I(a),R(x),9,删除策略,归结时将,无用,的子句,删除,掉，缩小搜索范围，减少比较次数，从而提高归结效率。,删除策略归结时将无用的子句删除掉，缩小搜索范围，减少比较次数,10,常用的删除方法：,（,1,）纯文字删除法,纯文字,：如果文字,L,在子句集中不存在与其互补的文字,L,，则称该文字为纯文字。,例：对于子句集,S=P,Q R,Q R,Q,R,其中,P,为纯文字，因此，,P,Q R,可从,S,中删除。,常用的删除方法：（1）纯文字删除法纯文字：如果文字L在子句集,11,（,2,）重言式删除法,重言式,：如果一个子句中包含有互补的文字对，则称该子句为重言式,。,例：,P(x),P(x),、,P(x),Q(x),P(x),（2）重言式删除法重言式：如果一个子句中包含有互补的文字对，,12,（,3,）包孕删除法,例：,P(x),包孕于,P(y),Q(z)s=y/x,P(x),包孕于,P(a)s=a/x,P(x),Q(z),包孕于,P(f(x),Q(a),R(y),s=f(a)/x),a/z,设有子句,C1,和,C2,，如果存在一个置换,s,使得,C1s,C2,，则称,C1,包孕于,C2,。,（3）包孕删除法例：设有子句C1和C2，如果存在一个置换s,13,单文字子句策略,要求每次参加归结的两个亲本子句至少有一个子句是,单文字子句,单文字子句策略要求每次参加归结的两个亲本子句至少有一个子句,14,单文字子句,：如果一个子句只包含一个文字，则称此子句为单文字子句,。,例：子句集,S=,I(x)R(x),I(a),R(x)L(y),L(a),S,:,S,0,:,R(a),I(x)R(x),I(a),R(x)L(y),L(a),R(a),NIL,采用单文字子句策略，归结式包含的文字数将少于其亲本子句中的文字数，这将有利于向空子句的方向发展。,但这种归结策略是不完备的。即当子句集为不可满足时，用这种归结策略不一定能归结出空子句。,单文字子句：如果一个子句只包含一个文字，则称此子句为单文字子,15,线性输入策略,要求每次参加归结的来年各个亲本子句中，至少应该有一个是初始子句集中的子句。,线性输入策略要求每次参加归结的来年各个亲本子句中，至少应该有,16,例：子句集,S=,I(x)R(x),I(a),R(x)L(y),L(a),S,:,S,0,:,R(a),I(x)L(x),I(x)R(x),I(a),R(x)L(y),L(a),R(a),S,1,:,I(a),L(a),L(a),I(a),NIL,线性输入策略可限制生成归结式的数目，具有简单高效的优点，但也是一种不完备的策略。,例：子句集S=I(x)R(x),I(a),R(x),17,例：子句集：,S=Q(u),P(a),Q(w),P(w),Q(x),P(x),Q(y),P(y),从,S,出发和容易找到一克归结反演树，却不存在线性输入策略的归结反演树。,例：子句集：S=Q(u)P(a),Q(w),18,祖先过滤策略,每次参加归结的两个亲本子句，只要满足以下两个条件中的任意一个就可进行归结：,（,1,）两个亲本子句中至少有一个是初始子句集中的子句。,（,2,）如果两个亲本子句都不是初始子句集中的子句，则一个子句应该是另一个子句的先辈子句。,祖先过滤策略每次参加归结的两个亲本子句，只要满足以下两个条件,19,例：子句集：,S=,Q(x),P(x),Q(y),P(y),Q(w),P(w),Q(a),P(A),用祖先过滤策略证明,S,为不可满足。,Q(x),P(x),Q(y),P(y),P(x),Q(w),P(w),Q(w),Q(a),P(A),P(A),NIL,可以证明祖先过滤策略也是完备的。,例：子句集：S=Q(x)P(x),Q(y,20,实际应用中可以将几种策略结合起来使用。在选择归结反演策略时，主要应考虑其完备性和效率问题。,实际应用中可以将几种策略结合起来使用。在选择归结反演策略时，,21,作业,1,：设有子句集：,P(x),Q(x,b),P(a),Q(a,b),Q(a,f(a),P(x),Q(x,x),，分别用各种归结策略求出其归结式。,作业,2,：对子句集：,P,Q,Q,R,R,W,R,P,W,Q,Q,R,用线性输入策略是否可证明该子句的不可满足性？,作业1：设有子句集：作业2：对子句集：P Q,Q R,22,