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