this repo has no description
dekker.one
1/*
2% FlatZinc built-in redefinitions for linear solvers.
3%
4% AUTHORS
5% Sebastian Brand
6% Gleb Belov
7*/
8
9%-----------------------------------------------------------------------------%
10%
11% Logic operations
12% Use indicators for reifs (CPLEX)? Seems weak.
13%
14%-----------------------------------------------------------------------------%
15
16predicate bool_not(var bool: p, var bool: q) =
17 bool2int(p) + bool2int(q) = 1;
18
19predicate bool_and(var bool: p, var bool: q, var bool: r) =
20% my_trace(" bool_and: \(p) /\\ \(q) <-> \(r) \n") /\
21 if false then
22 int_lin_le_reif__IND( [-1, -1], [p, q], -2, r)
23 else
24 array_bool_and( [p, q], r )
25% bool_and__INT(bool2int(p), bool2int(q), bool2int(r))
26 endif;
27
28predicate bool_and__INT(var int: x, var int: y, var int: z) =
29 x + y <= z + 1 /\
30 %% x + y >= z * 2; % weak
31 x >= z /\ y >= z; % strong
32
33
34predicate bool_or(var bool: p, var bool: q, var bool: r) =
35 if false then
36 int_lin_le_reif__IND( [-1, -1], [p, q], -1, r)
37 elseif true then
38 array_bool_or( [p, q], r )
39 else
40 let { var int: x = bool2int(p),
41 var int: y = bool2int(q),
42 var int: z = bool2int(r) }
43 in
44 x + y >= z /\
45 % x + y <= z * 2; % weak
46 x <= z /\ y <= z % strong
47 endif;
48
49predicate bool_xor(var bool: p, var bool: q) =
50 1==p+q;
51
52predicate bool_xor(var bool: p, var bool: q, var bool: r) =
53 if false then
54% int_lin_eq_reif__IND( [1, 1], [p, q], 1, r) /\
55 true
56 else
57 let { var int: x = bool2int(p),
58 var int: y = bool2int(q),
59 var int: z = bool2int(r) }
60 in
61 x <= y + z /\
62 y <= x + z /\
63 z <= x + y /\
64 x + y + z <= 2
65 endif;
66
67
68predicate bool_eq_reif(var bool: p, var bool: q, var bool: r) =
69%% trace(" bool_eq_reif: \(p), \(q), \(r) \n") /\
70 if is_fixed(r) then % frequent case
71 if fix(r) = true then p = q else bool_not(p,q) endif
72 elseif is_fixed(q) then
73 if fix(q) = true then p = r
74 else bool_not(p,r) endif
75 elseif is_fixed(p) then
76 if fix(p) = true then q = r
77 else bool_not(q,r) endif
78 elseif false then
79% int_lin_eq_reif__IND( [1, -1], [p, q], 0, r) /\
80 true
81 else
82 let { var int: x = bool2int(p),
83 var int: y = bool2int(q),
84 var int: z = bool2int(r) }
85 in
86 x + y <= z + 1 /\
87 x + z <= y + 1 /\
88 y + z <= x + 1 /\
89 x + y + z >= 1
90 endif;
91
92
93predicate bool_ne_reif(var bool: p, var bool: q, var bool: r) =
94 bool_xor(p, q, r);
95
96
97predicate bool_le(var bool: p, var bool: q) =
98 let { var int: x = bool2int(p),
99 var int: y = bool2int(q) }
100 in
101 x <= y;
102
103
104predicate bool_le_reif(var bool: p, var bool: q, var bool: r) =
105 if false then
106% int_lin_le_reif__IND( [1, -1], [p, q], 0, r) /\
107 true
108 else
109 let { var int: x = bool2int(p),
110 var int: y = bool2int(q),
111 var int: z = bool2int(r) }
112 in
113 1 - x + y >= z /\
114 %% /\ 1 - x + y <= z * 2 not needed
115 1 - x <= z /\ y <= z % strong
116 endif;
117
118
119predicate bool_lt(var bool: p, var bool: q) =
120 not p /\ q;
121
122
123predicate bool_lt_reif(var bool: p, var bool: q, var bool: r) =
124 (not p /\ q) <-> r;
125
126%-----------------------------------------------------------------------------%
127
128%% Reified disjunction
129predicate array_bool_or(array[int] of var bool: a, var bool: b) =
130 if exists( i in index_set( a ) )( is_fixed(a[i]) /\ fix(a[i]) ) then
131 b
132 elseif is_fixed(b) then % frequent case
133 if fix(b) = true then
134 sum(i in index_set(a))( bool2int(a[i]) ) >= 1 %% >=1 seems better for MIPDomains... 5.4.19
135 else
136 forall(i in index_set(a))( not a[i] )
137 endif
138 else
139 let { var int: x = bool2int(b),
140 array[1..length(a)] of var int: c =
141 [ bool2int(a[i]) | i in index_set(a) ] }
142 in
143 sum(c) >= x /\
144 % sum(c) <= x * length(a) % weak
145 forall (i in index_set(a)) (x >= c[i]) % strong
146 endif;
147
148%% Reified conjunction
149predicate array_bool_and(array[int] of var bool: a, var bool: b) =
150 if exists( i in index_set( a ) )( is_fixed(a[i]) /\ not fix(a[i]) ) then
151 not b
152 elseif is_fixed(b) then % frequent case
153 if fix(b) = false then
154 sum(i in index_set(a))( bool2int(a[i]) ) <= length(a)-1
155 else
156 forall(i in index_set(a))( a[i] )
157 endif
158 else
159 let { var int: x = bool2int(b),
160 array[1..length(a)] of var int: c =
161 [ bool2int(a[i]) | i in index_set(a) ] }
162 in
163 length(a) - sum(c) >= 1 - x /\
164 % length(a) - sum(c) <= (1 - x) * length(a); % weak
165 forall (i in index_set(a)) (x <= c[i]) % strong
166 endif;
167
168% predicate array_bool_xor(array[int] of var bool: a) = .. sum(a) is odd ..
169predicate array_bool_xor(array[int] of var bool: a) =
170 let { var 0..(length(a)-1) div 2: m,
171 var 1..((length(a)-1) div 2)*2+1: ss = sum(i in index_set(a))( bool2int(a[i]) ) }
172 in
173 ss == 1 + 2 * m;
174
175predicate bool_clause(array[int] of var bool: p, array[int] of var bool: n) =
176 sum(i in index_set(p))( bool2int(p[i]) )
177 - sum(i in index_set(n))( bool2int(n[i]) )
178 + length(n)
179 >= 1;
180
181predicate bool_lin_eq(array[int] of int: c, array[int] of var bool: x, var int: d) :: promise_total =
182 sum(i in index_set(x))( c[i]*bool2int(x[i]) ) == d;
183
184predicate bool_lin_eq_reif(array[int] of int: c, array[int] of var bool: x,
185 int: d, var bool: b) = %% No var int d, sorry
186 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*bool2int(x[i]) ), d, bool2int(b));
187
188