4.1.3 3C算法
本节围绕着提高回溯效率的目标,提出解决上述问题的3C(Conflict-directed backjumping,forward Checking,Closure)算法。3个方法共同完成BFS-BB的回溯操作,并在BFS-BB原型系统内被整合为一个高效的约束求解引擎。
1.前向检查
每次变量赋值通过区间运算判断都会产生很大计算量,而很多变量区间本身不可达,在不可达区间内所做的运算实际上是无用的。因此,在搜索过程中,可通过区间运算对未来变量区间进行前向检查,动态去除不可达区间。同时,由于区间运算的保守性,可以确保非不可达区间都得到保留。这种处理策略相当于在每次运算量较大的区间运算前加了一道“过滤网”(图4-4),只有判定非不可达才会进行后续的区间运算,从而尽量多地剪枝,这样可以减少执行时间并提高求解效率。
图4-4 前向检查策略对未来变量区间削减示意图
前向检查通过区间运算完成。为了更好地描述前向检查的过程,我们给出分支条件的定义。
定义4-1 令B为一个布尔变量的集合{true,false},D a是第a个分支前所有变量区间的集合,如果路径上有k个分支,那么分支条件Br(n qa,nqa+1):Da→B(a∈[1,k])可以通过式(4-1)计算,其中nqa是一个分支节点。
在式(4-1)中,D a满足前面的a-1个分支条件并且是计算第a个分支条件的输入,而
是一个临时区间,是通过Da计算Br(n qa,n qa+1)的结果且它满足第a个分支条件。如果D a∩
≠∅,则可以确定Da∩
既满足前面的a-1个分支条件,也满足第a个分支条件,区间运算可以继续向下判断剩下的分支条件。这个过程可以通过图4-5(a)看出来。如果D a∩D ~a=∅,则说明至少有一个变量(可能是个未来变量)的区间被消除且分支条件没有得到满足。若路径上有k个分支节点,则所对应的k个分支函数都为true才能保证路径可达(分支条件得到满足);否则,若少于k个分支条件为true,则分支函数取值为false的分支需要被定位出来并对矛盾的情况进行分析。对于分支条件Br(n qa,nqa+1)(a∈[1,k])是否能够为true的判断取决于两个区间的取值,即进入第a个分支的变量区间D a(满足前面的a-1个分支条件)和满足第a个分支条件的变量区间
,后者是将前者代入Br(n qa,nqa+1)计算的结果。
在我们的方法中,计算一个分支条件被认为是一次约束检查,与类似AC-3那样的弧一致性检查方法(4.2.1节)相比这其实是一种粗粒度的检查方式。可以看到,在区间运算过程中,总是所有变量的区间集而不是具体的值参加运算,这就导致了可能比较粗的区间削减和区间消除,当然其中也包括未来变量。
图4-5 区间运算检测矛盾的过程
为了简便起见,我们假定变量被赋值的顺序与预设的顺序是一样的,即x 1,x 2,…,x n。但是在实际的执行过程中,所使用的是动态排序方法,也就是说,下面对哪个变量进行赋值取决于当前的搜索状态。令当前变量为x i,前向检查的输入是所有变量的区间集,标记为{[V 1,V 1],[V 2,V 2],…,[V i,V i],D i+1,…,D n},它包括3个部分:过去变量的区间都是一个确定值(上、下界相同),通过了前向检查的一致性检查;当前变量的区间([V i,V i])是一个确定值(上、下界相同),正在进行前向检查的一致性检查;未来变量的区间基本上是一个值的范围,已经通过前面执行的前向检查对区间进行了过滤并且会通过当前的前向检查进一步得到过滤。由于前向检查的主要目的是判断当前变量x i的赋值V i是否会导致不一致或可能的区间消除,因此我们使用forward check(V i)来标识当前的前向检查。
2.矛盾驱动的回跳
矛盾驱动的回跳其关键是确定引起矛盾的变量所在的层次。在区间运算遇到矛盾(即检测到空区间)时,通过对矛盾信息的分析来定位矛盾变量(即导致空区间产生的变量,有可能不是当前变量),从而跨越不相关变量直接回跳到矛盾变量所在的层次(图4-6)重新赋值。由图4-6可以看出,一个回溯搜索可以被看作对搜索树的遍历,我们给出如下定义。
定义4-2 变量的层次标识其在搜索过程中被赋值的顺序,它与已经被赋值的变量个数相同。例如,0层代表搜索树的根节点,没有变量被赋值;1层代表x 1,它是第一个被赋值的变量,依此类推。距离根节点更近的节点是浅层节点,而距离根节点更远的节点是深层节点。(https://www.daowen.com)
从图4-6也可以看出,CBJ的回跳不是在相邻的层次间展开的。由于回跳是受矛盾驱动,下面给出一些与矛盾相关的定义。
图4-6 回跳机制工作方式示意图
定义4-3 如果两个变量x i和x j有关系r h∈R(h∈[1,k]),那么x i和x j之间互相是直接相关变量。x i的直接相关变量的集合记作S rel(x i)。从测试用例生成来说,在同一个谓词内的变量之间互相是直接相关变量。
定义4-4 能够直接或间接由任何带有x i的关系中所推导出的变量集合构成了x i的闭包,记作C(x i),并通过迭代使用式(4-2)来计算。
一个变量的闭包是这样的一个数据结构:它存储这个变量及所有与它有直接和间接关系的变量,这是一个映射,从一个变量指向所有路径上与它有关系的变量。所述变量都是符号变量,通过图4-7所示的简单例子说明。
图4-7 程序test
如果我们试图生成经过所有的if语句到达最后的打印语句的那条路径,那么路径上的符号变量及每个变量的闭包如表4-1所示。
表4-1 程序test的符号变量及闭包
续表
由于x 1对应的符号变量是x 2+1,所以x 1实际上是路径的一个不相关变量,也没有必要对其进行赋值,将一个随机值赋给它就可以满足路径上的约束,且它的闭包为∅。x 3也是同样的情况。我们在以前的工作中已经完成了不相关变量移除工作,将路径上的变量分为相关变量和不相关变量。为了简便起见,在本节我们认为所讨论的变量都是路径的相关变量。
基于上述分析,可以断定如果是由于任何已赋值变量导致了当前的不一致,那么那个赋值一定发生在与当前变量在同一闭包内的一个或多个变量之上。下面是关于矛盾变量的定义。
定义4-5 如果当前赋值＜x i,V i＞导致了不一致,且有一个过去变量的集合,这个集合中的变量与x i在同一闭包内且相应的区间被消除,那么其中层次最浅的变量x j是当前不一致的矛盾变量。
