this repo has no description
dekker.one
1% 布尔型变量x的总和 = s
2predicate bool_sum_eq(array[int] of var bool:x, int:s) =
3 let { int: c = length(x) } in
4 if s < 0 then false
5 elseif s == 0 then
6 forall(i in 1..c)(x[i] == false)
7 elseif s < c then
8 let { % cp = number of bits required for representing 0..c
9 int: cp = floor(log2(int2float(c))),
10 % z is sum of x in binary
11 array[0..cp] of var bool:z } in
12 binary_sum(x, z) /\
13 % z == s
14 forall(i in 0..cp)(z[i] == ((s div pow(2,i)) mod 2 == 1))
15 elseif s == c then
16 forall(i in 1..c)(x[i] == true)
17 else false endif;
18
19include "binarysum.mzn";