diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 4a1958a..1b4ffd8 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -111,7 +111,7 @@ Now, we will categorize the latter into the following three contexts. \end{description} Determining the monotonicity of a \constraint{} w.r.t.\@ an expression is a hard problem. -An expression might be monotone or antitone only through complex interactions, possibly through unknown \gls{native} \constraints{}. +An expression can be monotone or antitone only through complex interactions, possibly through unknown \gls{native} \constraints{}. Therefore, for our analysis, we approximate these definitions. We say an expression is in \mixc{} context when it cannot be determined syntactically whether the enclosing \constraint{} is monotone or antitone w.r.t.\@ the expression. @@ -162,76 +162,74 @@ Only full \gls{reif} can be used for expressions that are in this context. Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform: \begin{enumerate} - \item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}), + \item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the \constraint{} to be \gls{violated}), \item \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}, and \item check whether the \constraint{} is \(entailed\) (i.e., 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 tasks. -The \gls{half-reified} \gls{propagator} has 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{}. +The \gls{half-reified} \gls{propagator} has a \gls{cvar} \(b\), as an additional argument. +The \gls{cvar} can be in three states, it can currently not have been assigned a value, it can be assigned \true{}, or it can be assigned \false{}. Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows pseudocode for the \gls{propagation} of the \gls{half-reif} of the \constraint{}. \begin{algorithm}[t] \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\). } - \KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns whether the \constraint is entailed.} + \KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns to the \solver{} whether the \constraint{} is \gls{violated}, and whether it is entailed.} \BlankLine{} \If{\(b \text{ is unassigned}\)}{ \If{\(\neg{}check()\)}{ \(b \longleftarrow \false{}\)\; - \Return{} \(\true{}\)\; + \Return{} \(\false{},~\true{}\)\; } } \If{\(\texttt{b} = \true{}\)}{ \(prune()\)\; - \Return{} \(entailed()\)\; + \Return{} \(\neg{} check(),~entailed()\)\; } - \Return{} \(\false{}\)\; + \Return{} \(\false{},~\false{}\)\; \caption{\label{alg:half-prop} \gls{propagation} pseudocode 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. In practice, however, this is not always possible. -In some cases, \glspl{propagator} do not explicitly define \(check\) as a separate step. -Instead, this process can be implicit. -The \gls{propagator} merely prunes the \glspl{domain} of the \variables{}. +In some cases, \glspl{propagator} do not explicitly define \(check\), or \(entailed\) as separate steps, but perform them as part of the pruning process. When a \gls{domain} is found to be empty, then the \gls{propagator} declares the current state \gls{unsat}. -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{}. +It is not possible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) or \(entailed\) operation. +Instead, new explicit methods have to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}. -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. +In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical tasks. +In addition, we require the \(prune\) task from a \gls{propagator} of \(\neg{} c\). +Using these additional function, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}. Although this seems reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define. For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that forces that at least two values are equal. -This far from a common \constraint{} and we are not aware of any \solver{} that implements a \gls{propagator} for it. +This is far from a common \constraint{} and we are not aware of any \solver{} that implements a \gls{propagator} for it. \begin{algorithm}[t] - \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{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\). + \KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \(c\), the function \(pruneNeg\) that prunes the values of the \constraint{} \(\neg{} c\), and a Boolean \gls{cvar} \(b\). } - \KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns whether the \constraint{} is entailed.} + \KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns to the \solver{} whether the \constraint{} is \gls{violated}, and whether it is entailed.} \BlankLine{} \If{\(b \text{ is unassigned}\)}{ \If{\(\neg{} check()\)}{ \(b \longleftarrow \false{}\)\; } - \If{\(\neg{} checkNeg()\)}{ + \If{\(entailed()\)}{ \(b \longleftarrow \true{}\)\; } } \If{\(\texttt{b} = \true{}\)}{ \(prune()\)\; - \Return{} \(entailed()\)\; + \Return{} \(\neg{} check(),~entailed()\)\; } \If{\(\texttt{b} = \false{}\)}{ \(pruneNeg()\)\; - \Return{} \(entailedNeg()\)\; + \Return{} \(entailed(),~\neg{} check()\)\; } - \Return{} \(\false{}\)\; + \Return{} \(\false{},~\false{}\)\; \caption{\label{alg:reif-prop} \Gls{propagation} pseudocode for the \gls{reif} of a \constraint{} \(c\), based on the \glspl{propagator} for \(c\) and \(\neg{} c\).} \end{algorithm} @@ -887,7 +885,7 @@ This ensures that all \variables{} and \constraints{} created for the earlier ve \end{mzn} In this fragment the call \mzninline{int_le(i, 4)} occurs both in \posc{} and \mixc{} context. - Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions might result from function \gls{rewriting} were this is not possible. + Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions can result from function \gls{rewriting} were this is not possible. After \gls{rewriting} the first \constraint{}, the \nanozinc{} program would contain the following definitions. \begin{nzn} @@ -1146,8 +1144,8 @@ Even when we do not automatically introduce \glspl{half-reif}, they are still in 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 larger clauses. 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 \gls{booleanization} 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. +The relatively small changes shown indicate that additional work may be warranted in the \gls{booleanization} library. +It may be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts. \begin{table} \input{assets/table/half_mznc} @@ -1186,7 +1184,7 @@ 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}. 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. +The solving statistics for \gls{openwbo} may 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{}. It negatively impacts one \instance{}, for which find a \gls{sol} is not found any more. That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change. diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index 4bbb570..d26143d 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -9,9 +9,8 @@ \section{An Introduction to Meta-Optimization} -There are many kinds of \gls{meta-optimization} algorithms. -They share neither a goal nor an exact method. -However, many of them be described through the use of incremental \constraint{} modelling. +There are many kinds of \gls{meta-optimization} algorithms, with different goals and different methods. +However, many of them can be described through the use of incremental \constraint{} modelling. Each algorithm solves an \instance{}, adds new \constraints{}, the resulting \instance{} is solved again, and the \constraints{} may be removed again. This process is repeated until the goal of the \gls{meta-optimization} algorithm is reached. @@ -23,7 +22,7 @@ The following algorithms are examples of \gls{meta-optimization}. Instead, it can be achieved using a \gls{meta-optimization} approach: find a \gls{sol} to a (single-objective) problem, then add more \constraints{} to the original problem and repeat. \item[\gls{lns}] \autocite{shaw-1998-local-search} - This \gls{meta-optimization} algorithm was first introduced as a heuristic to vehicle routing problem, but has proven to be a very successful method to quickly improve \gls{sol} quality for many types of problem. + This \gls{meta-optimization} algorithm was first introduced as a heuristic for vehicle routing problems, but has proven to be a very successful method to quickly improve \gls{sol} quality for many types of problem. After finding a (sub-optimal) \gls{sol} to a problem, \constraints{} are added to restrict the search in the \gls{neighbourhood} of that \gls{sol}. When a new \gls{sol} is found, the \constraints{} are removed, and \constraints{} for a new \gls{neighbourhood} are added. @@ -42,13 +41,13 @@ The following algorithms are examples of \gls{meta-optimization}. \end{description} The usage of \gls{meta-optimization} algorithms is not new to \cmls{}. -Languages such as \gls{opl} and \gls{comet} \autocite{michel-2005-comet} language, later succeeded by the \gls{obj-cp} library \autocite{hentenryck-2013-objcp}, provide convenient syntax for programmable search for their target \solvers{}. -Crucially, \gls{comet} the first system to introduce the notion of applying new \constraints{} on \gls{restart}. +Languages such as \gls{opl} and \gls{comet} \autocite{michel-2005-comet}, later succeeded by the \gls{obj-cp} library \autocite{hentenryck-2013-objcp}, provide convenient syntax for programmable search for their target \solvers{}. +Crucially, \gls{comet} was the first system to introduce the notion of applying new \constraints{} on \gls{restart}. A \gls{restart} happens when a solver abandons its current search efforts, returns to its initial \gls{search-space}, and begins a new exploration. In many (\gls{cp}) \solvers{} it is possible to add new \constraints{} upon restarting that are only valid for the particular \gls{restart}. Many \gls{meta-optimization} algorithms can be implemented using only this technique. -Even though \minizinc{} does not have explicit support for programmable search, \gls{meta-optimization} algorithms have been successfully applied to the language. +Even though \minizinc{} does not have explicit support for programmable search, \gls{meta-optimization} algorithms have been successfully implemented using the language. \begin{itemize} \item \textcite{schiendorfer-2018-minibrass} use \gls{meta-optimization} algorithms to solve \minizinc{} \instances{} that have been extended to contain soft-\constraints{}. \item \textcite{ingmar-2020-diverse} implement \gls{meta-optimization} algorithms to explore the diversity of \glspl{sol} for \minizinc{} models. @@ -58,7 +57,7 @@ Even though \minizinc{} does not have explicit support for programmable search, In its most basic form, a simple scripting language is sufficient to implement these algorithms, by repeatedly \gls{rewriting} and solving the adjusted \instances{}. For some applications the runtime required to repeatedly rewrite the \instance{} can be prohibitive. Approaches such as \gls{search-comb} \autocite{schrijvers-2013-combinators} and \minisearch{} \autocite{rendl-2015-minisearch} have been proposed to reduce this overhead and ease the use of \gls{meta-optimization} in \minizinc{}. -However, these approaches were found hard to implement and maintain, and were never adopted into \minizinc{} +However, these approaches were found hard to implement and maintain, and were never adopted into \minizinc{}. \section{Modelling of Restart Based Meta-Optimization}\label{sec:inc-modelling} @@ -210,7 +209,7 @@ Therefore, we identify each \variable{} using their variable path \autocite{leo- The path of a \variable{} is designed to give a unique identifier to a \variable{} when an \instance{} is rewritten multiple times. The \variable{} path is mostly dependent on the \parameter{} arguments to the calls and the value of iterators for which the \variable{} is introduced. As such, this mechanism will between \glspl{restart} correctly identify the \variables{} for each call to the nullary function in the \mzninline{on_restart} \gls{annotation}. -However, it might lead to slightly unexpected behaviour when using \parameter{} function arguments that do not relate to the \mzninline{avar} introduced in the function. +However, it can lead to slightly unexpected behaviour when using \parameter{} function arguments that do not relate to the \mzninline{avar} introduced in the function. \paragraph{Parametric neighbourhood selection predicates} @@ -302,7 +301,7 @@ It takes advantage of the fact that the declared \gls{objective} is available th A more interesting example is a simulated annealing strategy. When using this strategy, the sequence of \glspl{sol} that the \solver{} finds are not required to steadily improve in quality. Instead, the \solver{} can produce \glspl{sol} that potentially with a potentially reduced objective value. -Over time, we decrease the amount by which a \gls{sol} might decrease objective value until we are only looking for improvements. +Over time, we decrease the amount by which a \gls{sol} can decrease objective value until we are only looking for improvements. This \gls{meta-optimization} can help the \solver{} to quickly approximate the \gls{opt-sol}. \Cref{lst:inc-sim-ann} show how this strategy is also easy to express using \gls{rbmo}. @@ -741,7 +740,7 @@ These orders can then be freely reassigned to any other slab. \Cref{subfig:inc-obj-gecode-steelmillslab} again only shows minimal overhead for the \gls{rbmo} compared to replaying the \glspl{neighbourhood}. For this problem a \gls{sol} with zero wastage is always optimal. -As such the \gls{lns} approaches are sometimes able to prove a \gls{sol} is optimal and might finish before the time-out. +As such the \gls{lns} approaches are sometimes able to prove a \gls{sol} is optimal and finish before the time-out. This is the case for \gls{chuffed} instances, where almost all \instances{} are solved using the \gls{rbmo} method. As expected, the \gls{lns} approaches find better \glspl{sol} more quickly for \gls{gecode}. However, we do see that, given enough time, baseline \gls{gecode} will eventually find better \glspl{sol}.