2.5. 搜索¶

2.5.1. 有限域搜索¶

利用有限域求解器搜索涉及到检查变量剩余的可能值以及选择进一步地约束一些变量。 搜索则会加一个新的约束来限制这个变量的剩余值（实际上猜测解可能存在于哪里），然后使用传播来确定其他的值是否可能存在于解中。 为了确保完全性，搜索会保留另外一个选择，而它是新约束的否定。 搜索会当有限域求解器发现所有的约束都被满足，此时一个解已经被找到，或者有约束不被满足时停止。 当不可满足出现的时候，搜索必须换另外一个不同的选择集合继续下去。通常有限域求解器使用 深度优先搜索 ，它会撤销最后一个做的选择然后尝试做一个新的选择。

int: n;
array [1..n] of var 1..n: q; % i列的皇后在行q[i]

include "alldifferent.mzn";

constraint alldifferent(q);                       % 不同行
constraint alldifferent([ q[i] + i | i in 1..n]); % 不同对角线
constraint alldifferent([ q[i] - i | i in 1..n]); % 上+下

% 搜索
solve :: int_search(q, first_fail, indomain_min, complete)
      satisfy;
output [ if fix(q[j]) == i then "Q" else "." endif ++
         if j == n then "\n" else "" endif | i,j in 1..n]

有限域问题的一个简单例子是 \(n\) 皇后问题，它要求我们放置 \(n\) 个皇后在 \(n \times n\) 棋盘上使得任何两个都不会互相攻击。变量 q[i] 记录了在 i 列的皇后放置在哪一行上。 alldifferent 约束确保了任何两个皇后都不会在同一行或者对角线上。 Fig. 2.5.1 的左边给出了 n = 9 的典型（部分）搜索树。我们首选设置 q[1] = 1 ， 这样就可以从其他变量的定义域里面移除一些数值，例如 q[2] 不能取值1或者2. 我们接下来设置 q[2] = 3 ，然后进一步地从其他变量的定义域里面移除一些数值。 我们设置 q[3] = 5 （它最早的可能值）。在这三个决策后，棋盘的状态显示为 Fig. 2.5.2 。其中皇后表示已经固定的皇后位置。星星表示此处放置的皇后会攻击到已经放置的皇后，所以我们不能在此处放置皇后。

Fig. 2.5.1 9皇后问题的部分搜索树

Fig. 2.5.2 在加入 q[1] = 1, q[2] = 4, q[3] = 5 的状态

Fig. 2.5.3 在进一步加入 q[6] = 4 后的初始传播

一个搜索策略决定要做哪一个选择。我们目前所做的决定都按照一个简单的策略：选择第一个还没有固定的变量，尝试设置它为它的最小可能值。按照这个策略，下一个决策应该是 q[4] = 7 。变量选择的另外一个策略是选择现在可能值集合 定义域 最小的变量。按照这个所谓 最先失败 变量选择策略，下一个决策应该是 q[6] = 4 。如果我们做了这个决策，则初始的传播会去除掉 Fig. 2.5.3 中显示的额外的值。 但是它使得 q[8] 只剩余有一个值。所以 q[8] = 7 被执行。但是这又使得 q[7] 和 q[9] 也只剩余一个值2。因此这个时候有个约束一定会被违反。我们检测到了不满足性，求解器必须回溯取消最后一个决策 q[6] = 4 并且加入它的否定 q[6] != 4 （引导我们到了 Fig. 2.5.1 中树的状态(c)），即强制使 q[6] = 8 。这使得有些值从定义域中被去除。我们接下来继续重新启用搜索策略来决定该怎么做。

很多有限域搜索被定义为这种方式：选择一个变量来进一步约束，然后选择如何进一步地约束它。

2.5.2. 搜索注解¶

MiniZinc中的搜索注解注明了为了找到一个问题的解应如何去搜索。 注解附在求解项，在关键字 solve 之后。 搜索注解

solve :: int_search(q, first_fail, indomain_min, complete)
      satisfy;

出现在求解项中。注解使用连接符 :: 附为模型的一部分。 这个搜索注解意思是我们应该按照从整型变量数组 q 中选择拥有最小现行定义域的变量（这个是 first_fail 规则），然后尝试设置其为它的最小可能值（ indomain_min 值选择），纵观整个搜索树来搜索（ complete 搜索）。

利用搜索构造注解，我们可以创建更加复杂的搜索策略。目前我们只有一个这样的注解。

seq_search([ <搜素注解>, ..., <搜素注解> ])

顺序搜索构造首先执行对列表中的第一个注解所指定的变量的搜索，当这个注解中的所有的变量都固定后，它执行第二个搜索注解，等等。直到所有的搜索注解都完成。

我们来看一下 Listing 2.3.8 中给出的车间作业调度模型。我们可以替换求解项为

solve :: seq_search([
             int_search(s, smallest, indomain_min, complete),
             int_search([end], input_order, indomain_min, complete)])
      minimize end

通过选择可以最早开始的作业并设置其为 s ，起始时间被设置为 s 。 当所有的起始时间都设置完后，终止时间 end 或许还没有固定。因此我们设置其为它的最小可能取值。

2.5.3. 注解¶

在MiniZinc中，注解是第一类对象。我们可以在模型中声明新的注解，以及声明和赋值给注解变量。

ann : <标识符>;
ann : <标识符> = <注解表达式> ;

annotation <注解名> ( <参数定义>, ..., <参数定义> ) ;

annotation bitdomain(int:nwords);

include "alldifferent.mzn";

int: n;
array [1..n] of var 1..n: q :: bitdomain(n div 32);

constraint alldifferent(q) :: domain;                      
constraint alldifferent([ q[i] + i | i in 1..n]) :: domain;
constraint alldifferent([ q[i] - i | i in 1..n]) :: domain;

ann: search_ann;

solve :: search_ann satisfy;

output [ if fix(q[j]) == i then "Q" else "." endif ++
         if j == n then "\n" else "" endif | i,j in 1..n]

Listing 2.5.2 中的程序阐述了注解声明，注解和注解变量的使用。 我们声明一个新的注解 bitdomain ，意思是来告诉求解器变量定义域应该通过大小为 nwords 的比特数组来表示。 注解附注在变量 q 的声明之后。每一个 alldifferent 约束都被注解为内部注解 domain ，而它指导求解器去使用 alldifferent 的定义域传播版本（如果有的话）。一个注解变量 search_ann 被声明和使用来定义搜索策略。我们可以在一个单独的数据文件中来给出搜素策略的值。

搜索注解的例子或许有以下几种（我们假设每一行都在一个单独的数据文件中）

search_ann = int_search(q, input_order, indomain_min, complete);
search_ann = int_search(q, input_order, indomain_median, complete);
search_ann = int_search(q, first_fail, indomain_min, complete);
search_ann = int_search(q, first_fail, indomain_median, complete);

第一个只是按顺序来选择皇后然后设置其为最小值。第二个按顺序来选择皇后，但是设置中间值给它。第三个选择定义域大小最小的皇后，然后设置最小值给它。最后一个策略选择定义域大小最小的皇后，设置中间值给它。

不同的搜索策略对于能多容易找到解有显著的差异。下面的表格给出了一个简单的关于使用4种不同的搜索策略找到n皇后问题的第一个解所要做的决策个数（其中—表示超过100,000个决策）。很明显地看到，合适的搜索策略会产生显著的提高。