Notes by Peter
This commit is contained in:
parent
7cd31c628c
commit
2bd95d1abd
@ -65,7 +65,7 @@ The flattener then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which
|
||||
\item A \gls{reification} sometimes provides too much information to its surrounding context, triggering propagators that will never be able to prune any values from a \gls{domain}.
|
||||
\end{enumerate}
|
||||
|
||||
In constast, the authors introduce \gls{half-reif}.
|
||||
In contrast, the authors introduce \gls{half-reif}.
|
||||
\gls{half-reif} follows from the idea that in many cases it might be sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
|
||||
Flattening with \gls{half-reif} is an approach that improves upon all these weaknesses of flattening with \emph{full} reification:
|
||||
|
||||
@ -98,7 +98,7 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
|
||||
|
||||
\noindent{}is an integer expression that contains the Boolean expression \mzninline{x = 5}.
|
||||
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 we can half-reify the expression.
|
||||
This means that we only need to half-reify the expression.
|
||||
\end{example}
|
||||
|
||||
To systematically analyse whether Booelean expressions can be half-reified, we introduce extra distinctions in the context of expressions.
|
||||
@ -225,7 +225,7 @@ If, however, a \gls{reification} is replaced by a \gls{half-reif}, then only one
|
||||
\end{example}
|
||||
|
||||
The same principle can be applied all throughout the linearisation process.
|
||||
Ultimately, \minizinc{}'s linearisation library rewrites most \glspl{reification} in terms of implied less than or equal to constraint.
|
||||
Ultimately, \minizinc{}'s linearisation library rewrites most \glspl{reification} in terms of implied less than or equal to \constraints{}.
|
||||
For all these \glspl{reification}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reification}.
|
||||
|
||||
For \gls{sat} solvers, a decomposition for a \gls{half-reif} can be created from its regular decomposition.
|
||||
@ -246,7 +246,7 @@ This adds a new binary clause for every literal in the original \gls{cnf}.
|
||||
In general, many more clauses are needed to decompose a \gls{reification} compared to a \gls{half-reif}.
|
||||
|
||||
According to the principles above, decomposition libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} solvers.
|
||||
In \cref{sec:half-experiments} we asses the effects when flattening with \gls{half-reif}.
|
||||
In \cref{sec:half-experiments} we assess the effects when flattening with \gls{half-reif}.
|
||||
|
||||
\section{Context Analysis}%
|
||||
\label{sec:half-context}
|
||||
@ -261,7 +261,7 @@ The context of an expression cannot always be determined by merely considering \
|
||||
Expressions bound to a variable can be used multiple times in expressions that influence their context.
|
||||
|
||||
\begin{example}
|
||||
Consider the following \minizinc\ fragment.
|
||||
Consider the following \minizinc{} fragment.
|
||||
|
||||
\begin{mzn}
|
||||
constraint let {
|
||||
@ -270,15 +270,17 @@ Expressions bound to a variable can be used multiple times in expressions that i
|
||||
\end{mzn}
|
||||
|
||||
The predicate call \mzninline{pred(a, b, c)} is bound to the variable \mzninline{x}.
|
||||
The call is in \posc\ context, and can be half-reified, if the variable \mzninline{x} is only used in \posc{} context.
|
||||
If the \variable{} \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 half-reified.
|
||||
|
||||
Although this is the case in the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
|
||||
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context, and must fully reified.
|
||||
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully reified.
|
||||
\end{example}
|
||||
|
||||
Note that an alternative approach for this example would be to replace the identifier with its definition.
|
||||
It would then be possible half-reify the call and the negation of the call.
|
||||
It would then be possible to half-reify the call and the negation of the call.
|
||||
Although this would increase the use of \gls{half-reif}, it should be noted that the propagation of these two \glspl{half-reif} would be equivalent to propagating the full \gls{reification} of the call.
|
||||
In this scenario, we prefer to create the full \gls{reification} as it decreases the number of \variables{} and \constraint{} in the model.
|
||||
In this scenario, we prefer to create the full \gls{reification} as it decreases the number of \variables{} and \constraints{} in the model.
|
||||
|
||||
\subsection{Automated analysis}%
|
||||
\label{subsec:half-automated}
|
||||
@ -340,7 +342,7 @@ The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
|
||||
\bigskip
|
||||
\begin{prooftree}
|
||||
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
|
||||
\infer1[(ITE)]{\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
|
||||
\infer1[(ITE)]{\ctxeval{b}{ctx},~\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
|
||||
\end{prooftree} \\
|
||||
\bigskip
|
||||
\begin{prooftree}
|
||||
@ -357,10 +359,10 @@ The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
|
||||
|
||||
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from let expressions.
|
||||
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affects any sub-expressions.
|
||||
Instead every context in which the identifier are found are collected and will be processed when evaluating the corresponding declaration.
|
||||
Instead every context in which the identifier is found is collected and will be processed when evaluating the corresponding declaration.
|
||||
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 an value is used in an implicit global state.
|
||||
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.
|
||||
A call expression can change the context in which its arguments should be evaluated.
|
||||
@ -370,11 +372,11 @@ A definition for this function for the \minizinc\ operators can be found in \cre
|
||||
Although a standard definition for the ``argMax'' function may cover the most common cases, it does not cover user-defined functions stemming from \minizinc{}.
|
||||
To address this issue, we introduce the \minizinc{} annotations \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 coressponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
|
||||
If a function argument is not annotated, then the argument is evaluated in \mixc context.
|
||||
If a function argument is not annotated, then the argument is evaluated in \mixc{} context.
|
||||
|
||||
\begin{example}
|
||||
|
||||
Consider the following user-defined \minizinc\ implementation of a logical implication.
|
||||
Consider the following user-defined \minizinc{} implementation of a logical implication.
|
||||
|
||||
\begin{mzn}
|
||||
predicate impli(
|
||||
@ -384,8 +386,8 @@ If a function argument is not annotated, then the argument is evaluated in \mixc
|
||||
not x \/ y;
|
||||
\end{mzn}
|
||||
|
||||
The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as a direct \minizinc\ implication, as shown in \cref{alg:arg-ctx}.
|
||||
In term of context analysis, this function now is equivalent to the \minizinc implication operator.
|
||||
The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as a direct \minizinc{} implication, as shown in \cref{alg:arg-ctx}.
|
||||
In term of context analysis, this function now is equivalent to the \minizinc{} implication operator.
|
||||
|
||||
\end{example}
|
||||
|
||||
@ -435,12 +437,12 @@ Otherwise, the compiler follows the following steps to try to introduce the most
|
||||
\item[\mixc] \glspl{reification} 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 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 non of the earlier steps were successful, then the compilation fails.
|
||||
Note that this can only occurr when a solver-level predicate does not have an \gls{reification}.
|
||||
\item Finally, if none of the earlier steps were successful, then the compilation fails.
|
||||
Note that this can only occur when a solver-level predicate does not have a \gls{reification}.
|
||||
\end{enumerate}
|
||||
|
||||
The (Access) and (ITE) rules show the context inference for array access and if-then-else expressions respectively.
|
||||
@ -503,7 +505,7 @@ Note that the \(ctx\) of the let-expression itself, is irrelevant for the analys
|
||||
The inference for \constraint{} items is described by the (Con) rule.
|
||||
Since \microzinc{} implements strict semantics, the \constraint{} can be assumed to hold globally.
|
||||
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the let-expression.
|
||||
The \constraint{}'s expression is evaluated in \rootc context.
|
||||
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.
|
||||
@ -539,7 +541,7 @@ The (Item0) rule is triggered when there are no more inner items in the let-expr
|
||||
\label{subsec:half-?root}
|
||||
|
||||
In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
|
||||
Different from the rules described, when an array access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc context as well.
|
||||
Different from the rules described, when an array access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc{} context as well.
|
||||
It is, however, not always safe to do so.
|
||||
|
||||
\begin{example}
|
||||
@ -566,7 +568,7 @@ It is, however, not always safe to do so.
|
||||
} in ret;
|
||||
\end{mzn}
|
||||
|
||||
One side of the if-then-else expression is not also used in a disjunction.
|
||||
One side of the if-then-else expression is also used in a disjunction.
|
||||
If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction.
|
||||
Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
|
||||
It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
|
||||
@ -605,7 +607,7 @@ Otherwise, it will act as a normal \rootc{} context.
|
||||
\bigskip
|
||||
\begin{prooftree}
|
||||
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
|
||||
\infer1[(ITE-R)]{\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
|
||||
\infer1[(ITE-R)]{\ctxeval{c}{ctx},~\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
|
||||
\end{prooftree}
|
||||
\caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
|
||||
\end{figure*}
|
||||
@ -635,7 +637,7 @@ In \cref{subsec:half-compress} we present a new post-processing method, \emph{ch
|
||||
The flattening with \gls{half-reif} also interacts with some of the optimisation methods used during the flattening process.
|
||||
Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} might change the context of 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 to context in which a expression is executed can be adjusted during the flattening process.
|
||||
Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which a expression is executed can be adjusted during the flattening process.
|
||||
|
||||
\subsection{Chain compression}%
|
||||
\label{subsec:half-compress}
|
||||
@ -654,11 +656,11 @@ The case shown in the example can be generalised to
|
||||
forall(i in N)(b1 -> c[i])
|
||||
\end{mzn}
|
||||
|
||||
\noindent{}after which \texttt{b1} can be removed from the model.
|
||||
\noindent{}after which \texttt{b2} can be removed from the model.
|
||||
|
||||
|
||||
An algorithm to remove these chains of implications is best visualised through the use of an implication graph.
|
||||
An implication graph \(\tuple{V,E}\) is a directed graph where the vertices \(V\) represent the variables in the instance and an edge \(\tuple{x,y} \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
|
||||
An implication graph \(\tuple{V,E}\) is a directed graph where the vertices \(V\) represent the variables in the instance and 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, a vertex is marked when it is used in other constraints in the constraint model.
|
||||
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 chain compression method in pseudo code.
|
||||
@ -673,12 +675,13 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
|
||||
\(V' \longleftarrow V\)\;
|
||||
\(E' \longleftarrow E\)\;
|
||||
\For{\(x \in V\)} {
|
||||
\If{\(x \not\in M\) \textbf{ and }\(\left|\left\{\tuple{a,x}| \tuple{a,x} \in E\right\}\right| = 1\)}{
|
||||
\For{\(\tuple{x, b} \in E\)}{
|
||||
\(E' \longleftarrow E' \cup \{ \tuple{a,b} \} \)\;
|
||||
\(E' \longleftarrow E' \backslash \{ \tuple{x,b} \} \)\;
|
||||
\If{\(x \not\in M\) \textbf{ and }\(\left|\left\{(a,x)| (a,x) \in E\right\}\right| = 1\)}{
|
||||
\(a \longleftarrow \text{how to bind??}\)\;
|
||||
\For{\((x, b) \in E\)}{
|
||||
\(E' \longleftarrow E' \cup \{ (a,b) \} \)\;
|
||||
\(E' \longleftarrow E' \backslash \{ (x,b) \} \)\;
|
||||
}
|
||||
\(E' \longleftarrow E' \backslash \{ \tuple{a,x} \} \)\;
|
||||
\(E' \longleftarrow E' \backslash \{ (a,x) \} \)\;
|
||||
\(V' \longleftarrow V' \backslash \{ x \} \)\;
|
||||
}
|
||||
}
|
||||
@ -686,6 +689,7 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
|
||||
\caption{\label{alg:half-compression} Implication chain compression algorithm}
|
||||
\end{algorithm}
|
||||
|
||||
\todo{Correctly bind a}
|
||||
The algorithm can be further improved by considering implied conjunctions.
|
||||
These can be split up into multiple implications:
|
||||
|
||||
@ -752,6 +756,8 @@ Moreover, this mechanism also allows us to detect when an expression and its neg
|
||||
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the constraint model is unsatisfiable.
|
||||
Clearly, a \constraint{} and its negation cannot both hold at the same time.
|
||||
|
||||
\todo{This needs an example!!! To complex}
|
||||
|
||||
\subsection{Dynamic Context Switching}%
|
||||
\label{subsec:half-dyn-context}
|
||||
|
||||
@ -783,18 +789,18 @@ The same situation can be caused by \gls{propagation}.
|
||||
The situation shown in the example is the most common change of context.
|
||||
If the control \variable{} of a \gls{reification} is fixed, the context often changes to either \rootc{} or a negated \rootc{} context.
|
||||
If, on the other hand, the control \variable{} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the constraint already holds.
|
||||
Since regular \constraints{} are strongly preferred over any form of \gls{reification}, it is important to dynamically pick the correct form at during the flattening process.
|
||||
Since regular \constraints{} are strongly preferred over any form of \gls{reification}, it is important to dynamically pick the correct form during the flattening process.
|
||||
|
||||
This problem can be solved by the compiler.
|
||||
For each \gls{reification} and \gls{half-reif} the compiler should introduce another layer of decomposition.
|
||||
In this layer, it checks its control \variable{}.
|
||||
If the control \variable{} is already fixed, then it rewrites itself into its form in another context.
|
||||
Otherwise, it behaves as it would have done normally.
|
||||
The control \variable is thus used to communicate any change in context.
|
||||
The control \variable{} is thus used to communicate any change in context.
|
||||
|
||||
\begin{example}
|
||||
|
||||
Let's assume the compiler find a call to \mzninline{int_lin_le} in \posc{} context.
|
||||
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}.
|
||||
This predicate is then generated as follows:
|
||||
|
||||
@ -826,7 +832,7 @@ The control \variable is thus used to communicate any change in context.
|
||||
|
||||
We now present experimental evaluation of the presented \gls{half-reif} techniques.
|
||||
First, to show the benefit of implementing propagators for half-reified constraint, we compare their performance against their decompositions.
|
||||
To do this, we recreate two experiments presented by \citeauthor{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
|
||||
To do this, we recreate two experiments presented by \citeauthor{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed} \autocite*{feydy-2011-half-reif}.
|
||||
In the experiment, we use propagators implemented according to the principles described in this paper.
|
||||
No new algorithm has been devised to perform the propagation.
|
||||
The propagator of the original constraint is merely adjusted to influence and watch a control \variable{}.
|
||||
@ -855,7 +861,7 @@ The results are grouped based on their size of the instance.
|
||||
For each group we show the number of instances solved by the configuration and the average time used for this process.
|
||||
|
||||
In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a newly created propagator.
|
||||
This propagator is an adjusted version from the existing bounds consistent \mzninline{all_different} propagator in chuffed.
|
||||
This propagator is an adjusted version from the existing bounds consistent \mzninline{all_different} propagator in \gls{chuffed}.
|
||||
The implementation of the propagator was already split into parts that \emph{check} the violation of the constraint and parts that \emph{prune} the \glspl{domain} of \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 propagator have to be adjusted as well.
|
||||
@ -919,7 +925,7 @@ In the 32-4-8 group, we even see that usage of the propagator allows us to solve
|
||||
|
||||
The introduction of automated context analysis and introduction of \glspl{half-reif} allows us to evaluate the usage of \gls{half-reif} on a larger scale.
|
||||
In our second experiment we assess its effects on the flattening 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 constraint, and the \minizinc{}'s linearisation library, which has been adapted to use \gls{half-reif} as earlier described.
|
||||
These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s linearisation library, which has been adapted to use \gls{half-reif} as earlier described.
|
||||
The \minizinc{} instances are flattened using the \minizinc{} 2.5.5 flattener, which can enable and disable the usage of \gls{half-reif}.
|
||||
The solving of the linearised models is tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
|
||||
|
||||
@ -964,7 +970,7 @@ Finally, the overhead of the introduction of \gls{half-reif} and the newly intro
|
||||
The \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearisation.
|
||||
Since both \glspl{reification} and \glspl{half-reif} are decomposed during the flattening process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall constraints.
|
||||
The ratio of \glspl{reification} that is replaced with \glspl{half-reif} is not as high as \gls{gecode}.
|
||||
This is caused by the fact that the linearisation process requires full \gls{reification} in the decomposition of many \gls{global} \constraints{}.
|
||||
This is caused by the fact that the linearisation process requires full \gls{reification} 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 flattening time slightly increases for the linearisation process.
|
||||
Since there are many more constraints, the introduced optimisation mechanisms have an slightly higher overhead.
|
||||
@ -1006,7 +1012,7 @@ Overall, these results do not show any significant positive or negative effects
|
||||
When using \gls{cplex} the usage of \gls{half-reif} is clearly a positive one.
|
||||
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.
|
||||
Eventhough it reduces the time required to prove that two instances are unsatisfiable, it can no longer find six optimal solutions.
|
||||
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 might in some cases help the \gls{mip} solver.
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
\noindent{}\citeauthor{feydy-2011-half-reif} introduced the notion of \gls{half-reif} as an improvement over the use of \gls{reification} \autocite*{feydy-2011-half-reif}.
|
||||
\noindent{}\citeauthor{feydy-2011-half-reif} introduced the notion of \gls{half-reif}\todo{You need an example of what half reification is b -> c !!!} as an improvement over the use of \gls{reification} \autocite*{feydy-2011-half-reif}.
|
||||
They show that some of the problems and expenses of the use of \gls{reification} can be mitigated using this technique.
|
||||
In addition, the creation of propagators for \glspl{half-reif} of constraints can often be an easy process.
|
||||
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reification}.
|
||||
@ -11,6 +11,6 @@ This chapter re-evaluates the usage of \gls{half-reif} and provides the first fu
|
||||
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and propagators for half-reified \constraints{}, as discussed by \citeauthor{feydy-2011-half-reif}.
|
||||
An additional benefit of \gls{half-reif} is that its decomposition can be significantly smaller than the decomposition of a \gls{reification}.
|
||||
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing decompositions 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 extend \minizinc{}.
|
||||
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-flattening}, we elaborate on how the usage of \gls{half-reif} changes the flattening process.
|
||||
Finally, the effects of propagators for half-reified constraints and the automatic introduction of half-reified is analysed in \cref{sec:half-experiments}.
|
||||
|
||||
Reference in New Issue
Block a user