From e3a864effefec145e65b39e43233cdf668225748 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Sat, 24 Jul 2021 22:17:56 +1000 Subject: [PATCH] Incorporate Guido's feedback on Half-Reification --- assets/listing/half_reif_check.mzn | 11 +- assets/shorthands.tex | 1 + chapters/1_introduction.tex | 4 +- chapters/2_background.tex | 16 +- chapters/4_half_reif.tex | 470 ++++++++++++++++++----------- chapters/4_half_reif_preamble.tex | 13 +- chapters/6_conclusions.tex | 14 +- 7 files changed, 319 insertions(+), 210 deletions(-) diff --git a/assets/listing/half_reif_check.mzn b/assets/listing/half_reif_check.mzn index d676391..7857986 100644 --- a/assets/listing/half_reif_check.mzn +++ b/assets/listing/half_reif_check.mzn @@ -1,15 +1,14 @@ -predicate _int_lin_le_imp( - array[int] of int: c, - array[int] of var int: x, - int: d, +predicate int_eq_imp_check( + var int: x, + var int: y, var bool: b ) = if is_fixed(b) then if fix(b) then - int_lin_le(c, x, d) + int_eq(x, y) else true endif else - int_lin_le_imp(c, x, d, b) + int_eq_imp(x, y, b) endif; diff --git a/assets/shorthands.tex b/assets/shorthands.tex index b895a25..2d795b0 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -4,6 +4,7 @@ % Academic writing \newcommand*{\eg}{e.g.,\xspace} \newcommand*{\ie}{i.e.,\xspace} +\newcommand*{\wrt}{w.r.t.\xspace} % Glossary entries \newcommand*{\Cmls}{\Glspl{cml}} diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index dd03f72..12d9628 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -265,8 +265,8 @@ We compare the performance of an implementation of the presented architecture ag In this chapter, we present a formal analysis technique to reason about \gls{reif}. This analysis can help us decide whether a \constraint{} has to be reified. In addition, the analysis allows us to determine whether we use \gls{half-reif}. -We thus present the first implementation of the usage of automatic \gls{half-reif}. -We conclude this chapter by analysing the impact of the usage of \gls{half-reif} for different types of \solvers{}. +We thus present the first implementation of automatic \gls{half-reif}. +We conclude this chapter by analysing the impact of \gls{half-reif} for different types of \solvers{}. \emph{\Cref{ch:incremental}} focuses on the development of incremental methods for \cmls{}. We first present a novel technique that eliminates the need for the incremental \gls{rewriting}. diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 59ef75b..a51d1f4 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -253,7 +253,7 @@ As an example, we can define a function that squares an integer as follows. \end{mzn} \Gls{rewriting} (eventually) transforms all \minizinc{} expressions into function calls. -As such, the usage of function declarations is the primary method for \solvers{} to specify how to rewrite a \minizinc{} model into a \gls{slv-mod}. +As such, function declarations are the primary method for \solvers{} to specify how to rewrite a \minizinc{} model into a \gls{slv-mod}. The collection of function declarations to rewrite for a \solver{} is generally referred to as a \solver{} library. In this library, functions can be declared without a function body. This marks them as \gls{native} to the \solver{}. @@ -454,11 +454,11 @@ In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\roo \subsection{Handling Undefined Expressions}% \label{subsec:back-mzn-partial} -In this subsection we discuss the handling of partial functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. +In this subsection we discuss the handling of \gls{partial} functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. When a function has a well-defined result for all its possible inputs it is said to be total. Some expression in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs. -Part of the semantics of a \cml{} is the choice as to how to treat these partial functions. +Part of the semantics of a \cml{} is the choice as to how to treat these \gls{partial} functions. \begin{example}\label{ex:back-undef} Consider, for example, the following ``complex \constraint{}''. @@ -471,11 +471,11 @@ Part of the semantics of a \cml{} is the choice as to how to treat these partial Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \mzninline{i} takes the value seven. This means the expression \mzninline{a[i]} undefined. - If \minizinc{} did not implement any special handling for partial functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found. + If \minizinc{} did not implement any special handling for \gls{partial} functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found. However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true. \end{example} -Other examples of partial functions in \minizinc{} are: +Other examples of \gls{partial} functions in \minizinc{} are: \begin{itemize} \item division (or modulus) when the divisor is zero, @@ -866,7 +866,7 @@ Specifically \gls{ampl} was designed to model linear programs. These days \gls{ampl} has been extended to allow more advanced \solver{} usage. Depending on the \gls{solver} targeted by \gls{ampl}, the language gives the modeller access to additional functionality. Different types of \solvers{} can also have access to different types of \constraints{}, such as quadratic and non-linear \constraints{}. -\gls{ampl} has even been extended to allow the usage of certain \glspl{global} when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}. +\gls{ampl} has even been extended to allow certain \glspl{global} when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}. \begin{example} @@ -1025,7 +1025,7 @@ In addition to all variable types that are supported by \minizinc{}, \gls{essenc \begin{itemize} \item Finite sets of non-integer types, \item finite multi-sets of any type, - \item finite (partial) functions, + \item finite (\gls{partial}) functions, \item and (regular) partitions of finite types. \end{itemize} @@ -1272,7 +1272,7 @@ The process then analyses the \gls{ast} to discover the types of all expressions If an inconsistency is discovered, then an error is reported to the modeller. Finally, the frontend also preprocesses the \gls{ast}. This process is used to transform expressions into a common form for the middle-end, removing the ``syntactic sugar''. -For instance, this replaces the usage of enumerated types by normal integers. +For instance, this replaces enumerated types by normal integers. \begin{figure} \centering diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 097477b..3fe8ddf 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -9,73 +9,115 @@ \input{chapters/4_half_reif_preamble} -\section{An Introduction to Half Reification} +\section{An Introduction to Half-Reification} \label{sec:half-intro} -The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reif} in the \gls{rewriting} process to reach a \gls{slv-mod}. -If 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, its \gls{cvar}. +The 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}. +If 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. +We call \mzninline{b} the \gls{cvar} of the expression. The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the truth-value of the expression (\ie\ \mzninline{b <-> pred(...)}). -\textcite{feydy-2011-half-reif} show that although the usage of \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses: +\textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses. -\begin{enumerate} - \item Many \glspl{reif} are created in the rewriting of partial expressions to accommodate \minizinc{}'s \glspl{rel-sem}. +\begin{itemize} + \item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \glspl{rel-sem}. \item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce. - \item A \gls{reif} sometimes provides too much information to its surrounding context, triggering \glspl{propagator} that will never be able to prune any values from a \gls{domain}. -\end{enumerate} +\end{itemize} As an alternative, the authors introduce \gls{half-reif}. -\gls{half-reif} follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}. -\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{reif}: +It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}. +\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{reif}. -\begin{enumerate} - \item \Gls{rewriting} using \glspl{half-reif} naturally produces \glspl{rel-sem}. - \item \Glspl{propagator} for a \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its regular \constraint{}. - \item \Gls{half-reif} does not often interact with its \gls{cvar}, limiting the amount of triggered \glspl{propagator} that are known to be unable to prune any \domains{}. -\end{enumerate} +\begin{itemize} + \item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls. + \item \Glspl{propagator} for \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its non-\gls{reified} \constraint{}. +\end{itemize} Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more complex than the \gls{decomp} of a \gls{half-reif}. -We will show that the usage of \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}. +We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}. \Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be false. -We see this in, for example, a disjunction \(a \lor b\). -No matter the value of \(a\), setting the value of \(b\) to be true can never make the overall expression false. -\(b\) is thus never forced to be false. This requirement follows from the difference between implication and logical equivalences. -Setting the left hand side of a implication to false, does not influence the value on the right hand side. -So if we know that this is never required in the overall expression, then using an implication instead of a logical equivalence (\ie{} a \gls{half-reif} instead of a full \gls{reif}) does not change the meaning of the \constraint{}. +Setting the left-hand side of an implication to false does not influence the value on the right-hand side. +This is why the \gls{cvar} should never be forced to be false, since this would not enforce the negation of the \constraint{}. +Setting the right-hand side of an implication to true also does not influence the left-hand side. +This is, however, not an issue since in this case the value can just be assigned by the \gls{propagation} of other \constraints{} or a \gls{search-decision}. + +\begin{example} + For example, \gls{half-reif} can be used in the following disjunction. + + \begin{mzn} + constraint (x = 5) \/ (y = 5); + \end{mzn} + + This \constraint{} forces that, between \mzninline{x} and \mzninline{y}, at least one \variable{} is takes the value five. + The usual \gls{rewriting} would result in the following (intermediate) model, using \glspl{reif} for the equalities. + + \begin{mzn} + var bool: b1; + var bool: b2; + constraint b1 <-> (x = 5); + constraint b2 <-> (y = 5); + constraint b1 \/ b2; + \end{mzn} + + However, independent of the value of \mzninline{b1}, if \mzninline{b2} takes the value true, then it can never make the disjunction false. + Therefore, \mzninline{propagation} of the disjunction can never force \mzninline{b2} to take the value false. + Consequently, this means using \gls{half-reif} is \gls{eqsat}. + \Gls{rewriting} using \gls{half-reif} will result in the following model. + + \begin{mzn} + var bool: b1; + var bool: b2; + constraint b1 -> (x = 5); + constraint b2 -> (y = 5); + constraint b1 \/ b2; + \end{mzn} + +\end{example} This property can be extended to include non-Boolean expressions. Since Boolean expressions in \minizinc{} can be used in, for example, integer expressions, we can apply similar reasoning to these types of expressions. \begin{example} - For example the left hand side of the following \constraint{} is an integer expression that contains the Boolean expression \mzninline{x = 5}. + For example, the left-hand side of the following \constraint{} is an integer expression that contains the Boolean expression \mzninline{x = 5}. \begin{mzn} constraint count(x in arr)(x = 5) > 5; \end{mzn} - Since the increasing left hand side of the \constraint{} will only ever help satisfy the \constraint{}, the expression \mzninline{x = 5} will never forced to be false. - This means that the expression can be \gls{half-reified}. + Making the left-hand side of the \constraint{} bigger will only ever help satisfy the \constraint{}. + This means \mzninline{propagation} of the expressions \mzninline{x = 5} can never force them to take the value false. + The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions. \end{example} -To systematically analyse whether Boolean expressions can be \gls{half-reified}, we introduce extra distinctions in the context of expressions. +To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} \wrt{} an expression. +A relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{monotone} with regards to its argument \(a_{i}\) when given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \geq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m})\), independent of other arguments. +Contrariwise, a relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{antitone} with regards to its argument \(a_{i}\) if given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \leq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m}) \), independent of the other arguments. +Where, for clarification, we assume \( \text{false} < \text{true} \). + +Using these definitions, we introduce extra distinctions in the context of expressions. Before, we would merely distinguish between \rootc{} context and non-\rootc{} context. -Now, we will categorise the latter into: +Now, we will categorise the latter into the following three contexts. \begin{description} - \item[\posc{}] when an expression must reach \textbf{at least} a certain value to satisfy its enclosing \constraint{}. - The expression is never forced to take a lower value. + \item[\posc{}] An expression is in \posc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} \wrt{} the expression. - \item[\negc{}] when an expression can reach \textbf{at most} a certain value to satisfy its enclosing \constraint{}. - The expression is never forced to take a higher value. + \item[\negc{}] An expression is in \negc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} \wrt{} the expression. - \item[\mixc{}] when an expression must take an \textbf{exact value}, be within a \textbf{specified range} or when during \gls{rewriting} it cannot be determined whether the expression must be increased or decreased to satisfy the enclosing \constraint{}. + \item[\mixc{}] An expression is in \mixc{} context when its enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone \wrt{} the expression. \end{description} -As previously explained, \gls{half-reif} can be used for expressions in \posc{} context. +Determining the monotonicity of a \constraint{} \wrt{} an expression is a hard problem. +An expression might be monotone or antitone only through complex interactions, possibly through unknown \gls{native} \constraints{}. +Therefore, for our analysis, we slightly relax these definitions. +We say an expression is in \mixc{} context when it cannot be determined whether its enclosing \constraint{} is monotone or antitone \wrt{} the expression. + +Expressions in \posc{} context are the ones we discussed before. +A Boolean expression in \posc{} context cannot be forced to be false. +As such, the\gls{half-reif} can be used for expressions in \posc{} context. Although 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}. \begin{example} @@ -86,7 +128,7 @@ Although expressions in a \negc{} context cannot be directly \gls{half-reified}, \end{mzn} The expression \mzninline{x = 5} is in a \negc{} context. - Although a \gls{half-reif} cannot be used directly, in some cases the \solver{} can negate the expression which are then placed in a \posc{} context. + 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{}. Our example can be transformed into the following \constraint{}. \begin{mzn} @@ -99,44 +141,58 @@ Although expressions in a \negc{} context cannot be directly \gls{half-reified}, Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible. Only full \gls{reif} can be used for expressions that are in this context. -This occurs, for example, when using an exclusive or expression in a \constraint{}. -The value that one side must take directly depends on the value that the other side takes. -Each side can thus be forced to be true or false. -The \mixc{} context can also be used as a ``fall back'' context. -If it cannot be determined if an expression is in a \posc{} or \negc{} context, then it is always safe to say the expression is in a \mixc{} context. + +\begin{example} + + An example of a \constraint{} that introduces \mixc{} contexts is the following. + + \begin{mzn} + constraint (x = 5) xor (y = 5); + \end{mzn} + + This \constraint{} forces either \mzninline{x} or \mzninline{y}, but not both, to take the value five. + The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on if \mzninline{x} has already taken the value five, and vice versa. + As such, when \mzninline{x} takes the value five it forces \mzninline{y} to not take the value five. + This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{} + +\end{example} + \section{Propagation and Half Reification}% \label{sec:half-propagation} -The tasks of a \gls{propagator} for any \constraint{} can logically be split into two: +Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform: \begin{enumerate} - \item to \(check\) if the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}), - \item and to \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}. + \item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}), + \item \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}, and + \item check whether the \constraint{} is \(entailed\) (\ie{}, proven to be \gls{satisfied}). \end{enumerate} -When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these two tasks. -The \gls{half-reified} \gls{propagator} is dependent on an additional argument \texttt{b}, the \gls{cvar}. -The Boolean \variable{} can be in three states, it can currently not have been assigned a value, it can be assigned \mzninline{true}, or it can be assigned \mzninline{false}. -Given \texttt{b}, \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo code for the \gls{propagation} of the \gls{half-reif} of the \constraint{}. +When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these tasks. +The \gls{half-reified} \gls{propagator} is dependent on an additional argument \(b\), the \gls{cvar}. +The Boolean \variable{} 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. +Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows pseudo code for the \gls{propagation} of the \gls{half-reif} of the \constraint{}. -\begin{algorithm} +\begin{algorithm}[t] - \KwIn{A function \(check\), that returns false when the \constraint{} \(c\) cannot be satisfied, a function \(prune\), that eliminates values from \variable{} \glspl{domain} that violate\glsadd{violated} the \constraint{} \(c\), and a Boolean \gls{cvar} \texttt{b}. + \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\). } - \KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(\texttt{b} \implies\ c\)).} + \KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)) and returns whether the \constraint is entailed.} \BlankLine{} - \If{\texttt{b} {\normalfont is unassigned} }{ + \If{\(b \text{ is unassigned}\)}{ \If{\(\neg{}check()\)}{ - \(\texttt{b} \longleftarrow \) \mzninline{false}\; + \(b \longleftarrow \text{false}\)\; + \Return{} \(\text{true}\)\; } } - \If{\(\texttt{b} = \mzninline{true}\)}{ + \If{\(\texttt{b} = \text{true}\)}{ \(prune()\)\; + \Return{} \(entailed()\)\; } - - \caption{\label{alg:half-prop} Propagation pseudo code for the \gls{half-reif} of a \constraint{} \(c\), based on the propagator for \(c\).} + \Return{} \(\text{false}\)\; + \caption{\label{alg:half-prop} \gls{propagation} pseudo code for the \gls{half-reif} of a \constraint{} \(c\), based on the \gls{propagator} for \(c\).} \end{algorithm} Logically, the creation of \glspl{propagator} for \glspl{half-reif} can always follow this simple principle. @@ -148,29 +204,62 @@ When a \gls{domain} is found to be empty, then the \gls{propagator} declares the It is not possible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) operation. Instead a new explicit \(check\) method has to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}. -\Glspl{propagator} gain certain advantages from \gls{half-reif}, but also may suffer certain penalties. -\Gls{half-reif} can cause propagators to wake up less frequently: \glspl{cvar} that are fixed to true by full \gls{reif} will never be fixed by \gls{half-reif}. -This is advantageous, but a corresponding disadvantage is that \glspl{cvar} that are fixed can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster. +In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical task. +In addition, we require the logical task from a \gls{propagator} of \(\neg{} c\): \(checkNeg\), \(pruneNeg\), and \(entailedNeg\). +Using these additional functions, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop} +Although this might seem reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define. +\todo{insert good example of global constraint.} -When a full \gls{reif} is required, its \gls{propagation} might still be performed using \gls{half-reif}. -A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using two half reified propagators, \mzninline{x -> pred(...)} and \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}. +\begin{algorithm}[t] + + \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \(c\), The functions \(checkNeg\), \(pruneNeg\), and \(entailedNeg\) that form the for non-\gls{reified} \gls{propagator} of \(\neg{} c\), and a Boolean \gls{cvar} \(b\). + } + \KwResult{This pseudo code propagates the \gls{reif} of \(c\) (\ie{} \(b \leftrightarrow{} c\)) and returns whether the \constraint{} is entailed.} + + \BlankLine{} + \If{\(b \text{ is unassigned}\)}{ + \If{\(\neg{} check()\)}{ + \(b \longleftarrow \text{false}\)\; + } + \If{\(\neg{} checkNeg()\)}{ + \(b \longleftarrow \text{true}\)\; + } + } + \If{\(\texttt{b} = \text{true}\)}{ + \(prune()\)\; + \Return{} \(entailed()\)\; + } + \If{\(\texttt{b} = \text{false}\)}{ + \(pruneNeg()\)\; + \Return{} \(entailedNeg()\)\; + } + \Return{} \(\text{false}\)\; + \caption{\label{alg:reif-prop} \Gls{propagation} pseudo code for the \gls{reif} of a \constraint{} \(c\), based on the \glspl{propagator} for \(c\) and \(\neg{} c\).} +\end{algorithm} + +\Gls{half-reified} \glspl{propagator} have certain advantages over \gls{reified} \glspl{propagator}, but also may suffer certain penalties. +\Gls{half-reif} can cause \glspl{propagator} that use their \gls{cvar} to wake up less frequently: \glspl{cvar} that are fixed to true by full \gls{reif} will never be fixed by \gls{half-reif}. +This can be advantageous, but has a corresponding disadvantage. +When a \gls{cvar} is fixed, it can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster. + +When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{propagator} to implement it. +A 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}. This does not lose \gls{propagation} strength. For 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}. Similarly in \negc{} context we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority. This means that the \glspl{cvar} are still fixed at the same time, but there is less overhead. -In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element}. -Both \glspl{propagator} are designed and implemented in \gls{chuffed} according to the principles explained above. +In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles. \section{Decomposition and Half Reification}% \label{sec:half-decomposition} The use of \gls{half-reif} does not only offer a benefit when a \gls{propagator} for the \gls{half-reified} \constraint{} is available. It can also be beneficial in the \gls{decomp} of \constraints{}. -Compared to full \gls{reif}, the \gls{decomp} of a \gls{half-reif} does not need to keep track of as much information. +Compared 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. In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} \solver{}. The \glspl{decomp} for these \solver{} technologies often explicitly encode \gls{reified} \constraints{} using two implications. -If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implication is required. +If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implications is required. \begin{example} @@ -188,10 +277,10 @@ If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of the The same principle can be applied all throughout the \gls{linearization} process. Ultimately, \minizinc{}'s \gls{linearization} library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}. -For all these \glspl{reif}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reif}. +For all these \glspl{reif}, replacement by a \gls{half-reif} can remove half of the implications. For \gls{sat} solvers, a \gls{decomp} for a \gls{half-reif} can be created from its regular \gls{decomp}. -Any \constraint{} \(c\) will \gls{decomp} into \gls{cnf} of the following form. +Any \constraint{} \(c\) will decompose into \gls{cnf} of the following form. \[ c = \forall_{i} \exists_{j} lit_{ij} \] The \gls{half-reif}, with \gls{cvar} \texttt{b}, could take the following encoding. \[ \texttt{b} \implies c = \forall_{i} \neg \texttt{b} \lor \exists_{j} lit_{ij} \] @@ -213,12 +302,6 @@ In \cref{sec:half-experiments} we assess the effects when \gls{rewriting} with \ \section{Context Analysis}% \label{sec:half-context} -When 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 value context, and the context in which the partiality of the expression is captured, its partiality context. -As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions. -This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false. -In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression. -The partiality context is the context in which this condition is placed. - The context of an expression cannot always be determined by merely considering \minizinc{} expressions top-down. Expressions bound to an identifier can be used multiple times in expressions that influence their context. @@ -231,7 +314,7 @@ Expressions bound to an identifier can be used multiple times in expressions tha } in y -> x /\ x -> z; \end{mzn} - The predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}. + The result of predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}. If \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well. As such, the call could then be \gls{half-reified}. @@ -240,23 +323,56 @@ Expressions bound to an identifier can be used multiple times in expressions tha \end{example} Note that an alternative approach for this example would be to replace the identifier with its definition. -It would then be possible to \gls{half-reified} versions of both the call and the negation of the call. +It would then be possible to use \gls{half-reified} versions of both the call and the negation of the call. Although 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. In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model. +When 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}. +As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions. +This means that if a function if the result of a function is undefined, then its nearest enclosing Boolean expression becomes false. +In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression. +The partiality context is the context in which this condition is placed. + +\begin{example} + We can illustrate the difference between the two contexts in the following \minizinc{} fragment. + + \begin{mzn} + var 0..10: x + constraint b \/ y div x < 4; + \end{mzn} + + In this fragment, we study the context of the division expression \mzninline{y div x}. + The expression itself return a integer \variable{} and it used on the left-hand side of a less than \constraint{}. + This result is therefore in a \negc{} context: it is only forced to take a smaller value. + This is its value context. + + 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. + In this case, the expression \mzninline{x != 0} is added to the right-hand side of the disjunction as follows. + + \begin{mzn} + var 0..10: x + constraint b \/ ( x != 0 /\ y div x < 4); + \end{mzn} + + \noindent{}The partiality context of the division is the context in which this condition is added. + Here, the condition is added in a \posc{} context. +\end{example} + \subsection{Automated analysis}% \label{subsec:half-automated} In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically. The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}. -It requires knowledge about all usages of certain \variable{} at the same time. -This information is not available during during the interpretation of \microzinc{}. +It requires knowledge about all usages of each \variable{} at the same time. +This information is not available during the interpretation of \microzinc{}. Without loss of generality we can define the context analysis process for \microzinc{} models. -This has the advantage that the value and partiality have already been explicitly separated and no longer requires special handling. +This has the advantage that \microzinc{} does not contain \gls{partial} function calls. +The partiality in \minizinc{} has already been translated using only total functions (see \cref{sec:rew-micronano}). +The context analysis therefore does not have to keep track of value and partiality contexts separately. We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules. The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}. -Each rules describe how an expression is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line. +Each rule describes how an expression that is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line. The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\). We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}. The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}. @@ -328,29 +444,27 @@ Note that the presented inference rules do not have any explicit state object. Instead, we introduce the functions ``pushCtx'' and ``collectCtx''. These functions track and combine the contexts in which a value is used in an implicit global state. -Most changes in the context of \microzinc{} expressions stem from the consequent (Call) rule. +Most changes in the context of \microzinc{} expressions stem from the (Call) rule. A call expression can change the context in which its arguments should be evaluated. As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call. A definition for this function for the \minizinc{} operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.} Although a standard definition for the ``argCtx'' function may cover the most common cases, it does not cover user-defined functions. To 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. -When a function argument is annotated with one of these annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation corresponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)). +When 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 annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)). If a function argument is not annotated, then the argument is evaluated in \mixc{} context. +It may be possible to infer these \glspl{annotation} from the function body. +However, we currently do not provide such analysis and annotate functions by hand. \begin{example} - Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}. - - \begin{listing} - \mznfile{assets/listing/half_impli.mzn} - \caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.} - \end{listing} - The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}. - In term of context analysis, this function now is equivalent to the \minizinc{} operator. - + In terms of context analysis, this function now is equivalent to the \minizinc{} operator. \end{example} +\begin{listing} + \mznfile{assets/listing/half_impli.mzn} + \caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.} +\end{listing} \begin{algorithm} \KwIn{A \minizinc\ operator \(op\) and calling context \(ctx\)} @@ -398,12 +512,12 @@ Otherwise, the \compiler{} follows the following steps to try to introduce the m \item[\mixc] \glspl{reif} can be defined as \(ident\)\mzninline{_reif}. \end{description} - \item If \(ident\) is a \microzinc{} function with an expression body \(E\), then copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}. + \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}. \item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1. \item Finally, if none of the earlier steps were successful, then the compilation fails. - Note that this can only occur when a \gls{native} \constraint{} does not define a \gls{reif}. + Note that this can only occur when there is no definition for the \gls{reif} of a \constraint{}, \ie{} neither a \gls{native} constraint nor a \gls{decomp}. \end{enumerate} The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively. @@ -469,7 +583,7 @@ And, unlike \minizinc{}, the \constraint{} is not dependent on the context of th The \constraint{}'s expression is evaluated in \rootc{} context. The (Assign) rule reasons about declarations that have a right hand side. -The expression that is assigned to the identifier must evaluated in the combined context of its usages. +The expression that is assigned to the identifier must be evaluated in the combined context of its usages. As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function. These contexts are then combined using a ``join'' function. This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}. @@ -494,7 +608,7 @@ The context of the individual members of tuples is tracked separately. This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts. Finally, the (Decl) and (Item0) rules describe two base cases in the inference. -The declaration item of a \variable{} does not further the context, and does not depend on it. +The declaration item of a \variable{} does not further affect the context, and does not depend on it. It merely triggers the creation of a new \variable{}. The (Item0) rule is triggered when there are no more inner items in the let-expression. @@ -519,7 +633,7 @@ It is, however, not always safe to do so. \end{mzn} Let us assume that \mzninline{b} is a \parameter{}, but that its value is not known during the compilation from \minizinc{} to \microzinc{}. - In this case, we know that only one side of the \gls{conditional} expression will evaluated, and that call will then globally constrain the \cmodel{}. + 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{}. As such, the \compiler{} can output calls to the \rootc{} variant of the functions. This will enforce the \constraint{} in the most efficient way. @@ -541,10 +655,10 @@ It is, however, not always safe to do so. In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls. \end{example} -Using the \changepos{} transformation for sub-expression contexts is safe, but it places a large burden on the \solver{}. -The solver performs better when the no \gls{reif} has to be used. +Using the \changepos{} transformation for sub-expressions contexts is safe, but it places a large burden on the \solver{}. +The solver performs better without using \gls{reif}. -To detect situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context. +To detect the situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context. This context functions as a ``weak'' \rootc{} context. If it is joined with any other context, then it acts as \posc{}. The extended join operation is shown in \cref{fig:half-maybe-join}. @@ -583,8 +697,8 @@ Otherwise, it will act as a normal \rootc{} context. Looking 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. For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context. Therefore, it will output the \posc{} call for the right hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}. -At compile time, this is only correct context to use. -We will, however, discuss the dynamically adjusting of contexts during \gls{rewriting} in \cref{subsec:half-dyn-context}. +At compile time, this is the only correct context to use. +We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}. \section{Rewriting and Half Reification}% \label{sec:half-rewriting} @@ -600,7 +714,7 @@ During the \gls{rewriting} process the contexts assigned to the different expres constraint (y -> f(x)) \/ not x = 5; \end{mzn} - \noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that be both \gls{reified} or \gls{half-reified}. + \noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that can be both \gls{reified} or \gls{half-reified}. For this \constraint{} we can determine the following contexts for its sub-expressions: \begin{itemize} @@ -609,7 +723,7 @@ During the \gls{rewriting} process the contexts assigned to the different expres \item and the rest are in \posc{} context. \end{itemize} - \Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraint{}. + \Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraints{}. \begin{mzn} constraint bool_clause([b1, b2], []); % b1 \/ b2 @@ -629,8 +743,8 @@ During the \gls{rewriting} process the contexts assigned to the different expres \end{mzn} We are able to replace the two \glspl{reif} and push the negation inwards, transforming the equals \constraint{} into a not equals \constraint{}. - Note, however, that the rewriting did form many extra implications. - If the Boolean \mzninline{y} was not further \constraint{} in the problem, then we could further reduce it to the following \constraints{}. + Note, however, that the rewriting produced many extra implications. + If the Boolean \mzninline{y} was not further constrained in the problem, then we could further reduce it to the following \constraints{}. \begin{mzn} constraint bool_clause([y, b2], []); % y \/ b2 @@ -643,13 +757,13 @@ During the \gls{rewriting} process the contexts assigned to the different expres As this example shows, the use of \gls{half-reif} can form so called \glspl{implication-chain}. This happens when the right hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression. Instead, we could have used the left hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}. -In \cref{subsec:half-compress} we present a new post-processing method we call \gls{chain-compression}. +In next section, we present a new post-processing method we call \gls{chain-compression}. It can be used to eliminate these \glspl{implication-chain}. The \gls{rewriting} with \gls{half-reif} also interacts with some of the optimisation methods used during the \gls{rewriting} process. -Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} can change the context of expression. +Most importantly, \gls{half-reif} has to be considered when using \gls{cse}, and \gls{propagation} can change the context of an expression. In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}. -Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is executed can be adjusted during the \gls{rewriting} process. +Finally, 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. \subsection{Chain compression}% \label{subsec:half-compress} @@ -674,7 +788,7 @@ An algorithm to remove these chains of implications is best comprehended through An implication graph \(\tuple{V,E}\) is a directed graph. The vertices \(V\) represent the \variables{} in the \instance{}. An edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance. -Additionally, for the benefit of the algorithm, is marked when it is used in other \constraints{} in the \constraint{} model. +Additionally, the algorithm requires vertices to be marked when their corresponding \variables{} are used in other \constraints{} in the \cmodel{}. The goal of the algorithm is now to identify and remove vertices that are not marked and have only one incoming edge. \Cref{alg:half-compression} provides a formal specification of the \gls{chain-compression} method in pseudo code. @@ -717,7 +831,7 @@ The expression above is logically equivalent to the following expression. \end{mzn} Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of \glspl{implication-chain}. -It should however be noted that although this transformation can increase the number of \constraints{} in the \gls{slv-mod}, it generally increases the \gls{propagation} efficiency. +It 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. To adjust the algorithm to simplify implied conjunctions, more introspection from the \minizinc{} \compiler{} is required. The \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. @@ -727,11 +841,11 @@ In the case where a \variable{} has one incoming edge, but it is marked as used \label{subsec:half-cse} When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table. -This ensure that if the same expression is \gls{reified} twice, then the resulting \gls{reif} will be reused. +This ensures that if the same expression is \gls{reified} twice, then the resulting \gls{cvar} will be reused. This avoids that the solver has to enforce the same functional relation twice. If 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. -For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{half-reif} from the first cannot be used for the second expression. +For 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. In general the following rules apply. \begin{itemize} @@ -741,7 +855,7 @@ In general the following rules apply. \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. \item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context. - Since we assume that the result of a \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated. + Since we assume that the result of \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated. \item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \mzninline{true} (or \mzninline{false} in \negc{} context). @@ -752,40 +866,37 @@ It would always be better to encounter the expression in a context that results This avoids creating both a full \gls{reif} and a \gls{half-reif} of the same expression. In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the result of their joint context. -The context recorded in the \gls{cse} table and the found context are joint using the join operator, as described in \cref{fig:half-join}. +The context recorded in the \gls{cse} table and the found context are joined using the join operator, as described in \cref{fig:half-join}. If 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. -All usages of the previously recorded result is replaced by the new result. +All usages of the previously recorded \gls{cvar} are replaced by the new result. The dependency tracking through the use of \constraints{} attached to \variables{} ensures no defining \constraints are left in the model. -This ensures that all \variables{} and \constraints{} created the earlier version are correctly removed. +This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed. Because 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. This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards. In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table. -If it is found that for an expression that is about to be \gls{half-reified} there already exists an \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context. +If 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. The expression is \gls{reified} and replaces the existing \gls{half-reified} expression. \begin{example} - - Consider for example the \mzninline{=} operator, in \microzinc{} seen as a \mzninline{int_eq} call. + Consider for example the \mzninline{=} operator on integers, which \microzinc{} represents as an \mzninline{int_eq} call. When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} operator, a \mzninline{int_ne} call. The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} operator. 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. The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for an \mzninline{int_ne} call. - \end{example} This canonical form for expressions and their negations can also be used for the expressions in other contexts. Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation. Instead, when one is created, the negation of the resulting \variable{} can directly be used as the \gls{reif} of its negation. Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context. -This is simple way to detect conflicts between \constraints{} and, by extend, prove that the \cmodel{} is \gls{unsat}. -Clearly, a \constraint{} and its negation cannot both hold at the same time. +Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsatisfiable}. \subsection{Dynamic Context Switching}% \label{subsec:half-dyn-context} In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing \microzinc{}. -Its context depends on data that is only known at an \instance{} level. +The context may depends on data that is only known at an \instance{} level. The same situation can be caused by \gls{propagation}. \begin{example} @@ -810,43 +921,39 @@ The same situation can be caused by \gls{propagation}. \end{example} The situation shown in the example is the most common change of context. -If the \gls{cvar} of a \gls{reif} is fixed, the context often changes to either \rootc{} or a negated \rootc{} context. -If, on the other hand, the \gls{cvar} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the \constraint{} already holds. +If the \gls{cvar} of a \gls{reif} is fixed, the context changes to either \rootc{} or a negated \rootc{} context. +If, on the other hand, the \gls{cvar} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the \constraint{} is trivially \gls{satisfied}. Since 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. This problem can be solved by the \compiler{}. -For each \gls{reif} and \gls{half-reif} the \compiler{} introduces another layer of \gls{decomp}. -In this layer, it checks its \gls{cvar}. -If the \gls{cvar} is already fixed, then it rewrites itself into its form in another context. +For each \gls{reif} and \gls{half-reif} the \compiler{} introduces a layer of indirection. +In this layer, it checks the \gls{cvar}. +If the \gls{cvar} is already fixed, then it rewrites itself into the corresponding form in another context. Otherwise, it behaves as it would have done normally. The \gls{cvar} is thus used to communicate the change in context. \begin{example} - - Let's assume the \compiler{} finds a call to \mzninline{int_lin_le} in \posc{} context. - Instead of outputting the call to \mzninline{int_lin_le_imp} directly, it will instead output a call to \mzninline{_int_lin_le_imp}. + Let's assume the \compiler{} finds a call to \mzninline{int_eq} in \posc{} context. + Instead of outputting the call to \mzninline{int_eq_imp} directly, it will instead output a call to \mzninline{int_eq_imp_check}. This predicate is then generated as shown in \cref{lst:half-check-reif}. - This new predicate (calls) can then be rewritten normally. - - \begin{listing} - \mznfile{assets/listing/half_reif_check.mzn} - \caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_lin_le_imp} that checks its \gls{cvar} to ensure a \gls{half-reif} is still required.} - \end{listing} - + The \gls{rewriting} of the calls to the generated predicate then follow the normal process. \end{example} +\begin{listing} + \mznfile{assets/listing/half_reif_check.mzn} + \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.} +\end{listing} + \section{Experiments} \label{sec:half-experiments} -We now present experimental evaluation of the presented techniques. -First, to show the benefit of implementing propagators for \gls{half-reified} \constraint{}, we compare their performance against their \glspl{decomp}. -To do this, we 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}. -In the experiment, we use \glspl{propagator} implemented according to the principles described in this paper. -No new algorithm has been devised to perform the \gls{propagation}. -The \gls{propagator} of the direct \constraint{} is merely adjusted to influence and watch a \gls{cvar}. +We now present an experimental evaluation of the presented techniques. +First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{} by comparing their performance against their \glspl{decomp}. +We 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}. +We 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}. Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the \gls{rewriting} process. -We rewrite and solve 200 \minizinc{} instances for several \solvers{} with and without the use of \gls{half-reif}. +We rewrite and solve 200 \minizinc{} \instances{} for several \solvers{} with and without the use of \gls{half-reif}. We then analyse the trends in the generated \glspl{slv-mod} and their solving performance. A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}. @@ -856,13 +963,13 @@ A description of the used computational environment, \minizinc{} instances, and Our first experiment considers the QCP-max quasi-group completion problem. In this problem, we need to decide the value of an \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}. -The aim of the problem is to create as many rows and columns where all \variables{} take a unique value. +The aim of the problem is to create as many rows and columns as possible where all \variables{} take a unique value. In each \instance{} certain values have already been fixed. It is not always possible for all rows and columns to contain only distinct values. In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}. Since the goal of the problem is to maximise the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}. -This means these \constraints{} in a \posc{} context and can be \gls{half-reified}. +This means these \constraints{} are in \posc{} context and can be \gls{half-reified}. \Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem. The results are grouped based on their size of the instance. @@ -870,18 +977,18 @@ For each group we show the number of instances solved by the configuration and t In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a \gls{propagator}. This \gls{propagator} is an adjusted version from the existing \gls{bounds-con} \mzninline{all_different} \gls{propagator} in \gls{chuffed}. -The 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 \variables{}. +The 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{}. Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied. Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well. -These adjustments happen in a similar fashion to the adjustments of the general algorithm: explanations used for the violation of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false} and the explanations given to prune a variable are appended by requirement that the \gls{cvar} is \mzninline{true}. +These adjustments happen in a similar fashion 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 \mzninline{false}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \mzninline{true}. In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}. The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}. -Their conjunction, then represent the \gls{reif} of the \mzninline{all_different} \constraint{}. +Their conjunction then represent the \gls{reif} of the \mzninline{all_different} \constraint{}. \begin{listing} \mznfile{assets/listing/half_alldiff.mzn} - \caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} standard library.} + \caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} library.} \end{listing} @@ -894,22 +1001,22 @@ Their conjunction, then represent the \gls{reif} of the \mzninline{all_different \end{center} \end{table} -The results in \cref{tab:half-qcp} show that the usage of the specialised \gls{propagator} has a significant advantage over the use of the \gls{decomp}. -Although it only allows us to solve a one extra instance, there is a significant reduction in solving time for most \instances{}. +The results in \cref{tab:half-qcp} show that the specialised \gls{propagator} has a significant advantage over the use of the \gls{decomp}. +Although it only allows us to solve one extra instance, there is a significant reduction in solving time for most \instances{}. Note that the qcp-15 \instances{} are the only exception. It 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. -For our second experiment we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem. +In addition, we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem. In the problem we are given a graph with weighted edges, both positive and negative. The aim of the problem is to find the optimal acyclic path from a given start node that maximises the weights on the path. It is not required to visit every node. In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly. -The \minizinc{} model for this problem contains a unsafe \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}. +The \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}. We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}. The \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}. Otherwise, it will set its surrounding context to \mzninline{false}. -The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the result of the \mzninline{element} \constraint{} does not match the value of the index variable. +The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}. Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above. \begin{table} @@ -922,20 +1029,20 @@ Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \co \end{table} The results of the experiment are shown in \cref{tab:half-prize}. -Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the usage of the \gls{decomp}. +Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the \gls{decomp}. The difference in performance becomes more pronounced in the bigger \instances{}. In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}. \subsection{Rewriting with Half Reification} \label{sec:half-exp-rewriting} -The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate the usage of \gls{half-reif} on a larger scale. +The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \gls{half-reif} on a larger scale. In 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}. -These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which has been adapted to use \gls{half-reif} as earlier described. -The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable the usage of \gls{half-reif}. -The solving of the linearised \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}. -The solving of the Booleanised \instances are testing using the \gls{openwbo} \solver{}. -is +These experiments are conducted using the \gls{gecode} \solver{}, which have \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which has been adapted to use \gls{half-reif} as earlier described. +The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable \gls{half-reif}. +The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}. +The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}. + \begin{table} \begin{subtable}[b]{\linewidth} \input{assets/table/half_flat_gecode} @@ -971,23 +1078,24 @@ This replacement happens mostly 1-for-1; the difference between the number of \g In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced. Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimisation techniques is minimal. -The \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearization. -Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall \constraints{}. -The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as \gls{gecode}. +The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization. +Since 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{}. +The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as with \gls{gecode}. This is caused by the fact that the linearization process requires full \gls{reif} in the decomposition of many \glspl{global}. Similar to \gls{gecode}, the number of implications that is removed is dependent on the problem. Lastly, the \gls{rewriting} time slightly increases for the linearization process. -Since there are many more \constraints{}, the introduced optimisation mechanisms have an slightly higher overhead. +Since there are many more \constraints{}, the introduced optimisation mechanisms have a slightly higher overhead. -Finally, statistics for the \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} is shown in \cref{subtab:half-flat-bool}. -Unlike linearization, the usage of \gls{half-reif} does not significantly reduces number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent. -We also see that that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}. +Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} are shown in \cref{subtab:half-flat-bool}. +Unlike 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. +We also see that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}. Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition. Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}. -Furthermore, the usage of \gls{chain-compression} does not seem to have any effect. +Furthermore, \gls{chain-compression} does not seem to have any effect. Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into bigger clauses. -Surprisingly, the usage of \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload. -The relatively small changes shown might indicate that additional work is required to correctly annotate predicates and functions in the Booleanisation library. +Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload. +The relatively small changes shown might indicate that additional work might be warranted in the Booleanisation library. +It might 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. \begin{table} \input{assets/table/half_mznc} @@ -997,7 +1105,7 @@ The relatively small changes shown might indicate that additional work is requir \Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports \begin{description} - \item[Unsatisfiable] when it proofs the instance does not have a solution, + \item[Unsatisfiable] when it proves the instance does not have a solution, \item[Optimal solution] when it has found a solution and has proven it optimal, \item[Satisfied] when it has found a solution for the problem, \item[Unknown] when no solution is found, and @@ -1006,25 +1114,25 @@ The relatively small changes shown might indicate that additional work is requir \noindent{}For \solver{} statuses that end the solving process before the time-out of 15 minutes we also show the average time. -The results shown is this table are very mixed. -For \gls{gecode}, the usage of \gls{half-reif} does not seem to impact its solving performance. -Although we would have hoped that propagators for \glspl{half-reif} would be more efficient and reduce the number of propagators scheduled in general. -Neither number of instances solved, nor the solving time required improved. -A single instance, however, is negatively impacted by the change; an optimal solution for this instance is no longer found. -We expect that this \instance{} has benefited from the increased Boolean propagation that is caused by full \gls{reif}. +The results shown in this table are very mixed. +For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance. +We would have hoped that \glspl{propagators} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general. +However, neither number of \instances{} solved, nor the solving time required improved. +A single \instance{}, however, is negatively impacted by the change; an \gls{opt-sol} for this \instance{} is no longer found. +We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}. Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}. -When using \gls{cplex} the usage of \gls{half-reif} is clearly a positive one. +When using \gls{cplex}, \gls{half-reif} clearly has a positive effect. Although it no longer proves the unsatisfiability of one instance and slightly increases the number of solver errors, an optimal solution is found for five more instances. -The same linearised instances when using the \gls{cbc} solver seem to have the opposite effect. +The same linearized instances when using the \gls{cbc} solver seem to have the opposite effect. Even though it reduces the time required to prove that two instances are unsatisfiable, it can no longer find six optimal solutions. These results are hard to explain. In general, we would expect the reduction of \constraints{} in a \gls{mip} instance would help the \gls{mip} solver. However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver. -An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance. -Some patterns can only be detected when using a full \gls{reif}. +An important technique used by \gls{mip} solvers is to detect certain patterns, such as cliques, during the pre-processing of the \gls{mip} instance. +Some patterns can only be detected when using full \gls{reif}. Furthermore, 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}. -With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}. +When 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. The solving statistics for \gls{openwbo} might be most positive. Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}. diff --git a/chapters/4_half_reif_preamble.tex b/chapters/4_half_reif_preamble.tex index 8a42b46..f69eb3c 100644 --- a/chapters/4_half_reif_preamble.tex +++ b/chapters/4_half_reif_preamble.tex @@ -1,23 +1,24 @@ \noindent{}Whether a \constraint{} has to be \gls{reified} is a crucial decision made during \gls{rewriting}. \minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other. -However, determining whether a \constraint{} holds, \(b \leftrightarrow{} c\), requires significantly more effort from the \solver{} than merely enforcing the \constraint{} \(c\). -A \gls{reified} \constraint{} results in a larger \gls{decomp} or a more complex \gls{native} \constraint{}. -It it thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required. +However, using a \gls{reif} \(b \leftrightarrow{} c\), that determines whether a \constraint{} \(c\) holds, can slow the \solver{} down. +Even in \gls{cp} \solvers{}, not many \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak. +Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result a large number of \gls{native} \constraints{} and \variables{}. +It is thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required. In this chapter we present an extended \gls{reif} analysis to help minimise the required \solver{} effort. Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}. The notion of \gls{half-reif} \(b \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}. -It is shown \gls{half-reif} can relieve some of the problems and expenses of the use of \gls{reif}. +It is shown \gls{half-reif} can mitigate some of the problems and expenses of the use of \gls{reif}. It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}. The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique. Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalise to the full \minizinc{} language. -This chapter re-evaluates the usage of \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}. +This chapter re-evaluates \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}. This chapter is organised as follows. In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and \glspl{propagator} for \gls{half-reified} \constraints{}, as discussed by \textcite{feydy-2011-half-reif}. An additional benefit of \gls{half-reif} is that its \gls{decomp} can be significantly smaller than the \gls{decomp} of a \gls{reif}. \Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} for \gls{mip} and \gls{sat} \solvers{}. In \cref{sec:half-context} we introduce our new context analysis algorithm: a way to determine where \gls{half-reif} can be used in \microzinc{}, and by extension \minizinc{}. -Then, in \cref{sec:half-rewriting}, we elaborate on how the usage of \gls{half-reif} changes the \gls{rewriting} process. +Then, in \cref{sec:half-rewriting}, we elaborate on how using \gls{half-reif} changes the \gls{rewriting} process. Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the automatic introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}. diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index 71a5a29..8018f26 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -46,8 +46,8 @@ Crucially, the architecture is easily extended with well-known simplification te Two prototype programs were developed to evaluate this architecture: \begin{itemize} - \item a \compiler{} that translates \minizinc{} models to a \microzinc{} \gls{byte-code}, - \item and a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}. + \item a \compiler{} that translates \minizinc{} models to a \microzinc{} \gls{byte-code}, and + \item a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}. \end{itemize} The implementation of these prototypes lacks the maturity of the existing \minizinc{} \compiler{}. @@ -71,10 +71,10 @@ Not only does this analysis reduce the number of required \glspl{reif}, it is th Our method introduces a new analysis step after the compilation from \minizinc{} to \microzinc{}. To determine whether a \constraint{} has to be \gls{reified}, this analysis determines the context of each \constraint{}. -Crucially, our analysis considers the possibility of identifiers being used in multiple positions, and the usage of user-defined \constraints{}. -Depending on the context of a \constraint, we can decide if a \gls{reif} can be avoided, if a \gls{half-reif} can be used, or if we have to use a full \gls{reif}. +Crucially, our analysis considers the possibility of identifiers being used in multiple positions and user-defined functions. +Depending on the context of a \constraint{}, we can decide if a \gls{reif} can be avoided, if a \gls{half-reif} can be used, or if we have to use a full \gls{reif}. -We noted that the usage of \gls{half-reif} interacts with some of the existing simplification techniques in the architecture and propose alterations to accommodate them. +We noted that \gls{half-reif} interacts with some of the existing simplification techniques in the architecture and propose alterations to accommodate them. Foremost, \gls{cse} can no longer always reuse the same results for identical \constraints{}, it must now consider the context of the \constraint{}. For \constraints{} were \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result. Using this adjustment we ensure that identical \constraints{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts. @@ -100,7 +100,7 @@ As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solve As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}. In this form the propagator would set the \gls{cvar} to \mzninline{true} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \mzninline{false}. The downside of this form is that it is no longer equivalent to a logical implication (and, for example, \gls{chain-compression} would no longer be applicable), but \glspl{propagator} for this form are still easy to design/implement and they ensure that the \gls{cvar} is fixed through \gls{propagation}. -Finally, the usage of automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}. +Finally, automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}. \paragraph{Incremental Solving} Using a \cml{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and open up new opportunities. The modeller can describe the process as a changing \cmodel{}. @@ -134,7 +134,7 @@ Our experiments show that this method is not as effective as \gls{rbmo}. It is, however, still a significant improvement over repeatedly \gls{rewriting} the full \instance{} that can be employed even in cases where \gls{rbmo} cannot be used. The improvements offered by these new methods may spark future research. -Primarily, they will allow and promote the usage of \gls{meta-optimization} methods in \cmls{} for new problems. +Primarily, they will allow and promote using \gls{meta-optimization} algorithms in \cmls{} for new problems. It could even be worthwhile to revisit existing applications of incremental constraint modelling. The utilisation of the presented methods might offer a significant improvement in performance, allowing the solving of more complex problems. Finally, new \gls{meta-optimization} techniques could require extensions of the methods presented.