2.7. 在MiniZinc中对布尔可满足性问题建模¶
MiniZinc 可以被用来给布尔可满足性问题建模，这种问题的变量被限制为是布尔型 (bool)。MiniZinc 可以使用有效率的布尔可满足性求解器来有效地解决求得的模型。
2.7.1. 整型建模¶
很多时候，尽管我们想要使用一个布尔可满足性求解器，我们可能也需要给问题的 整数部分建模。 有三种通用的方式使用布尔型变量对定义域为范围 \(0 \dots m\) 内的整型变量 \(I\) 建模，其中 \(m = 2^{k}-1\) 。
二元： \(I\) 被表示为 \(k\) 个二元变量 \(i_0, \ldots, i_{k-1}\) ，其中 \(I = 2^{k-1} i_{k-1} + 2^{k-2} i_{k-2} + \cdots + 2 i_1 + i_0\) 。在MiniZinc 中，这可表示为
array[0..k-1] of var bool: i; var 0..pow(2,k)-1: I = sum(j in 0..k-1)(bool2int(i[j])*pow(2,j));
一元: \(I\) 被表示为 \(m\) 个二元变量 \(i_1, \ldots, i_m\) 且 \(i = \sum_{j=1}^m \mathtt{bool2int}(i_j)\) 。由于在一元表 示中有大量的冗余表示，我们通常要求 \(i_j \rightarrow i_{j-1}, 1 < j \leq m\) 。在MiniZinc中，这可表示为
array[1..m] of var bool: i; constraint forall(j in 2..m)(i[j] -> i[j-1]); var 0..m: I = sum(j in 1..m)(bool2int(i[j]);
值: 其中 \(I\) 被表示为 \(m+1\) 个二元变量 \(i_0, \ldots, i_m\) ，其中 \(i = k \Leftrightarrow i_k\) 并且 \(i_0, \ldots, i_m\) 中最多有一个为真。在MiniZinc中，这可表示为
array[0..m] of var bool: i; constraint sum(j in 0..m)(bool2int(i[j]) == 1; var 0..m: I; constraint foall(j in 0..m)(I == j <-> i[j]);
每种表示都有其优点和缺点。这取决于模型中需要对整数做什么样的操作，而这些 操作在哪一种表示上更为方便。
2.7.2. 非等式建模¶
接下来，让我们考虑如何为一个拉丁方问题建模。一个拉丁方问题是在 \(n \times n\) 个网 格上放置 \(1..n\) 之间的数值使得每个数在每行每列都仅出现一次。图 Listing 2.7.1 中给出了拉丁方问题的的一个整数模型。
int: n; % 拉丁方的大小
array[1..n,1..n] of var 1..n: a;
include "alldifferent.mzn";
constraint forall(i in 1..n)(
alldifferent(j in 1..n)(a[i,j]) /\
alldifferent(j in 1..n)(a[j,i])
);
solve satisfy;
output [ show(a[i,j]) ++ if j == n then "\n" else " " endif |
i in 1..n, j in 1..n ];
整型变量直接的唯一的约束实际上是非等式，而它在约束 alldifferent 中被编码。 数值表示是表达非等式的最佳方式。图 Listing 2.7.2 给出了一个关于拉丁方问题的只含有布尔型 变量的模型。注意每个整型数组元素 a[i,j] 被替换为一个布尔型数组。我们使用谓词 exactlyone 来约束每个数值在每行每列都仅出现一次，也用来约束有且仅有一个布尔型 变量对应于整型数组元素 a[i,j] 为真。
int: n; % 拉丁方的大小
array[1..n,1..n,1..n] of var bool: a;
predicate atmostone(array[int] of var bool:x) =
forall(i,j in index_set(x) where i < j)(
(not x[i] \/ not x[j]));
predicate exactlyone(array[int] of var bool:x) =
atmostone(x) /\ exists(x);
constraint forall(i,j in 1..n)(
exactlyone(k in 1..n)(a[i,j,k]) /\
exactlyone(k in 1..n)(a[i,k,j]) /\
exactlyone(k in 1..n)(a[k,i,j])
);
solve satisfy;
output [ if fix(a[i,j,k]) then
show(k) ++ if j == n then "\n" else " " endif
else "" endif | i,j,k in 1..n ];
2.7.3. 势约束建模¶
让我们来看下如何对点灯游戏建模。这个游戏由一个矩形网格组成，每个网格为空 白或者被填充。每个被填充的方格可能包含1到4之间的数字，或者没有数字。我们的 目标是放置灯泡在空白网格使得
- 每个空白的网格是“被照亮的”，也就是说它可以透过一行没有被打断的空白网格 看到光亮。
- 任何两个灯泡都不能看到彼此。
- 一个有数值的填充的网格相邻的灯泡个数必须等于这个网格中的数值。
Fig. 2.7.1 给出了点灯游戏的一个例子以及 Fig. 2.7.2 给出了它的解。
Fig. 2.7.1 点灯游戏的一个例子展示
Fig. 2.7.2 点灯游戏的完整的解
这个问题很自然地可以使用布尔型变量建模。布尔型变量用来决定哪一个网格包含有一个点灯以及哪一个没有。同时我们也有一些作用于填充的网格上的整数算术运算要 考虑。
int: h; set of int: H = 1..h; % 板高度
int: w; set of int: W = 1..w; % 板宽度
array[H,W] of -1..5: b; % 板
int: E = -1; % 空白格
set of int: N = 0..4; % 填充并含有数字的网格
int: F = 5; % 填充但不含有数字的网格
% 位置 (i1,j1) 对位置 (i2,j2) 可见
test visible(int: i1, int: j1, int: i2, int: j2) =
((i1 == i2) /\ forall(j in min(j1,j2)..max(j1,j2))(b[i1,j] == E))
\/ ((j1 == j2) /\ forall(i in min(i1,i2)..max(i1,i2))(b[i,j1] == E));
array[H,W] of var bool: l; % is there a light
% 填充的网格没有灯泡
constraint forall(i in H, j in W, where b[i,j] != E)(l[i,j] == false);
% lights next to filled numbered square agree
include "boolsum.mzn";
constraint forall(i in H, j in W where b[i,j] in N)(
bool_sum_eq([ l[i1,j1] | i1 in i-1..i+1, j1 in j-1..j+1 where
abs(i1 - i) + abs(j1 - j) == 1 /\
i1 in H /\ j1 in W ], b[i,j]));
% 每个空白网格是被照亮的
constraint forall(i in H, j in W where b[i,j] == E)(
exists(j1 in W where visible(i,j,i,j1))(l[i,j1]) \/
exists(i1 in H where visible(i,j,i1,j))(l[i1,j])
);
% 任何两个灯泡看不到彼此
constraint forall(i1,i2 in H, j1,j2 in W where
(i1 != i2 \/ j1 != j2) /\ b[i1,j1] == E
/\ b[i2,j2] == E /\ visible(i1,j1,i2,j2))(
not l[i1,j1] \/ not l[i2,j2]
);
solve satisfy;
output [ if b[i,j] != E then show(b[i,j])
else if fix(l[i,j]) then "L" else "." endif
endif ++ if j == w then "\n" else " " endif |
i in H, j in W];
图 Listing 2.7.3 中给出了这个问题的一个模型。图 Fig. 2.7.1 中给出的问题的数据文件在图 Listing 2.7.4 中给出。
h = 7;
w = 7;
b = [| -1,-1,-1,-1, 0,-1,-1
| -1,-1,-1,-1,-1,-1,-1
| 0,-1,-1, 3,-1,-1,-1
| -1,-1, 2,-1, 4,-1,-1
| -1,-1,-1, 5,-1,-1, 1
| -1,-1,-1,-1,-1,-1,-1
| 1,-1, 2,-1,-1,-1,-1 |];
模型利用了一个布尔型求和谓词
predicate bool_sum_eq(array[int] of var bool:x, int:s);
使得一个布尔型数组的和等于一个固定的整数。多种方式都能使用布尔型变量给 cardinality 约束建模。
- 加法器网络：我们可以使用包含加法器的一个网络给布尔型总和建立一个二元布 尔型表达式
- 排序网络：我们可以通过使用一个排序网络去分类布尔型数组来创建一个布尔型 总和的一元表达式
- 二元决策图：我们可以创建一个二维决策图（BDD）来编码势约束。
% 布尔型变量x的总和 = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
let { int: c = length(x) } in
if s < 0 then false
elseif s == 0 then
forall(i in 1..c)(x[i] == false)
elseif s < c then
let { % cp = number of bits required for representing 0..c
int: cp = floor(log2(int2float(c))),
% z is sum of x in binary
array[0..cp] of var bool:z } in
binary_sum(x, z) /\
% z == s
forall(i in 0..cp)(z[i] == ((s div pow(2,i)) mod 2 == 1))
elseif s == c then
forall(i in 1..c)(x[i] == true)
else false endif;
include "binarysum.mzn";
% 位 x 的的总和 = 二元表示的 s。
% s[0], s[1], ..., s[k] 其中 2^k >= length(x) > 2^(k-1)
predicate binary_sum(array[int] of var bool:x,
array[int] of var bool:s)=
let { int: l = length(x) } in
if l == 1 then s[0] = x[1]
elseif l == 2 then
s[0] = (x[1] xor x[2]) /\ s[1] = (x[1] /\ x[2])
else let { int: ll = (l div 2),
array[1..ll] of var bool: f = [ x[i] | i in 1..ll ],
array[1..ll] of var bool: t = [x[i]| i in ll+1..2*ll],
var bool: b = if ll*2 == l then false else x[l] endif,
int: cp = floor(log2(int2float(ll))),
array[0..cp] of var bool: fs,
array[0..cp] of var bool: ts } in
binary_sum(f, fs) /\ binary_sum(t, ts) /\
binary_add(fs, ts, b, s)
endif;
% 把两个二元数值 x 和 y 加起来，位 ci 用来表示进位，来得到二元 s
predicate binary_add(array[int] of var bool: x,
array[int] of var bool: y,
var bool: ci,
array[int] of var bool: s) =
let { int:l = length(x),
int:n = length(s), } in
assert(l == length(y),
"length of binary_add input args must be same",
assert(n == l \/ n == l+1, "length of binary_add output " ++
"must be equal or one more than inputs",
let { array[0..l] of var bool: c } in
full_adder(x[0], y[0], ci, s[0], c[0]) /\
forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
if n > l then s[n] = c[l] else c[l] == false endif ));
predicate full_adder(var bool: x, var bool: y, var bool: ci,
var bool: s, var bool: co) =
let { var bool: xy = x xor y } in
s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));
我们可以使用图 Listing 2.7.5 给出的二元加法器网络代码实现 bool_sum_eq 。图 Listing 2.7.6 中定义的 谓词 binary_sum 创建了一个 x 总和的二维表示法。它把列表分为两部分，把每一部分 分别加起来得到它们的一个二元表示，然后用 binary_add 把这两个二元数值加起来。 如果 x 列大小是奇数，则最后一位被保存起来作为二元加法时的进位来使用。
% 布尔型变量 x的总和 = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
let { int: c = length(x) } in
if s < 0 then false
elseif s == 0 then forall(i in 1..c)(x[i] == false)
elseif s < c then
let { % cp = nearest power of 2 >= c
int: cp = pow(2,ceil(log2(int2float(c)))),
array[1..cp] of var bool:y, % y is padded version of x
array[1..cp] of var bool:z } in
forall(i in 1..c)(y[i] == x[i]) /\
forall(i in c+1..cp)(y[i] == false) /\
oesort(y, z) /\ z[s] == true /\ z[s+1] == false
elseif s == c then forall(i in 1..c)(x[i] == true)
else false endif;
include "oesort.mzn";
%% 奇偶排序
%% y是x的有序版本，所有的真都在假之前
predicate oesort(array[int] of var bool:x, array[int] of var bool:y)=
let { int: c = card(index_set(x)) } in
if c == 1 then x[1] == y[1]
elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
else
let {
array[1..c div 2] of var bool:xf = [x[i] | i in 1..c div 2],
array[1..c div 2] of var bool:xl = [x[i] | i in c div 2 +1..c],
array[1..c div 2] of var bool:tf,
array[1..c div 2] of var bool:tl } in
oesort(xf,tf) /\ oesort(xl,tl) /\ oemerge(tf ++ tl, y)
endif;
%% 奇偶合并
%% y 是 x的有序版本，所有的真都在假之前
%% 假设 x的前一半是有序的，后一半也是
predicate oemerge(array[int] of var bool:x, array[int] of var bool:y)=
let { int: c = card(index_set(x)) } in
if c == 1 then x[1] == y[1]
elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
else
let { array[1..c div 2] of var bool:xo =
[ x[i] | i in 1..c where i mod 2 == 1],
array[1..c div 2] of var bool:xe =
[ x[i] | i in 1..c where i mod 2 == 0],
array[1..c div 2] of var bool:to,
array[1..c div 2] of var bool:te } in
oemerge(xo,to) /\ oemerge(xe,te) /\
y[1] = to[1] /\
forall(i in 1..c div 2 -1)(
comparator(te[i],to[i+1],y[2*i],y[2*i+1])) /\
y[c] = te[c div 2]
endif));
% 比较器 o1 = max(i1,i2), o2 = min(i1,i2)
predicate comparator(var bool:i1,var bool:i2,var bool:o1,var bool:o2)=
(o1 = (i1 \/ i2)) /\ (o2 = (i1 /\ i2));
我们可以使用图 Listing 2.7.7 中给出的一元排序网络代码来实现 bool_sum_eq 。势约束通过扩展输入 x 长度为2 的次幂，然后使用奇偶归并排序网络给得到的位排序来实现。奇偶归 并排序工作方式在图 Listing 2.7.8 中给出，它递归地把输入列表拆为两部分，给每一部分排序，然 后再把有序的两部分归并起来。
% the sum of booleans x = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
let { int: c = length(x),
array[1..c] of var bool: y = [x[i] | i in index_set(x)]
} in
rec_bool_sum_eq(y, 1, s);
predicate rec_bool_sum_eq(array[int] of var bool:x, int: f, int:s) =
let { int: c = length(x) } in
if s < 0 then false
elseif s == 0 then
forall(i in f..c)(x[i] == false)
elseif s < c - f + 1 then
(x[f] == true /\ rec_bool_sum_eq(x,f+1,s-1)) \/
(x[f] == false /\ rec_bool_sum_eq(x,f+1,s))
elseif s == c - f + 1 then
forall(i in f..c)(x[i] == true)
else false endif;
我们可以使用图 Listing 2.7.9 中给出的二元决策图代码来实现 bool_sum_eq 。势约束被分为两种情况：或者第一个元素 x[1] 为 true 并且剩下位的总和是 s-1 ，或者 x[1] 为 false 并 且剩下位的总和是 s 。它的效率的提高依赖于去除共同子表达式来避免产生太多的相同的约束。