dekker.one
Jip Dekker's PhD Thesis
1%************************************************
2\chapter{Reasoning about Reification}\label{ch:half-reif}
3%************************************************
4
5\glsreset{half-reif}
6\glsreset{half-reified}
7\glsreset{reif}
8\glsreset{reified}
9
10\input{chapters/4_half_reif_preamble}
11
12\section{An Introduction to Half-Reification}
13\label{sec:half-intro}
14
15The complex expression language used in \cmls{}, such as \minizinc{}, often requires the use of \gls{reif} in order to arrive at a \gls{slv-mod}.
16If the Boolean expression \mzninline{pred(@...@)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
17We call \mzninline{b} the \gls{cvar} of the expression.
18The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(@...@,b)}, which binds the \variable{} to be the truth-value of the expression (i.e., \mzninline{b <-> pred(@...@)}).
19
20\textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses.
21
22\begin{itemize}
23 \item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \gls{rel-sem}.
24 \item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce.
25\end{itemize}
26
27As an alternative, the authors introduce \gls{half-reif}.
28It follows from the idea that in many cases it is \gls{eqsat} to use the logical implication of an expression, \mzninline{b -> pred(@...@)}, instead of the logical equivalence, \mzninline{b <-> pred(@...@)}.
29\Gls{rewriting} with \gls{half-reif} is an approach that improves upon these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
30
31\begin{itemize}
32 \item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls.
33 \item \Glspl{propagator} for \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its non-\gls{reified} \constraint{}.
34\end{itemize}
35
36Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more complex than the \gls{decomp} of a \gls{half-reif}.
37We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
38
39A Boolean expression \(e\) can be \gls{half-reified} when every \gls{sol} to the \instance{} in which it is located is also a \gls{sol} for the \instance{} in which \(e\) is replaced by \true{}.
40This requirement follows from the difference between implication and logical equivalence.
41When the left-hand side of an implication \(b \implies{} e\) is \false{}, it does not influence the value on the right-hand side.
42Therefore, it can be used in these cases as it is guaranteed that if \(e\) represented by a new Boolean \variable{} \(b\), then it is never implied that \(b = \false\).
43Note that when the right-hand side of an implication \(b \implies{} e\) is \true{}, it also does not influence the left-hand side.
44A possible downside of \gls{half-reif} is thus that its \gls{cvar} might need to be assigned by a \gls{search-decision}.
45
46\pagebreak{}
47\begin{example}
48\label{ex:hr-disjunction}
49
50 For example, \gls{half-reif} can be used in the following disjunction.
51
52 \begin{mzn}
53 constraint (x = 5) \/ (y = 5);
54 \end{mzn}
55
56 This \constraint{} states that, between \mzninline{x} and \mzninline{y}, at least one \variable{} takes the value five.
57 The usual \gls{rewriting} would result in the following (intermediate) model, using \glspl{reif} for the equalities.
58
59 \begin{mzn}
60 var bool: b1;
61 var bool: b2;
62 constraint b1 <-> (x = 5);
63 constraint b2 <-> (y = 5);
64 constraint b1 \/ b2;
65 \end{mzn}
66
67 However, independent of the value of \mzninline{x = 5}, if \mzninline{y = 5} takes the value \true{}, then it can never make the disjunction \false{}.
68 Therefore, all \glspl{sol} are still \glspl{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}.
69 Consequently, this means using \gls{half-reif} is \gls{eqsat}.
70 \Gls{rewriting} using \gls{half-reif} will result in the following model.
71
72 \begin{mzn}
73 var bool: b1;
74 var bool: b2;
75 constraint b1 -> (x = 5);
76 constraint b2 -> (y = 5);
77 constraint b1 \/ b2;
78 \end{mzn}
79 \codeendsexample{}
80\end{example}
81
82This property can be extended to include non-Boolean expressions.
83Since Boolean expressions in \minizinc{} can be used in, for example, integer expressions, we can apply similar reasoning to these types of expressions.
84
85\begin{example}
86 For example, the left-hand side of the following \constraint{} is an integer expression that contains the Boolean expression \mzninline{x = 5}.
87
88 \begin{mzn}
89 constraint count(x in arr)(x = 5) > 5;
90 \end{mzn}
91
92 Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}.
93 This means that all \glspl{sol} will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}.
94 Similar to \cref{ex:hr-disjunction}, the \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for the \mzninline{x = 5} expressions.
95\end{example}
96
97To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the monotonicity of \constraints{} w.r.t.\@ an expression.
98A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \gls{monotone} w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\).
99The relation is said to be \gls{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
100For clarification, here we assume that \( \false{} < \true{} \).
101
102Using these definitions, we introduce additional distinctions in the context of expressions.
103Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
104Now, we will categorize the latter into the following three contexts.
105
106\begin{description}
107
108 \item[\posc{}] An expression is in \posc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} w.r.t.\@ the expression.
109
110 \item[\negc{}] An expression is in \negc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} w.r.t.\@ the expression.
111
112 \item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{neither} monotone nor antitone w.r.t.\@ the expression.
113
114\end{description}
115
116Determining the monotonicity of a \constraint{} w.r.t.\@ an expression is a hard problem.
117An expression can be monotone or antitone only through complex interactions, possibly through unknown \gls{native} \constraints{}.
118Therefore, for our analysis, we approximate these definitions.
119We say an expression is in \mixc{} context when it cannot be determined syntactically whether the enclosing \constraint{} is monotone or antitone w.r.t.\@ the expression.
120
121Expressions in \posc{} context are the ones we discussed before.
122Any solution to an \instance{} is still a \gls{sol} when a Boolean expression in a \posc{} is replaced by \true{}.
123As such, \gls{half-reif} can be used for expressions in \posc{} context.
124Although expressions in a \negc{} context cannot be directly \gls{half-reified}, the negation of an expression in a \negc{} context can be \gls{half-reified}.
125
126\begin{example}
127 Consider, for example, the following \constraint{}.
128
129 \begin{mzn}
130 constraint b \/ not (x = 5);
131 \end{mzn}
132
133 The expression \mzninline{x = 5} is in a \negc{} context.
134 Although a \gls{half-reif} cannot be used directly, in some cases the \solver{} can negate the expression which then also negates the context to \posc{}.
135 Our example can be transformed into the following \constraint{}.
136
137 \begin{mzn}
138 constraint b \/ x != 5;
139 \end{mzn}
140
141 The transformed expression, \mzninline{x != 5}, is now in a \posc{} context.
142 We can also speak of this process as ``pushing the negation inwards''.
143\end{example}
144
145Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible.
146Only full \gls{reif} can be used for expressions that are in this context.
147
148\begin{example}
149 An example of a \constraint{} that introduces \mixc{} contexts is the following.
150
151 \begin{mzn}
152 constraint (x = 5) xor (y = 5);
153 \end{mzn}
154
155 This \constraint{} states either \mzninline{x} or \mzninline{y}, but not both, must take the value five.
156 The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on whether \mzninline{x} has already taken the value five, and vice versa.
157 Neither when \mzninline{x = 5} nor \mzninline{y = 5} is replaced by \true{} will all \glspl{sol} to the \instance{} remain \glspl{sol}.
158 This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{}.
159\end{example}
160
161
162\section{Propagation and Half-Reification}%
163\label{sec:half-propagation}
164
165Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform:
166
167\begin{enumerate}
168 \item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the \constraint{} to be \gls{violated}),
169 \item \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}, and
170 \item check whether the \constraint{} is \(entailed\) (i.e., proven to be \gls{satisfied}).
171\end{enumerate}
172
173When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these tasks.
174The \gls{half-reified} \gls{propagator} has a \gls{cvar} \(b\), as an additional argument.
175The \gls{cvar} can be in three states, it can currently not have been assigned a value, it can be assigned \true{}, or it can be assigned \false{}.
176Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows pseudocode for the \gls{propagation} of the \gls{half-reif} of the \constraint{}.
177
178\begin{algorithm}[t]
179
180 \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\).}
181 \KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns to the \solver{} whether the \gls{half-reif} of \(c\) is \gls{violated}, and whether it is entailed.}
182
183 \BlankLine{}
184 \If{\(b \text{ is unassigned}\)}{
185 \If{\(\neg{}check()\)}{
186 \(b \longleftarrow \false{}\)\;
187 \Return{} \(\false{},~\true{}\)\;
188 }
189 }
190 \If{\(\texttt{b} = \true{}\)}{
191 \(prune()\)\;
192 \Return{} \(\neg{} check(),~entailed()\)\;
193 }
194 \Return{} \(\false{},~\false{}\)\;
195 \caption{\label{alg:half-prop} \gls{propagation} pseudocode for the \gls{half-reif} of a \constraint{} \(c\), based on the \gls{propagator} for \(c\).}
196\end{algorithm}
197
198Logically, the creation of \glspl{propagator} for \glspl{half-reif} can always follow this simple principle.
199In practice, however, this is not always possible.
200In some cases, \glspl{propagator} do not explicitly define \(check\), or \(entailed\) as separate steps, but perform them as part of the pruning process.
201When a \gls{domain} is found to be empty, then the \gls{propagator} declares the current state \gls{unsat}.
202It is infeasible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) or \(entailed\) operation.
203Instead, new explicit methods have to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
204
205In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical tasks.
206In addition, we require the \(prune\) task from a \gls{propagator} of \(\neg{} c\).
207Using this additional function, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}. Although this seems reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
208For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that requires that at least two values are equal.
209This is far from a common \constraint{}, and we are not aware of any \solver{} that implements a \gls{propagator} for it.
210
211\begin{algorithm}[t]
212
213 \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \(c\), the function \(pruneNeg\) that prunes the values of the \constraint{} \(\neg{} c\), and a Boolean \gls{cvar} \(b\).
214 }
215 \KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns to the \solver{} whether the \gls{reif} of \(c\) is \gls{violated}, and whether it is entailed.}
216
217 \BlankLine{}
218 \If{\(b \text{ is unassigned}\)}{
219 \If{\(\neg{} check()\)}{
220 \(b \longleftarrow \false{}\)\;
221 }
222 \If{\(entailed()\)}{
223 \(b \longleftarrow \true{}\)\;
224 }
225 }
226 \If{\(\texttt{b} = \true{}\)}{
227 \(prune()\)\;
228 \Return{} \(\neg{} check(),~entailed()\)\;
229 }
230 \If{\(\texttt{b} = \false{}\)}{
231 \(pruneNeg()\)\;
232 \Return{} \(entailed(),~\neg{} check()\)\;
233 }
234 \Return{} \(\false{},~\false{}\)\;
235 \caption{\label{alg:reif-prop} \Gls{propagation} pseudocode for the \gls{reif} of a \constraint{} \(c\), based on the \glspl{propagator} for \(c\) and \(\neg{} c\).}
236\end{algorithm}
237
238\Gls{half-reified} \glspl{propagator} have certain advantages over \gls{reified} \glspl{propagator}, but also may suffer certain penalties.
239\Gls{half-reif} can cause \glspl{propagator} that use their \gls{cvar} to wake up less frequently: \glspl{cvar} that are \gls{fixed} to \true{} by full \gls{reif} will never be \gls{fixed} by \gls{half-reif}.
240This can be advantageous, but has a corresponding disadvantage.
241When a \gls{cvar} is \gls{fixed}, it can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
242
243When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{propagator} to implement it.
244A full \gls{reif} \mzninline{x <-> pred(@...@)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(@...@)}, the \gls{half-reified} \gls{propagator} of its negation, \mzninline{y -> not pred(@...@)}, and the \constraint{} \mzninline{x <-> not y}.
245This does not lose \gls{propagation} strength.
246For Booleans appearing in \posc{} context we can make the \gls{propagator} of the negated \gls{half-reif} run at the lowest priority, since it will never detect if the state is \gls{unsat}.
247Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(@...@)} run at the lowest priority.
248This means that the \glspl{cvar} are still \gls{fixed} at the same time, but there is less overhead.
249
250In \cref{sec:half-experiments} we assess \gls{propagator} implementations for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
251
252\section{Decomposition and Half-Reification}%
253\label{sec:half-decomposition}
254
255The use of \gls{half-reif} does not only offer a benefit when a \gls{propagator} for the \gls{half-reified} \constraint{} is available.
256It can also be beneficial in the \gls{decomp} of \constraints{}.
257Compared to full \gls{reif}, the \gls{decomp} of a \gls{half-reif} does not have to implement the negation of the \constraint{}, and can therefore often be much more compact than the fully \gls{reified} version.
258In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} \solver{}.
259The \glspl{decomp} for these \solver{} technologies often explicitly encode \gls{reified} \constraints{} using two implications.
260If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implications is required.
261
262\begin{example}
263
264 Consider the \gls{reif} of the \constraint{} \mzninline{i <= 4} using the \gls{cvar} \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
265 If the target \solver{} is a \gls{mip} \solver{}, then this \gls{reif} would be linearized.
266 It would take the following form.
267
268 \begin{mzn}
269 constraint i <= 10 - 6 * b; % b -> i <= 4
270 constraint i >= 5 - 5 * b; % not b -> i >= 5
271 \end{mzn}
272
273 Instead, if we could determine that the \constraint{} could be \gls{half-reified}, then the \gls{linearization} could be simplified to only the first \constraint{}.
274\end{example}
275
276The same principle can be applied all throughout the \gls{linearization} process.
277Ultimately, \minizinc{}'s \gls{linearization} library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}.
278For all these \glspl{reif}, replacement by a \gls{half-reif} can remove half of the implications.
279
280For \gls{sat} solvers, a \gls{decomp} for a \gls{half-reif} can be created from its regular \gls{decomp}.
281Any \constraint{} \(c\) will decompose into \gls{cnf} of the following form.
282\[ c = \forall_{i} \exists_{j} lit_{ij} \]
283The \gls{half-reif}, with \gls{cvar} \texttt{b}, could take the following encoding.
284\[ \texttt{b} \implies c = \forall_{i} \neg \texttt{b} \lor \exists_{j} lit_{ij} \]
285The transition from the \gls{cnf} of the regular \constraint{} \(c\) to its \gls{half-reif} \(\texttt{b} \implies{} c\) only adds a single literal to each clause.
286
287It is, however, not as straightforward to construct its full \gls{reif}.
288In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
289Based on the \gls{cnf} of \(c\), this would result in the following logical formula.
290\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
291This formula, however, is not a direct set of clauses.
292Rewriting this formula would result in the following \gls{cnf}.
293\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
294It adds a new binary clause for every literal in the original \gls{cnf}.
295In general, many more clauses are needed to decompose a \gls{reif} compared to a \gls{half-reif}.
296
297According to the principles above, \gls{decomp} libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} \solvers{}.
298In \cref{sec:half-experiments} we assess the effects when \gls{rewriting} with \gls{half-reif}.
299
300\section{Context Analysis}%
301\label{sec:half-context}
302
303The context of an expression cannot always be determined by merely considering \minizinc{} expressions top-down.
304Expressions bound to an identifier can be used multiple times in expressions that influence their context.
305
306\begin{example}
307 Consider the following \minizinc{} fragment.
308
309 \begin{mzn}
310 constraint let {
311 var bool: x = pred(a, b, c);
312 } in y -> x /\ x -> z;
313 \end{mzn}
314
315 The result of predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}.
316 If \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well.
317 As such, the call could then be \gls{half-reified}.
318
319 Although this is the case on the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
320 This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully \gls{reified}.
321\end{example}
322
323Note that an alternative approach for this example would be to replace the identifier with its definition.
324It would then be possible to use \gls{half-reified} versions of both the call and the negation of the call.
325Although this would increase the use of \gls{half-reif}, it should be noted that the \gls{propagation} of these two \glspl{half-reif} would be equivalent to the \gls{propagation} of the full \gls{reif} of the call.
326In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model.
327
328When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
329As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \gls{rel-sem} for partial functions.
330This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes \false{}.
331In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
332The partiality context is the context in which this condition is placed.
333
334\begin{example}
335 We can illustrate the difference between the two contexts in the following \minizinc{} fragment.
336
337 \begin{mzn}
338 var 0..10: x
339 constraint b \/ y div x < 4;
340 \end{mzn}
341
342 In this fragment, we study the context of the division expression \mzninline{y div x}.
343 The expression itself return an integer \variable{}, and it is used on the left-hand side of a less than \constraint{}.
344 This result is therefore in a \negc{} context.
345 This is its value context.
346
347 However, since the \domain{} of \mzninline{x} includes zero, \gls{rewriting} \mzninline{x div y} will introduce the condition under which its result can be used.
348 In this case, the expression \mzninline{x != 0} is added to the right-hand side of the disjunction as follows.
349
350 \begin{mzn}
351 var 0..10: x
352 constraint b \/ ( x != 0 /\ y div x < 4);
353 \end{mzn}
354
355 \noindent{}The partiality context of the division is the context in which this condition is added.
356 Here, the condition is added in a \posc{} context.
357\end{example}
358
359\subsection{Automated analysis}%
360\label{subsec:half-automated}
361
362In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically.
363The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}.
364It requires knowledge about all usages of each \variable{} at the same time.
365This information is not available during the interpretation of \microzinc{}.
366Without loss of generality we can define the context analysis for \microzinc{} models.
367This has the advantage that \microzinc{} does not contain \gls{partial} function calls.
368The partiality in \minizinc{} has already been translated using only total functions (see \cref{sec:rew-micronano}).
369The context analysis therefore does not have to keep track of value and partiality contexts separately.
370
371We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules.
372The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}.
373Each rule describes how an expression that is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
374The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\).
375We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
376The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
377
378\begin{figure*}
379 \begin{center}
380 \begin{tabular}{ccc}
381 \(
382 \begin{array}{lcl}
383 \changepos \rootc & = & \posc \\
384 \changepos \posc & = & \posc \\
385 \changepos \negc & = & \negc \\
386 \changepos \mixc & = & \mixc
387 \end{array}
388 \)
389 & ~ &
390 \(
391 \begin{array}{lcl}
392 \changeneg \rootc & = & \negc \\
393 \changeneg \posc & = & \negc \\
394 \changeneg \negc & = & \posc \\
395 \changeneg \mixc & = & \mixc
396 \end{array}
397 \)
398 \end{tabular}
399 \end{center}
400 \caption{\label{fig:half-ctx-trans} Definitions of the \changepos{} and \changeneg{} context transitions.}
401\end{figure*}
402
403\begin{figure*}
404 \centering
405 \begin{prooftree}
406 \hypo{\ctxeval{x}{ctx}}
407 \infer1[(Ident)]{\text{pushCtx}(x, ctx)}
408 \end{prooftree} \\
409 \bigskip
410 \begin{prooftree}
411 \hypo{\ctxeval{ident\texttt{(} e_{1}, \ldots, e_{n} \texttt{)}}{ctx}}
412 \hypo{\text{argCtx}(ident, ctx) = \tuple{ ctx'_{1}, \ldots, ctx'_{n}}}
413 \infer2[(Call)]{\ctxfunc{ident}{ctx},~\ctxeval{e_{1}}{ctx'_{1}},~\ldots,~ \ctxeval{e_{n}}{ctx'_{n}}}
414 \end{prooftree} \\
415 \bigskip
416 \begin{prooftree}
417 \hypo{\ctxeval{x\texttt{[}i\texttt{]}}{ctx}}
418 \infer1[(Access)]{\ctxeval{x}{\changepos{}ctx}}
419 \end{prooftree} \\
420 \bigskip
421 \begin{prooftree}
422 \hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
423 \infer1[(ITE)]{\ctxeval{b}{ctx},~\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
424 \end{prooftree} \\
425 \bigskip
426 \begin{prooftree}
427 \hypo{\ctxeval{\texttt{[}e~\texttt{|}~G\texttt{]}}{ctx}}
428 \infer1[(Compr)]{\ctxeval{e}{ctx}}
429 \end{prooftree} \\
430 \bigskip
431 \begin{prooftree}
432 \hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
433 \infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
434 \end{prooftree}
435 \caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc{} expressions.}
436\end{figure*}
437
438\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from \glspl{let}.
439The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affect other expressions.
440Instead, every context in which the identifier is found is collected and will be processed when evaluating the corresponding declaration.
441Note that the presented inference rules do not have any explicit state object.
442Instead, we introduce the functions ``pushCtx'' and ``collectCtx''.
443These functions track and combine the contexts in which a value is used in an implicit global state.
444
445Most changes in the context of \microzinc{} expressions stem from the (Call) rule.
446A call expression can change the context in which its arguments should be evaluated.
447As an input to the inference process, an ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
448A definition for this function for the \minizinc{} \glspl{operator} can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc{} \gls{operator} syntax instead of \microzinc{} identifiers for brevity and clarity.}
449
450Although a standard definition for the ``argCtx'' function may cover the most common cases, it does not cover user-defined functions.
451To address this issue, we introduce the \glspl{annotation} \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
452When a function argument is annotated with one of these \glspl{annotation}, the context of the argument in a call in context \(ctx\) is transformed with the operation corresponding to the \gls{annotation} (e.g., \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
453If a function argument is not annotated, then the argument is evaluated in \mixc{} context.
454It may be possible to infer these \glspl{annotation} from the function body.
455However, we currently do not provide such analysis and annotate functions by hand.
456
457\begin{example}
458 Consider the following user-defined \minizinc{} implementation of a logical implication.
459 \begin{mzn}
460 predicate impli(
461 var bool: x ::promise_ctx_antitone,
462 var bool: y ::promise_ctx_monotone
463 ) =
464 not x \/ y;
465 \end{mzn}
466 The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} \gls{operator} shown in \cref{alg:arg-ctx}.
467 In terms of context analysis, this function now is equivalent to the \minizinc{} \gls{operator}.
468\end{example}
469
470\begin{algorithm}
471 \KwIn{A \minizinc{} \gls{operator} \(op\) and calling context \(ctx\)}
472
473 \KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
474
475 \Switch{op}{
476 \Case{\mzninline{ not }}{
477 \Return{\tuple{\changeneg{}ctx}}
478 }
479 \Case{\mzninline{ \/}, \mzninline{+ }}{
480 \Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
481 }
482 \Case{\mzninline{ ->}, \mzninline{<}, \mzninline{<= }}{
483 \Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
484 }
485 \Case{\mzninline{ >}, \mzninline{>=}, \mzninline{- }}{
486 \Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
487 }
488 \Case{\mzninline{ <->}, \mzninline{=}, \mzninline{xor}, \mzninline{* }}{
489 \Return{\tuple{\mixc, \mixc}}
490 }
491 \Case{\mzninline{ /\ }}{
492 \Return{\tuple{ctx, ctx}}
493 }
494 \Other{
495 \Return{\tuple{\mixc, \ldots, \mixc}}
496 }
497 }
498 \caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} \glspl{operator}.}
499\end{algorithm}
500
501The context in which the result of a call expression is used must also be considered.
502The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
503This syntax is used to declare that the \compiler{} must introduce a \microzinc{} function variant that rewrites the function call to \(ident\) in the context \(ctx\).
504This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as defined.
505Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function.
506
507\begin{enumerate}
508 \item If a direct definition for \(ctx\) exists, then use this definition.
509
510 \begin{description}
511 \item[\posc] \Glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
512 \item[\negc] Negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
513 \item[\mixc] \Glspl{reif} can be defined as \(ident\)\mzninline{_reif}.
514 \end{description}
515
516 \item If \(ident\) is a \microzinc{} function with an expression body \(E\), then a copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}.
517
518 \item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
519
520 \item Finally, if none of the earlier steps were successful, then the compilation fails.
521 Note that this can only occur when there is no definition for the \gls{reif} of a \constraint{}, i.e., neither a \gls{native} constraint nor a \gls{decomp}.
522\end{enumerate}
523
524The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively.
525Their inner expressions are evaluated in \(\changepos{}ctx\).
526The inner expressions cannot be simply be evaluated in \(ctx\), because it is not yet certain which expression will be chosen.
527This is important for when \(ctx\) is \rootc{}, since we, at compile time, cannot say which expression will hold globally.
528We will revisit this issue in \cref{subsec:half-?root}.
529
530Finally, the (Compr) and (Arr) rules show simple inference rules for \gls{array} construction expressions.
531If such an expression is evaluated in the context \(ctx\), then its members can be evaluated in the same context \(ctx\).
532
533\begin{figure*}
534 \centering
535 \begin{prooftree}
536 \hypo{\ctxeval{\texttt{let \{ }I\texttt{ \} in } e}{ctx}}
537 \infer1[(Let)]{\ctxeval{e}{ctx}, \ctxitem{I} }
538 \end{prooftree} \\
539 \bigskip
540 \begin{prooftree}
541 \hypo{\ctxitem{I \texttt{; constraint } e }}
542 \infer1[(Con)]{\ctxeval{e}{\rootc},~\ctxitem{I}}
543 \end{prooftree} \\
544 \bigskip
545 \begin{prooftree}
546 \hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
547 \hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
548 \infer2[(Assign)]{\ctxeval{e}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
549 \end{prooftree} \\
550 \bigskip
551 \begin{prooftree}
552 \hypo{\ctxitem{I \texttt{; } \texttt{tuple(}\ldots\texttt{):}~x \texttt{ = (} e_{1}, \ldots, e_{n}\texttt{)}}}
553 \hypo{\text{collectCtx}(x) = \tuple{ctx_{1}, \ldots, ctx_{n}}}
554 \infer2[(TupC)]{\ctxeval{e_{1}}{ctx_{1}}, \ldots, \ctxeval{e_{n}}{ctx_{n}}, ~\ctxitem{I}}
555 \end{prooftree} \\
556 \bigskip
557 \begin{prooftree}
558 \hypo{\ctxitem{I \texttt{; (} T_{1}: x_{1}, \ldots, T_{n}: x_{n} \texttt{) = } e }}
559 \infer[no rule]1{\text{collectCtx}(x_{1}) = [ctx^{1}_{1}, \ldots, ctx^{1}_{k}], \ldots, \text{collectCtx}(x_{n}) = [ctx^{n}_{1}, \ldots, ctx^{n}_{l}]}
560 \infer1[(TupD)]{\ctxeval{e}{\tuple{\text{join}\left(\left[ctx^{1}_{1}, \ldots, ctx^{1}_{k}\right]\right), \ldots, \text{join}\left(\left[ctx^{n}_{1}, \ldots, ctx^{n}_{l}\right]\right)}},~\ctxitem{I}}
561 \end{prooftree} \\
562 \bigskip
563 \begin{prooftree}
564 \hypo{\ctxitem{I \texttt{; } T: x}}
565 \infer1[(Decl)]{}
566 \end{prooftree} \\
567 \bigskip
568 \begin{prooftree}
569 \hypo{\ctxitem{\epsilon{}}}
570 \infer1[(Item0)]{}
571 \end{prooftree}
572 \caption{\label{fig:half-analysis-it} Context inference rules for \microzinc{} let-expressions.}
573\end{figure*}
574
575\Cref{fig:half-analysis-it} shows the inference rules for \glspl{let} and their inner items.
576The first rule, (Let), propagates the context in which the expression is evaluated, \(ctx\), directly to the \mzninline{in}-expression.
577Thereafter, the analysis will continue by iterating over its inner items.
578This is described using the syntax \ctxitem{I}.
579Note that the \(ctx\) of the \gls{let} itself, is irrelevant for the analysis of its inner items.
580
581The inference for \constraint{} items is described by the (Con) rule.
582Since all expressions in well-formed \microzinc{} are total, the \constraint{} can be assumed to hold globally.
583Unlike \minizinc{}, the \constraint{} is not dependent on the context of the \gls{let}.
584The \constraint{}'s expression is evaluated in \rootc{} context.
585
586The (Assign) rule reasons about declarations that have a right-hand side.
587The expression that is assigned to the identifier must be evaluated in the combined context of its usages.
588As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
589These contexts are then combined using a ``join'' function.
590This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
591The right-hand expression of the item is then evaluated in the resulting context.
592
593\begin{figure*}
594 \begin{center}
595 \begin{tabular}{r | c c c c}
596 join & \rootc & \posc & \negc & \mixc \\
597 \hline
598 \rootc & \rootc & \rootc & \rootc & \rootc \\
599 \posc & \rootc & \posc & \mixc & \mixc \\
600 \negc & \rootc & \mixc & \negc & \mixc \\
601 \mixc & \rootc & \mixc & \mixc & \mixc \\
602 \end{tabular}
603 \end{center}
604 \caption{\label{fig:half-join} A table showing the result of joining two contexts.}
605\end{figure*}
606
607(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.
608The context of the individual members of tuples is tracked separately.
609This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts.
610
611Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
612The declaration item of a \variable{} does not further affect the context, and does not depend on it.
613It merely triggers the creation of a new \variable{}.
614The (Item0) rule is triggered when the inner items in the let-expression have been depleted.
615
616\subsection{Potentially Root}%
617\label{subsec:half-?root}
618
619In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
620Different from the rules described, when an \gls{array} access or \gls{conditional} expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc{} context as well.
621It is, however, not always safe to do so.
622
623\begin{example}
624\label{ex:half-maybe-root}
625
626 For example, consider the following \microzinc{} fragment.
627
628 \begin{mzn}
629 constraint if b then
630 F(x, y, z)
631 else
632 G(x, y, z)
633 endif;
634 \end{mzn}
635
636 Let us assume that \mzninline{b} is a \parameter{}, but that its value is not known during the compilation from \minizinc{} to \microzinc{}.
637 In this case, we know that only one side of the \gls{conditional} expression will be evaluated, and that call will then globally constrain the \cmodel{}.
638 As such, the \compiler{} can output calls to the \rootc{} variant of the functions.
639 This will enforce the \constraint{} in the most efficient way.
640
641 Things, however, change when the situation gets more complex.
642 Consider the following \microzinc{} fragment.
643
644 \begin{mzn}
645 let {
646 var bool: p = F(x, y, z);
647 var bool: q = G(x, y, z);
648 constraint if b then p else q endif;
649 var bool: ret = bool_or(p, r);
650 } in ret;
651 \end{mzn}
652
653 One side of the \gls{conditional} expression is also used in a disjunction.
654 If \mzninline{b} evaluates to \true{}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \true{} in the disjunction.
655 Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
656 In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls.
657\end{example}
658
659Using the \changepos{} transformation for sub-expressions contexts is safe, but it places a large burden on the \solver{}.
660The solver performs better without using \gls{reif}.
661
662To detect the situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context.
663This context functions as a ``weak'' \rootc{} context.
664If it is joined with any other context, then it acts as \posc{}.
665The extended join operation is shown in \cref{fig:half-maybe-join}.
666Otherwise, it will act as a normal \rootc{} context.
667
668\begin{figure*}
669 \begin{center}
670 \begin{tabular}{r | c c c c c}
671 join & \rootc & \mayberootc & \posc & \negc & \mixc \\
672 \hline
673 \rootc & \rootc & \rootc & \rootc & \rootc & \rootc \\
674 \mayberootc & \rootc & \mayberootc & \posc & \mixc & \mixc \\
675 \posc & \rootc & \posc & \posc & \mixc & \mixc \\
676 \negc & \rootc & \mixc & \mixc & \negc & \mixc \\
677 \mixc & \rootc & \mixc & \mixc & \mixc & \mixc \\
678 \end{tabular}
679 \end{center}
680 \caption{\label{fig:half-maybe-join} A table showing the result of joining two contexts, considering the \mayberootc{} context.}
681\end{figure*}
682
683\begin{figure*}
684 \centering
685 \begin{prooftree}
686 \hypo{\ctxeval{x\texttt{[}i\texttt{]}}{\rootc}}
687 \infer1[(Access-R)]{\ctxeval{x}{\mayberootc}}
688 \end{prooftree} \\
689 \bigskip
690 \begin{prooftree}
691 \hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
692 \infer1[(ITE-R)]{\ctxeval{c}{ctx},~\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
693 \end{prooftree}
694 \caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
695\end{figure*}
696
697\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions.
698Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
699For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
700Therefore, it will output the \posc{} call for the right-hand side of \mzninline{p}, even when \mzninline{b} evaluates to \true{}.
701At compile time, this is the only correct context to use.
702We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}.
703
704\section{Rewriting and Half-Reification}%
705\label{sec:half-rewriting}
706
707During the \gls{rewriting} process the contexts assigned to the different expressions can be used directly to determine if and how an expression has to be \gls{reified}.
708
709\begin{example}
710\label{ex:half-rewriting}
711
712 Consider the \gls{rewriting} of the following \constraint{}.
713
714 \begin{mzn}
715 constraint (y -> f(x)) \/ not x = 5;
716 \end{mzn}
717
718 \noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that can be both \gls{reified} or \gls{half-reified}.
719 For this \constraint{} we can determine the following contexts for its sub-expressions:
720
721 \begin{itemize}
722 \item the disjunction itself is in \rootc{} context,
723 \item \mzninline{y} and \mzninline{x = 5} are in \negc{} context,
724 \item and the rest are in \posc{} context.
725 \end{itemize}
726
727 \Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraints{}.
728
729 \begin{mzn}
730 constraint bool_clause([b1, b2], []); % b1 \/ b2
731 constraint bool_clause_reif([b3], [y], b1); % b1 <-> y -> b3
732 constraint f_reif(x, b3); % b3 <-> f(x)
733 constraint bool_not(b4, b2); % b2 <-> not b4
734 constraint int_eq_reif(x, 5, b4); % b4 <-> x = 5
735 \end{mzn}
736
737 \Gls{rewriting} using \gls{half-reif} can simplify it to the following \gls{native} \constraints{}.
738
739 \begin{mzn}
740 constraint bool_clause([b1, b2], []); % b1 \/ b2
741 constraint bool_clause_imp([b3], [y], b1); % b1 -> (y -> b3)
742 constraint f_imp(x, b3); % b3 -> f(x)
743 constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
744 \end{mzn}
745
746 We are able to replace the two \glspl{reif} and push the negation inwards, transforming the equals \constraint{} into a not equals \constraint{}.
747 Note, however, that the rewriting produced many extra implications.
748 If the Boolean \mzninline{y} was not further constrained in the problem, then we could further reduce it to the following \constraints{}.
749
750 \begin{mzn}
751 constraint bool_clause([y, b2], []); % y \/ b2
752 constraint f_imp(x, y); % y -> f(x)
753 constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
754 \end{mzn}
755\end{example}
756
757As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}.
758This happens when the right-hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
759Instead, we could have used the left-hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
760In the next section, we present a new post-processing method we call \gls{chain-compression}.
761It can be used to eliminate these \glspl{implication-chain}.
762
763The \gls{rewriting} with \gls{half-reif} also interacts with some simplification methods used during the \gls{rewriting} process.
764Most importantly, \gls{half-reif} has to be considered when using \gls{cse}, and \gls{propagation} can change the context of an expression.
765In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
766Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is evaluated can be adjusted during the \gls{rewriting} process.
767
768\subsection{Chain compression}%
769\label{subsec:half-compress}
770
771\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} does not occur elsewhere.
772In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the \cmodel{}.
773The case shown in the example can be generalized to
774
775\begin{mzn}
776 constraint b1 -> b2 /\ forall(i in N)(b2 -> c[i])
777\end{mzn}
778
779\noindent{}which, if \texttt{b2} does not occur elsewhere in the \instance{}, can be resolved to
780
781\begin{mzn}
782 constraint forall(i in N)(b1 -> c[i])
783\end{mzn}
784
785\noindent{}after which \texttt{b2} can be removed from the model.
786
787An algorithm to remove these chains of implications is best comprehended through the use of an implication graph.
788An implication graph \(\tuple{V,E}\) is a directed graph.
789The vertices \(V\) represent the \variables{} in the \instance{}.
790An edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
791Additionally, the algorithm requires vertices to be marked when their corresponding \variables{} are used in other \constraints{} in the \cmodel{}.
792The goal of the algorithm is now to identify and remove vertices that are not marked and have only one incoming edge.
793\Cref{alg:half-compression} provides a formal specification of the \gls{chain-compression} method in pseudocode.
794
795\begin{algorithm}
796 \KwIn{An implication \constraint{} graph \(G=\tuple{V, E}\) and a set \(M
797 \subseteq{} V\) of vertices used in other \constraints{}.}
798
799 \KwOut{An \gls{eqsat} graph \(G'=\tuple{V', E'}\) where chained
800 implications have been removed.}
801
802 \(V' \longleftarrow V\)\;
803 \(E' \longleftarrow E\)\;
804 \For{\( x \in V \backslash{} M \)} {
805 \Switch{\( \left\{ a~|~(a,x) \in E \right\} \)}{
806 \Case{\( \left\{ a \right \} \)}{
807 \For{\((x, b) \in E\)}{
808 \(E' \longleftarrow E' \cup \{ (a,b) \} \)\;
809 \(E' \longleftarrow E' \backslash \{ (x,b) \} \)\;
810 }
811 \(E' \longleftarrow E' \backslash \{ (a,x) \} \)\;
812 \(V' \longleftarrow V' \backslash \{ x \} \)\;
813 }
814 }
815 }
816 \(G' \longleftarrow \tuple{V', E'}\)\;
817 \caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm.}
818\end{algorithm}
819
820The algorithm can be further improved by considering implied conjunctions.
821These can be split up into multiple implications.
822
823\begin{mzn}
824 constraint b -> forall(x in N)(x)
825\end{mzn}
826
827\noindent{}The expression above is logically equivalent to the following expression.
828
829\begin{mzn}
830 constraint forall(x in N)(b -> x)
831\end{mzn}
832
833Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of \glspl{implication-chain}.
834It should be noted that, although this transformation can increase the number of \constraints{} in the \gls{slv-mod}, it generally increases the \gls{propagation} efficiency.
835
836To adjust the algorithm to simplify implied conjunctions, more introspection from the \minizinc{} \compiler{} is required.
837The \compiler{} must be able to tell if a \variable{} is (only) a \gls{cvar} of a reified conjunction and what the elements of that conjunction are.
838In the case where a \variable{} has one incoming edge, but it is marked as used in another \constraint{}, we can now check if it is only a \gls{cvar} for a \gls{reified} conjunction and perform the transformation in this case.
839
840\subsection{Common Sub-expression Elimination}%
841\label{subsec:half-cse}
842
843When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
844This ensures that if the same expression is \gls{reified} twice, then the resulting \gls{cvar} will be reused.
845This avoids that the solver has to enforce the same functional relation twice.
846
847If the \gls{rewriting} uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
848For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{cvar} of the first \gls{half-reif} cannot be used for the second expression.
849In general the following rules apply.
850
851\begin{itemize}
852
853 \item The result of \gls{rewriting} an expression in \posc{} context, a \gls{half-reif}, can only be reused if the same expression is again found in \posc{} context.
854
855 \item The result of \gls{rewriting} an expression in \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
856
857 \item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context.
858 Since we assume that the result of \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{cvar} does need to be negated when used in \negc{}.
859
860 \item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \true{} (or \false{} in \negc{} context).
861
862\end{itemize}
863
864When considering these compatibility rules, the result of \gls{rewriting} is highly dependent on the order in which expressions are seen.
865It would always be better to encounter the expression in a context that results in a reusable expression, e.g., \mixc{}, before seeing the same expression in another context, e.g., \posc{}.
866This avoids creating both a full \gls{reif} and a \gls{half-reif} of the same expression.
867
868In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the result of their joint context.
869The context recorded in the \gls{cse} table and the found context are joined using the join \gls{operator}, as described in \cref{fig:half-join}.
870If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
871All usages of the previously recorded \gls{cvar} are replaced by the new result.
872The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
873This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed.
874
875\begin{example}
876
877 Consider, for example, the following \minizinc{} fragment, which uses the linearization of \mzninline{int_le}.
878
879 \begin{mzn}
880 predicate int_le_imp(var int: x, int: y, var bool: b) =
881 x <= ub(x) - (ub(x) - y) * b;
882
883 predicate int_le_reif(var int: x, int: y, var bool: b) =
884 x <= ub(x) - (ub(x) - y) * b /\ x >= (y + 1) - (y + 1) * b;
885
886 var 1..10: i;
887 constraint j \/ int_le(i, 4);
888 constraint k xor int_le(i, 4);
889 \end{mzn}
890
891 In this fragment the call \mzninline{int_le(i, 4)} occurs both in \posc{} and \mixc{} context.
892 Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions can result from function \gls{rewriting} were this is not possible.
893 After \gls{rewriting} the first \constraint{}, the \nanozinc{} program would contain the following definitions.
894
895 \begin{nzn}
896 var bool: b1;
897 ↳ constraint int_lin_le([1, 6], [i, b1], 10);
898 constraint bool_clause([j, b1], []);
899 \end{nzn}
900
901 In this program \mzninline{b1} is the \gls{cvar} of the \gls{half-reif} of the \mzninline{int_le(i, 4)} call.
902 The \gls{cvar} is added to the \gls{cse} table as the result of the call.
903 However, since the second call is in \mixc{} context, it cannot use the \gls{half-reif}, and must create the \gls{reif} instead.
904 This results in the following \nanozinc{} program.
905
906 \begin{nzn}
907 var bool: b1;
908 ↳ constraint int_lin_le([1, 6], [i, b1], 10);
909 constraint bool_clause([j, b1], []);
910 var bool: b2;
911 ↳ constraint int_lin_le([1, 6], [i, b2], 10);
912 ↳ constraint int_lin_le([-1, -5], [i, b2], -5);
913 constraint bool_not(k, b2);
914 \end{nzn}
915
916 Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context.
917 As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}.
918 Once all usage of the \gls{cvar} has been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program.
919
920 \begin{nzn}
921 constraint bool_clause([j, b2], []);
922 var bool: b2;
923 ↳ constraint int_lin_le([1, 6], [i, b2], 10);
924 ↳ constraint int_lin_le([-1, -5], [i, b2], -5);
925 constraint bool_not(k, b2);
926 \end{nzn}
927 \codeendsexample{}
928\end{example}
929
930Since the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
931This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
932In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.
933If it is found that for an expression that is about to be \gls{half-reified} there already exists a \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context.
934The expression is \gls{reified} and replaces the existing \gls{half-reified} expression.
935
936\begin{example}
937 Consider for example the \mzninline{=} \gls{operator} on integers, which \microzinc{} represents as an \mzninline{int_eq} call.
938 When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} \gls{operator}, a \mzninline{int_ne} call.
939 The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} \gls{operator}.
940 So to ensure that a \negc{} occurrence of \mzninline{int_eq} and a \posc{} occurrence of \mzninline{int_ne} use the same \gls{cvar} they are both mapped to \mzninline{int_eq} in the \gls{cse} table.
941 The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for an \mzninline{int_ne} call.
942\end{example}
943
944This canonical form for expressions and their negations can also be used for the expressions in other contexts.
945Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation.
946Instead, when one is created, the negation of its \gls{cvar} can directly be used as the \gls{reif} of its negation.
947Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
948Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsat}.
949
950\subsection{Dynamic Context Switching}%
951\label{subsec:half-dyn-context}
952
953In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing \microzinc{}.
954The context may depend on data that is only known at an \instance{} level.
955The same situation can be caused by \gls{propagation}.
956
957\begin{example}
958 Consider the following \minizinc{} fragment
959
960 \begin{mzn}
961 var 1..4: x;
962 var 5..10: y;
963 var bool: b = x < y;
964 constraint b -> (2*x = y);
965 \end{mzn}
966
967 Since the values in the \domain{} of \mzninline{x} are strictly smaller than the values in the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value \true{}.
968 This however means that the \constraint{} is equivalent to the following \constraint{}.
969
970 \begin{mzn}
971 constraint 2*x = y;
972 \end{mzn}
973
974 The linear \constraint{} could be evaluated in \rootc{} context, instead of the \posc{} context that is detected by our context analysis.
975\end{example}
976
977The situation shown in the example is the most common change of context.
978If the \gls{cvar} of a \gls{reif} is \gls{fixed}, the context changes to either \rootc{} or a negated \rootc{} context.
979If, on the other hand, the \gls{cvar} of a \gls{half-reif} is \gls{fixed}, then either the context becomes \rootc{} or the \constraint{} is trivially \gls{satisfied}.
980Since direct \constraints{} are strongly preferred over any form of \gls{reif}, it is important to dynamically pick the correct form during the \gls{rewriting} process.
981
982This problem can be solved by the \compiler{}.
983For each \gls{reif} and \gls{half-reif} the \compiler{} introduces a layer of indirection.
984In this layer, it checks the \gls{cvar}.
985If the \gls{cvar} is already \gls{fixed}, then it rewrites itself into the corresponding form in another context.
986Otherwise, it behaves as it would have done normally.
987The \gls{cvar} is thus used to communicate the change in context.
988
989\begin{example}
990 Let's assume the \compiler{} finds a call to \mzninline{int_eq} in \posc{} context.
991 Instead of outputting the call to \mzninline{int_eq_imp} directly, it will instead output a call to \mzninline{int_eq_imp_check}.
992 This predicate is then generated as shown in \cref{lst:half-check-reif}.
993 The \gls{rewriting} of the calls to the generated predicate then follow the normal process.
994\end{example}
995\begin{listing}
996 \mznfile{assets/listing/half_reif_check.mzn}
997 \caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_eq_imp} that checks the \gls{cvar} to ensure a \gls{half-reif} is still required.}
998\end{listing}
999
1000
1001\section{Experiments}
1002\label{sec:half-experiments}
1003
1004We now present an experimental evaluation of the presented techniques.
1005First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{}, we compare their performance against their \glspl{decomp}.
1006We recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
1007We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}.
1008
1009Additionally, we assess the effects of detecting and introducing \glspl{half-reif} during the \gls{rewriting} process.
1010We rewrite and solve 200 \minizinc{} \instances{} for several \solvers{} with and without the use of \gls{half-reif}.
1011We then analyse the trends in the generated \glspl{slv-mod} and their solving performance.
1012
1013A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
1014
1015\subsection{Half-Reified Propagators}
1016\label{sec:half-exp-prop}
1017
1018Our first experiment considers the QCP-max quasi-group completion problem.
1019In this problem, we need to decide the value of a \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}.
1020The aim of the problem is to create as many rows and columns as possible where all \variables{} take a unique value.
1021In each \instance{} certain values have already been \gls{fixed}.
1022It is not always possible for all rows and columns to contain only distinct values.
1023
1024In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}.
1025Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are in \posc{} context and can be \gls{half-reified}.
1026
1027\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
1028The results are grouped based on their size of the instance.
1029For each group we show the number of instances solved by the configuration and the average time used for this process.
1030
1031In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a \gls{propagator}.
1032This \gls{propagator} is an adjusted version from the existing \gls{boundsz-con} \mzninline{all_different} \gls{propagator} in \gls{chuffed}.
1033The implementation of the \gls{propagator} was already split into parts that check the violation of the \constraint{} and parts that prune the \glspl{domain} of the \variables{}.
1034Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
1035Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well.
1036These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \false{}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \true{}.
1037
1038In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
1039The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
1040Their conjunction then represents the \gls{reif} of the \mzninline{all_different} \constraint{}.
1041
1042\begin{listing}
1043 \mznfile{assets/listing/half_alldiff.mzn}
1044 \caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} library.}
1045\end{listing}
1046
1047
1048\begin{table}
1049 \begin{center}
1050 \input{assets/table/half_qcp}
1051
1052 \caption{\label{tab:half-qcp} QCP-max problems: number of solved \instances{} and average time (in seconds) with a 300s timeout.}
1053
1054 \end{center}
1055\end{table}
1056
1057The results in \cref{tab:half-qcp} show that the specialized \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
1058Although it only allows us to solve one extra instance, there is a significant reduction in solving time for most \instances{}.
1059Note that the qcp-15 \instances{} are the only exception.
1060It appears that none of the \instances{} in this group proved to be a real challenge to either method, and we see similar solve times between the two methods.
1061
1062In addition, we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem.
1063In the problem we are given a graph with weighted edges, both positive and negative.
1064The aim of the problem is to find the optimal acyclic path from a given start node that maximizes the weights on the path.
1065It is not required to visit every node.
1066
1067In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly.
1068The \minizinc{} model for this problem contains an \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
1069We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}.
1070The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the \gls{array}.
1071Otherwise, it will set its surrounding context to \false{}.
1072The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \false{} whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
1073Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above.
1074
1075\begin{table}
1076 \begin{center}
1077
1078 \input{assets/table/half_prize}
1079
1080 \caption{\label{tab:half-prize} Prize collecting paths: number of solved \instances{} and average time (in seconds) and with a 300s timeout.}
1081 \end{center}
1082\end{table}
1083
1084The results of the experiment are shown in \cref{tab:half-prize}.
1085Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the \gls{decomp}.
1086The difference in performance becomes more pronounced in the larger \instances{}.
1087In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}.
1088
1089\subsection{Rewriting with Half-Reification}
1090\label{sec:half-exp-rewriting}
1091
1092The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \gls{half-reif} on a larger scale.
1093In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
1094These experiments are conducted using the \gls{gecode} \solver{}, which has \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which have been adapted to use \gls{half-reif} as earlier described.
1095The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable \gls{half-reif}.
1096The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
1097The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}.
1098
1099\begin{table}
1100 \begin{subtable}[b]{\linewidth}
1101 \input{assets/table/half_flat_gecode}
1102 \caption{\label{subtab:half-flat-gecode}\gls{gecode} library}
1103 \end{subtable}
1104 \begin{subtable}[b]{\linewidth}
1105 \input{assets/table/half_flat_linear}
1106 \caption{\label{subtab:half-flat-lin}\Gls{linearization} library}
1107 \end{subtable}
1108 \begin{subtable}[b]{\linewidth}
1109 \input{assets/table/half_flat_sat}
1110 \caption{\label{subtab:half-flat-bool}\Gls{booleanization} library}
1111 \end{subtable}
1112 \caption{\label{tab:half-rewrite} Cumulative statistics of \gls{rewriting} all \minizinc{} \instances{} from \minizinc{} challenge 2019 \& 2020 (200 \instances{}).}
1113\end{table}
1114
1115Grouped by \solver{} library and whether \gls{half-reif} is used, \cref{tab:half-rewrite} shows the following cumulative figures from the \gls{rewriting} process of the \minizinc{} challenge.
1116
1117\begin{itemize}
1118
1119 \item The number of \constraints{} in \flatzinc{}.
1120 \item The number of \glspl{reif} evaluated during the \gls{rewriting} process.
1121 This includes both the \glspl{reif} that are decomposed and the \glspl{reif} that are present in the \flatzinc{}.
1122 \item The number of \glspl{half-reif} evaluated during the \gls{rewriting} process.
1123 \item The number of implications removed using the \gls{chain-compression} method.
1124 \item The runtime of the \gls{rewriting} process.
1125
1126\end{itemize}
1127
1128The \gls{rewriting} statistics for the \gls{gecode} \solver{} library, shown in \cref{subtab:half-flat-gecode}, show significant changes in the resulting \flatzinc{}.
1129Although the total number of \constraints{} remains stable, we see that well over half of all \glspl{reif} are replaced by \glspl{half-reif}.
1130This replacement happens mostly 1-for-1; the difference between the number of \glspl{half-reif} introduced and the number of \glspl{reif} reduced is only 20. In comparison, the number of implications removed by \gls{chain-compression} looks small, but this number is highly dependent on the \minizinc{} model.
1131In many models \gls{chain-compression} does not remove any implications, but in some models an implication is removed for every \gls{half-reif} that is introduced.
1132Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimization techniques is minimal.
1133
1134The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization.
1135Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, \gls{half-reif} is able to remove almost 7.5\% of the overall \constraints{}.
1136The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as with \gls{gecode}.
1137This is caused by the fact that the linearization process requires full \gls{reif} in the decomposition of many \glspl{global}.
1138Similar to \gls{gecode}, the number of implications that is removed is dependent on the problem.
1139Lastly, the \gls{rewriting} time slightly increases for the linearization process.
1140Since there are many more \constraints{}, the introduced optimization mechanisms have a slightly higher overhead.
1141
1142Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} are shown in \cref{subtab:half-flat-bool}.
1143Unlike linearization, \gls{half-reif} does not significantly reduce the number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
1144We also see that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}.
1145Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
1146Even when \gls{rewriting} does not introduce \glspl{half-reif}, they are still introduced by the \glspl{decomp} of other \constraints{}.
1147Furthermore, \gls{chain-compression} does not seem to have any effect.
1148Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into larger clauses.
1149Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
1150The relatively small changes shown indicate that additional work may be warranted in the \gls{booleanization} library.
1151It may be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts.
1152
1153\begin{table}
1154 \input{assets/table/half_mznc}
1155 \caption{\label{tab:half-mznc} Status overview of solving \minizinc{} Challenge 2019 \& 2020 with and without \gls{half-reif}.}
1156\end{table}
1157
1158\Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports
1159
1160\begin{description}
1161 \item[Unsatisfiable] when it proves the \instance{} does not have a \gls{sol},
1162 \item[Optimal solution] when it has found a \gls{sol} and has proven the \gls{sol} to be optimal,
1163 \item[Satisfied] when it has found a \gls{sol} for the problem,
1164 \item[Unknown] when it does not find a \gls{sol} within the time limit, and
1165 \item[Error] when the \solver{} program crashes.
1166\end{description}
1167
1168\noindent{}For \solver{} statuses that end the solving process before the time-out of 15 minutes we also show the average time.
1169
1170The results shown in this table are very mixed.
1171For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance.
1172We would have hoped that \glspl{propagator} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general.
1173However, neither number of \instances{} solved, nor the required solving time improved.
1174A single \instance{}, however, is negatively impacted by the change; for this \instance{} it cannot find an \gls{opt-sol} any longer.
1175We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}.
1176Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.
1177
1178When using \gls{cplex}, \gls{half-reif} clearly has a positive effect.
1179Although it does not prove the unsatisfiability of one instance any longer and slightly increases the number of solver errors, an \gls{opt-sol} is found for five more instances.
1180The same linearized instances when using the \gls{cbc} solver seem to have the opposite effect.
1181Even though it reduces the time required to prove that two instances are \gls{unsat}, it cannot find six \glspl{opt-sol} any longer.
1182These results are hard to explain.
1183In general, we would expect the reduction of \constraints{} in a \gls{mip} instance would help the \gls{mip} solver.
1184However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver.
1185An important technique used by \gls{mip} solvers is to detect certain patterns, such as cliques, during the pre-processing of the \gls{mip} instance.
1186Some patterns can only be detected when using full \gls{reif}.
1187Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given \autocite{lodi-2013-variability,fischetti-2014-erratiscism}.
1188When using \gls{half-reif} in addition to \gls{aggregation} and \gls{del-rew}, the order and form of the \gls{slv-mod} can be exceedingly different.
1189
1190The solving statistics for \gls{openwbo} may be most positive.
1191Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}.
1192It negatively impacts one \instance{}, for which find a \gls{sol} is not found any more.
1193That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change.
1194
1195\section{Summary}
1196\label{sec:half-summary}
1197
1198For some models avoiding \gls{reif} or the usage of \gls{half-reif} instead of \gls{reif} can lead to a significant improvement in solver performance.
1199This chapter presented a framework to reason about \gls{reif} during the \gls{rewriting} process.
1200It provided a \microzinc{} analysis that associates each expression with a certain context.
1201Depending on the context, we then know whether a \constraint{} can remain non-\gls{reified}, can be \gls{half-reified}, or must be \gls{reified}.
1202Notably, the best context cannot always be determined without a complete \gls{parameter-assignment} and \gls{propagation}.
1203We showed how the best context for a \constraint{} can still always be used by introducing an additional check of the \gls{cvar}.
1204Finally, we adapted the simplification techniques used during \gls{rewriting} to the use of \gls{half-reif}.
1205We showed how \gls{cse} can be modified to take the context of an expression into account, and we introduced a new simplification technique, \gls{chain-compression}, to eliminate \glspl{implication-chain} introduced by \gls{half-reif}.
1206
1207To make full use of \gls{half-reif}, we extended \gls{chuffed} with two \glspl{propagator} for \gls{half-reif} \constraints{} that were shown to be effective for certain models.
1208We also extended the \minizinc{} \gls{linearization} and \gls{booleanization} libraries to make use of \gls{half-reif} in their \glspl{decomp}.
1209Although the results for the \gls{mip} \solvers{} were mixed, the results for the \gls{maxsat} \solver{} were very encouraging.
1210
1211Another significant aspect of this thesis is to improve the incremental usage of \constraint{} modelling.
1212The next chapter will present both a method to model \gls{meta-optimization} algorithms directly in \minizinc{}, and a method to extend the \gls{rewriting} architecture with an incremental interface.