Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update HR chapter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-03-11 11:42:09 +11:00
parent 73d7c2cded
commit 873d277fe7
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 217 additions and 221 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
assets/shorthands.tex
View File

@ -8,8 +8,6 @@
\newcommand{\cml}{\gls{constraint-modelling} language\xspace{}} \newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
\newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}} \newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
\newcommand{\vari}{\mzninline{var}}
\newcommand{\pari}{\mzninline{par}}
\renewcommand{\phi}{\varphi} \renewcommand{\phi}{\varphi}
\newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}} \newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}}
\newcommand{\Prog}{\ensuremath{\mathcal{P}}} \newcommand{\Prog}{\ensuremath{\mathcal{P}}}
@ -17,17 +15,11 @@
\newcommand{\Env}{\ensuremath{\sigma}} \newcommand{\Env}{\ensuremath{\sigma}}
\newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}} \newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}}
\newcommand{\Cbind}{\ensuremath{\wedge}} \newcommand{\Cbind}{\ensuremath{\wedge}}
\newcommand{\true}{\mzninline{true}}
\newcommand{\false}{\mzninline{false}}
\newcommand{\mdiv}{\mzninline{div}}
\newcommand{\element}{\mzninline{element}}
\newcommand{\alldiff}{\mzninline{all_different}}
% Half-reification math things % Half-reification math things
\newcommand{\VV}{{\cal V}} \newcommand{\VV}{{\cal\ V}}
\newcommand{\PP}{{\cal P}} \newcommand{\PP}{{\cal\ P}}
\newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]} \newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]}
\newcommand{\gfp}{\textup{gfp}} \newcommand{\gfp}{\textup{gfp}}
\newcommand{\lfp}{\textup{lfp}} \newcommand{\lfp}{\textup{lfp}}

17
chapters/4_rewriting.tex
View File

@ -134,7 +134,7 @@ have omitted the definitions of \syntax{<type-inst>} and \syntax{<ident>}, which
you can assume to be the same as in the definition of \minizinc. While we omit you can assume to be the same as in the definition of \minizinc. While we omit
the typing rules here for space reasons, we will assume that in well-typed the typing rules here for space reasons, we will assume that in well-typed
\microzinc\ programs, the conditions \syntax{<exp>} in if-then-else and where \microzinc\ programs, the conditions \syntax{<exp>} in if-then-else and where
expressions have \pari\ type. expressions have \mzninline{par} type.
\begin{figure} \begin{figure}
\begin{grammar} \begin{grammar}
@ -353,13 +353,14 @@ that introduces the variable.
A \nanozinc\ model (\cref{fig:4-nzn-syntax}) consists of a topologically-ordered A \nanozinc\ model (\cref{fig:4-nzn-syntax}) consists of a topologically-ordered
list of definitions. Each definition binds a variable to the result of a call or list of definitions. Each definition binds a variable to the result of a call or
another variable, and it is associated with a list of identifiers of auxiliary another variable, and it is associated with a list of identifiers of auxiliary
constraints. The \nanozinc\ model contains a special definition $\true$, constraints. The \nanozinc\ model contains a special definition
containing all ``root-context'' constraints of the model, i.e., those that have \mzninline{true}, containing all ``root-context'' constraints of the model,
to hold globally and are not just used to define an auxiliary variable. Only i.e., those that have to hold globally and are not just used to define an
root-context constraints (attached to $\true$) can effectively constrain the auxiliary variable. Only root-context constraints (attached to \mzninline{true})
overall problem. Constraints attached to definitions originate from function can effectively constrain the overall problem. Constraints attached to
calls, and since all functions are guaranteed to be total, attached constraints definitions originate from function calls, and since all functions are
can only define the function result. guaranteed to be total, attached constraints can only define the function
result.
\begin{example}\label{ex:4-absnzn} \begin{example}\label{ex:4-absnzn}

409
chapters/5_half_reif.tex
View File

@ -13,7 +13,7 @@ formulated. Modelling languages map the more expressive formulations to
existentially quantified conjunction through a combination of loop unrolling, existentially quantified conjunction through a combination of loop unrolling,
and flattening using reification. and flattening using reification.
\begin{example}\label{ex:cons} \begin{example}\label{ex:hr-cons}
Consider the following ``complex constraint'' written in \minizinc\ syntax Consider the following ``complex constraint'' written in \minizinc\ syntax
\begin{mzn} \begin{mzn}
@ -74,7 +74,7 @@ This is known as the \emph{strict} semantics
The usual choice for modeling partial functions in modelling languages is the The usual choice for modeling partial functions in modelling languages is the
\emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the \emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the
relational semantics the value $\bot$ percolates up through the term until it relational semantics the value $\bot$ percolates up through the term until it
reaches a Boolean subterm where it becomes $\false$. For the example reaches a Boolean subterm where it becomes $\mzninline{false}$. For the example
\begin{mzn} \begin{mzn}
/* t1 @\(\equiv\)@ */ a[7] = ⊥; /* t1 @\(\equiv\)@ */ a[7] = ⊥;
@ -91,7 +91,7 @@ original complex constraint needs to be far more complex.
The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models
implementing the relational semantics. Assuming \texttt{i} takes values in the implementing the relational semantics. Assuming \texttt{i} takes values in the
set \mzninline{1..8}, and \texttt{a} has an index set \mzninline{1..5}, its set \mzninline{1..8}, and \texttt{a} has an index set \mzninline{1..5}, its
translation of the constraint in \cref{ex:cons} is translation of the constraint in \cref{ex:hr-cons} is
\begin{mzn} \begin{mzn}
constraint b1 <-> i <= 4; % b1 holds iff i <= 4 constraint b1 <-> i <= 4; % b1 holds iff i <= 4
@ -120,7 +120,7 @@ functions, is that each reified version of a constraint requires further
implementation to create, and indeed most solvers do not provide any reified implementation to create, and indeed most solvers do not provide any reified
versions of their global constraints. versions of their global constraints.
\begin{example}\label{ex:alldiff} \begin{example}\label{ex:hr-alldiff}
Consider the complex constraint Consider the complex constraint
\begin{mzn} \begin{mzn}
@ -201,19 +201,22 @@ expressiveness in using global constraints.
\section{Propagation Based Constraint Solving} \section{Propagation Based Constraint Solving}
\jip{This section looks like background and should probably be moved}
We consider a typed set of variables $\VV = \VV_I \cup \VV_B$ made up of We consider a typed set of variables $\VV = \VV_I \cup \VV_B$ made up of
\emph{integer} variables, $\VV_I$, and \emph{Boolean} variables, $\VV_b$. We use \emph{integer} variables, $\VV_I$, and \emph{Boolean} variables, $\VV_b$. We use
lower case letters such as $x$ and $y$ for integer variables and letters such as lower case letters such as $x$ and $y$ for integer variables and letters such as
$b$ for Booleans. $b$ for Booleans.
% %
A \emph{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers A \gls{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers
(for the variables in $\VV_I$) and to subsets of $\{\true,\false\}$ (for the (for the variables in $\VV_I$) and to subsets of
variables in $\VV_b$). $\{\mzninline{true},\mzninline{false}\}$ (for the variables in $\VV_b$).
% %
We can understand a domain $D$ as a formula $\wedge_{v \in \VV} (v \in D(v))$ We can understand a \gls{domain} $D$ as a formula
stating for each variable $v$ that its value is in its domain. A \emph{false $\wedge_{v \in \VV} (v \in D(v))$ stating for each variable $v$ that its value
domain} $D$ is a domain where $\exists_{v \in \VV} D(v) = \emptyset$, and is in its domain. A \emph{false domain} $D$ is a domain where
corresponds to an unsatisfiable formula. $\exists_{v \in \VV} D(v) = \emptyset$, and corresponds to an unsatisfiable
formula.
Let $D_1$ and $D_2$ be domains and $V\subseteq\VV$. We say that $D_1$ is Let $D_1$ and $D_2$ be domains and $V\subseteq\VV$. We say that $D_1$ is
\emph{stronger} than $D_2$, written $D_1 \sqsubseteq D_2$, if \emph{stronger} than $D_2$, written $D_1 \sqsubseteq D_2$, if
@ -281,7 +284,7 @@ $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \min D(v_i)$ and
$\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$, and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$, and
similarly exists $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \max D(v_i)$ similarly exists $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \max D(v_i)$
and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$. For and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$. For
Boolean variables $v$ we assume $\false < \true$. Boolean variables $v$ we assume $\mzninline{false} < \mzninline{true}$.
% A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ if the same % A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ if the same
% conditions as for bounds(Z) consistency hold except $\theta \in solns(c')$ where % conditions as for bounds(Z) consistency hold except $\theta \in solns(c')$ where
@ -323,7 +326,10 @@ fixpoint w.r.t $\sqsubseteq$ lifted to functions.
% not going up from an empty one.) % not going up from an empty one.)
\subsection{A Language of Constraints}\label{sec:syntax} \subsection{A Language of Constraints}\label{sec:hr-syntax}
\jip{This introduces a subset of \minizinc, but we can probably use \microzinc\
instead.}
\newcommand{\nonterm}[1]{\textsc{#1}} \newcommand{\nonterm}[1]{\textsc{#1}}
\newcommand{\subs}[1]{[\![ #1 ]\!] } \newcommand{\subs}[1]{[\![ #1 ]\!] }
@ -414,13 +420,13 @@ Given a \syntax{<cons>} term defining the constraints of the model we can split
its \syntax{<cons>} subterms as occurring in different kinds of places: root its \syntax{<cons>} subterms as occurring in different kinds of places: root
contexts, positive contexts, negative contexts, and mixed contexts. A Boolean contexts, positive contexts, negative contexts, and mixed contexts. A Boolean
subterm $t$ of constraint $c$ is in a \emph{root context} iff there is no subterm $t$ of constraint $c$ is in a \emph{root context} iff there is no
solution of $c\subs{t/\false}$, that is $c$ with subterm $t$ replaced by solution of $c\subs{t/\mzninline{false}}$, that is $c$ with subterm $t$ replaced by
$\false$.\footnote{For the definitions of context we assume that the subterm $t$ $\mzninline{false}$.\footnote{For the definitions of context we assume that the subterm $t$
is uniquely defined by its position in $c$, so the replacement is of exactly is uniquely defined by its position in $c$, so the replacement is of exactly
one subterm.} Similarly, a subterm $t$ of constraint $c$ is in a one subterm.} Similarly, a subterm $t$ of constraint $c$ is in a
\emph{positive context} iff for any solution $\theta$ of $c$ then $\theta$ is \emph{positive context} iff for any solution $\theta$ of $c$ then $\theta$ is
also a solution of $c\subs{t/\true}$; and a \emph{negative context} iff for any also a solution of $c\subs{t/\mzninline{true}}$; and a \emph{negative context} iff for any
solution $\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\false}$. solution $\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\mzninline{false}}$.
The remaining Boolean subterms of $c$ are in \emph{mixed} contexts. While The remaining Boolean subterms of $c$ are in \emph{mixed} contexts. While
determining contexts according to these definitions is hard, there are simple determining contexts according to these definitions is hard, there are simple
syntactic rules which can determine the correct context for most terms, and the syntactic rules which can determine the correct context for most terms, and the
@ -432,7 +438,7 @@ Consider the constraint expression
constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5); constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5);
\end{mzn} \end{mzn}
then $x > 0$ is in the root context, $i \leq 4$ is in a negative context, then \mzninline{x > 0} is in the root context, $i \leq 4$ is in a negative context,
$x + \texttt{bool2int}(b) = 5$ is in a positive context, and $b$ is in a mixed $x + \texttt{bool2int}(b) = 5$ is in a positive context, and $b$ is in a mixed
context. If the last equality were $x + \texttt{bool2int}(b) \geq 5$ then $b$ context. If the last equality were $x + \texttt{bool2int}(b) \geq 5$ then $b$
would be in a positive context. would be in a positive context.
@ -452,10 +458,10 @@ for each subterm bottom up using approximation.
% \cons{} subterms as occurring in kinds of places: positive contexts, negative % \cons{} subterms as occurring in kinds of places: positive contexts, negative
% contexts, and mixed contexts. A Boolean subterm $t$ of constraint $c$, written % contexts, and mixed contexts. A Boolean subterm $t$ of constraint $c$, written
% $c[t]$, is in a \emph{positive context} iff for any solution $\theta$ of $c$ % $c[t]$, is in a \emph{positive context} iff for any solution $\theta$ of $c$
% then $\theta$ is also a solution of $c[\true]$, that is $c$ with subterm $t$ % then $\theta$ is also a solution of $c[\mzninline{true}]$, that is $c$ with subterm $t$
% replaced by $\true$. Similarly, a subterm $t$ of constraint $c$ is in a % replaced by $\mzninline{true}$. Similarly, a subterm $t$ of constraint $c$ is in a
% \emph{negative context} iff for any solution $\theta$ of $c$ then $\theta$ is % \emph{negative context} iff for any solution $\theta$ of $c$ then $\theta$ is
% also a solution of $c[\false]$. The remaining Boolean subterms of $c$ are in % also a solution of $c[\mzninline{false}]$. The remaining Boolean subterms of $c$ are in
% mixed contexts. % mixed contexts.
% \begin{example} % \begin{example}
@ -486,7 +492,7 @@ set of possible values of $t$ are included in the domain of $a$,
$poss(t) \subseteq \dom(a)$. $poss(t) \subseteq \dom(a)$.
\section{Flattening with Full Reification} \section{Flattening with Full Reification}
\label{sec:translation} \label{sec:hr-translation}
Constraint problems formulated in \minizinc\ are solved by translating them to a Constraint problems formulated in \minizinc\ are solved by translating them to a
simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc
@ -534,13 +540,13 @@ detailed discussion) but makes the pseudo-code much longer.
The complex part of flattening arises in flattening the constraints, we shall The complex part of flattening arises in flattening the constraints, we shall
ignore the declarations part for flattening and assume that any objective ignore the declarations part for flattening and assume that any objective
function term $e$ is replaced by a new variable $obj$ and a constraint item function term \mzninline{e} is replaced by a new variable \mzninline{obj} and a
$\texttt{constraint}~obj = e$ which will then be flattened as part of the constraint item \mzninline{constraint obj = e} which will then be flattened as
model. part of the model.
\subsection{Flattening Constraints} \subsection{Flattening Constraints}
Flattening a constraint $c$ in context $\ctxt$, $\flatc(c,\ctxt)$, returns a Flattening a constraint $c$ in context \ctxt, $\flatc(c,\ctxt)$, returns a
Boolean literal $b$ representing the constraint and as a side effect adds a set Boolean literal $b$ representing the constraint and as a side effect adds a set
of constraints (the flattening) $S$ to the store such that of constraints (the flattening) $S$ to the store such that
$S \models b \full c$. $S \models b \full c$.
@ -616,7 +622,7 @@ actual flattening rules only differentiate between $\rootc$ and other contexts.
The importance of the $\pos$ context is that \texttt{let} expressions within a The importance of the $\pos$ context is that \texttt{let} expressions within a
$\pos$ context can declare new variables. The important of the $\negc$ context $\pos$ context can declare new variables. The important of the $\negc$ context
is to track $\pos$ context arising under double negations. Note that flattening is to track $\pos$ context arising under double negations. Note that flattening
in the root context always returns a Boolean $b$ made equivalent to $\true$ by in the root context always returns a Boolean $b$ made equivalent to $\mzninline{true}$ by
the constraints in $S$. For succinctness we use the notation $\new b$ ($\new v$) the constraints in $S$. For succinctness we use the notation $\new b$ ($\new v$)
to introduce a fresh Boolean (resp.\ integer) variable and return the name of to introduce a fresh Boolean (resp.\ integer) variable and return the name of
the variable. the variable.
@ -628,7 +634,7 @@ again. We retrieve the result of the previous flattening $h$ and the previous
context $prev$. If the expression previously appeared at the root then we simply context $prev$. If the expression previously appeared at the root then we simply
reuse the old value, since regardless of the new context the expression must reuse the old value, since regardless of the new context the expression must
hold. If the new context is $\rootc$ we reuse the old value but require it to be hold. If the new context is $\rootc$ we reuse the old value but require it to be
$\true$ in $S$, and modify the hash table to record the expression appears at $\mzninline{true}$ in $S$, and modify the hash table to record the expression appears at
the root. If the expression appeared in a mixed context we simply reuse the old the root. If the expression appeared in a mixed context we simply reuse the old
result since this is the most constrained context. Similarly if the previous result since this is the most constrained context. Similarly if the previous
context is the same as the current one we reuse the old result. In the remaining context is the same as the current one we reuse the old result. In the remaining
@ -683,7 +689,7 @@ expression using function \textsf{flatlet} which returns the extracted
constraint and a rewritten term (not used in this case, but used in \flatt{}). constraint and a rewritten term (not used in this case, but used in \flatt{}).
The constraints returned by function \textsf{flatlet} are then flattened. The constraints returned by function \textsf{flatlet} are then flattened.
Finally if we are in the root context, we ensure that the Boolean $b$ returned Finally if we are in the root context, we ensure that the Boolean $b$ returned
must be $\true$ by adding $b$ to $S$. must be $\mzninline{true}$ by adding $b$ to $S$.
{ {
\begin{tabbing} \begin{tabbing}
@ -701,8 +707,8 @@ $\tuple{h,\rootc}$; \textbf{return} $h$
\> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\ \> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\
\> \textbf{else} \\ \> \textbf{else} \\
\> \> \textbf{switch} $c$ \\ \> \> \textbf{switch} $c$ \\
%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ %\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ %\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
\> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\ \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\ \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\
\>\>\> $\tuple{v_1, b_1}$ := $\flatt(t_1,\ctxt)$; \>\>\> $\tuple{v_1, b_1}$ := $\flatt(t_1,\ctxt)$;
@ -739,7 +745,7 @@ $S$ \cupp $\{ \new b \full (\flatc(c_1,\mix) \full
%\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'),
%b'' \full v \in \{1,..,n\} \} $ \\ %b'' \full v \in \{1,..,n\} \} $ \\
\>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\texttt{element}(v', [b_1, \ldots, b_n], \>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\texttt{element}(v', [b_1, \ldots, b_n],
\true)\}$; $b$ := $\true$ \\ \mzninline{true})\}$; $b$ := $\mzninline{true}$ \\
\>\>\> \textbf{else} \\ \>\>\> \textbf{else} \\
\>\>\>\> $S$ \cupp \>\>\>\> $S$ \cupp
$\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, $\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1,
@ -755,7 +761,7 @@ b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} $
\> \> \> \> \textbf{else} $S$ \cupp $\{ p\_reif(v_1,\ldots,v_n,\new b'), \> \> \> \> \textbf{else} $S$ \cupp $\{ p\_reif(v_1,\ldots,v_n,\new b'),
\new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}$ \\ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}$ \\
\> \> \> \textbf{else} \\ \> \> \> \textbf{else} \\
\>\> \> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j \>\> \> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
\}$ \}$
\\ \\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\ \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
@ -771,7 +777,7 @@ b_j\}$
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\ \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\
\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ \> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
\>\> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ \>\> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$
\\ \\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\ \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\ \>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
@ -886,7 +892,7 @@ $\flatt(t,\ctxt)$ flattens an integer term $t$ in context $\ctxt$. It returns a
tuple $\tuple{v,b}$ of an integer variable/value $v$ and a Boolean literal $b$, tuple $\tuple{v,b}$ of an integer variable/value $v$ and a Boolean literal $b$,
and as a side effect adds constraints to $S$ so that and as a side effect adds constraints to $S$ so that
$S \models b \full (v = t)$. Note that again flattening in the root context $S \models b \full (v = t)$. Note that again flattening in the root context
always returns a Boolean $b$ made equivalent to $\true$ by the constraints in always returns a Boolean $b$ made equivalent to $\mzninline{true}$ by the constraints in
$S$. $S$.
Flattening first checks if the same expression has been flattened previously and Flattening first checks if the same expression has been flattened previously and
@ -936,13 +942,13 @@ $\tuple{h,b',\rootc}$; \textbf{return} $\tuple{h,b'}$
\>\> \textbf{if} ($prev = \mix \vee prev = \ctxt$) \>\> \textbf{if} ($prev = \mix \vee prev = \ctxt$)
\textbf{return} $\tuple{h,b'}$ \\ \textbf{return} $\tuple{h,b'}$ \\
\>\> $\ctxt$ := $\mix$ \\ \>\> $\ctxt$ := $\mix$ \\
\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\ \> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\mzninline{true}$ \\
\> \textbf{else} %\\ \> \textbf{else} %\\
%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ %% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
%\> \> %\> \>
\textbf{switch} $t$ \\ \textbf{switch} $t$ \\
%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\ %\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\
\> \> \textbf{case} $v'$ (\syntax{<ivar>}): $v$ := $v'$; $b$ := $\true$\\ \> \> \textbf{case} $v'$ (\syntax{<ivar>}): $v$ := $v'$; $b$ := $\mzninline{true}$\\
\> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\ \> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\
\> \> \> \> \> \>
$\tuple{v_1,b_1}$ := $\flatt(t_1,\ctxt)$; $\tuple{v_1,b_1}$ := $\flatt(t_1,\ctxt)$;
@ -1035,14 +1041,16 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
\> \textbf{return} $\tuple{v,b}$ \> \textbf{return} $\tuple{v,b}$
\end{tabbing} \end{tabbing}
\begin{example}\label{ex:flat} \begin{example}\label{ex:hr-flat}
Consider the flattening of the expression Consider the flattening of the expression
$$ $$
a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee
(a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b)) (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b))
$$ $$
The different terms and subterms of the expression are
illustrated and numbered in Figure~\ref{fig:tree}. The different terms and subterms of the expression are illustrated and
numbered in \cref{fig:hr-tree}.
\begin{figure}[t] \begin{figure}[t]
$$ $$
\xymatrix@R=1em@C=0.6em{ \xymatrix@R=1em@C=0.6em{
@ -1060,7 +1068,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
} }
$$ $$
\caption{An expression to be flattened with non-leaf (sub-)terms \caption{An expression to be flattened with non-leaf (sub-)terms
numbered.\label{fig:tree}} numbered.\label{fig:hr-tree}}
\end{figure} \end{figure}
Note that positions 0 is in the $\rootc$ context, while position 10 is in a Note that positions 0 is in the $\rootc$ context, while position 10 is in a
$\negc$ context, positions 13 and 15 are in a $\mix$ context, and the rest are $\negc$ context, positions 13 and 15 are in a $\mix$ context, and the rest are
@ -1171,7 +1179,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
% The pseudo-code for \flatc($b$,$c$) flattens a constraint expression $c$ to be % The pseudo-code for \flatc($b$,$c$) flattens a constraint expression $c$ to be
% equal to $b$, returning a set of constraints implementing $b \full c$. We % equal to $b$, returning a set of constraints implementing $b \full c$. We
% flatten a whole model $c$ using $\flatc(\true, c)$. In the pseudo-code the % flatten a whole model $c$ using $\flatc(\mzninline{true}, c)$. In the pseudo-code the
% expressions $\new b$ and $\new v$ create a new Boolean and integer variable % expressions $\new b$ and $\new v$ create a new Boolean and integer variable
% respectively. % respectively.
@ -1193,8 +1201,8 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
% \> \textbf{case} \texttt{not} $c_1$: % \> \textbf{case} \texttt{not} $c_1$:
% \textbf{return} $\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}$ \\ % \textbf{return} $\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}$ \\
% \> \textbf{case} $c_1$ \verb+/\+ $c_2$: \= % \> \textbf{case} $c_1$ \verb+/\+ $c_2$: \=
% \textbf{if} ($b \equiv \true$) \textbf{return} $\flatc(\true, c_1) \cup % \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $\flatc(\mzninline{true}, c_1) \cup
% \flatc(\true, c_2)$ \\ % \flatc(\mzninline{true}, c_2)$ \\
% \> \> \textbf{else} \textbf{return} $\flatc(\new b_1, c_1) \cup % \> \> \textbf{else} \textbf{return} $\flatc(\new b_1, c_1) \cup
% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}$ \\ % \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}$ \\
% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill % xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
@ -1208,7 +1216,7 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$
% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full % \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full
% b_2)\}$ \\ % b_2)\}$ \\
% \> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): \\ % \> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): \\
% \> \> \textbf{if} ($b \equiv \true$) \textbf{return} $\safen(b, % \> \> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $\safen(b,
% \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}$ \\ % \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}$ \\
% \> \> \textbf{else} \textbf{abort} % \> \> \textbf{else} \textbf{abort}
% \end{tabbing} % \end{tabbing}
@ -1237,21 +1245,22 @@ The procedure \safen($b, C$) enforces the relational semantics for unsafe
expressions, by ensuring that the unsafe relational versions of partial expressions, by ensuring that the unsafe relational versions of partial
functions are made safe. Note that to implement the \emph{strict semantics} as functions are made safe. Note that to implement the \emph{strict semantics} as
opposed to the relational semantics we just need to define $\safen(b,C) = C$. If opposed to the relational semantics we just need to define $\safen(b,C) = C$. If
$b \equiv \true$ then the relational semantics and the strict semantics $b \equiv \mzninline{true}$ then the relational semantics and the strict semantics
coincide, so nothing needs to be done. The same is true if the set of coincide, so nothing needs to be done. The same is true if the set of
constraints $C$ is safe. For $div(x,y,z)$, the translation introduces a new constraints $C$ is safe. For $div(x,y,z)$, the translation introduces a new
variable $y'$ which cannot be 0, and equates it to $y$ if $y \neq 0$. The variable $y'$ which cannot be 0, and equates it to $y$ if $y \neq 0$. The
constraint $div(x,y',z)$ never reflects a partial function application. The new constraint $div(x,y',z)$ never reflects a partial function application. The new
variable $b'$ captures whether the partial function application returns a non variable $b'$ captures whether the partial function application returns a non
$\bot$ value. For $\element(v,a,x)$, it introduces a new variable $v'$ which $\bot$ value. For \mzninline{element(v, a, x)}, it introduces a new variable $v'$
only takes values in $\dom(a)$ and forces it to equal $v$ if $v \in \dom(a)$. A which only takes values in $\dom(a)$ and forces it to equal $v$ if
partial function application forces $b = \false$ since it is the conjunction of $v \in \dom(a)$. A partial function application forces $b = \mzninline{false}$ since it is
the new variables $b'$. The \%HALF\% comments will be explained later. the conjunction of the new variables $b'$. The \%HALF\% comments will be
explained later.
\begin{tabbing} \begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\safen($b$,$C$) \\ \safen($b$,$C$) \\
\> \textbf{if} ($b \equiv \true$) \textbf{return} $C$ \\ \> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $C$ \\
\> \textbf{if} ($C$ is a set of safe constraints) \textbf{return} $C$ \\ \> \textbf{if} ($C$ is a set of safe constraints) \textbf{return} $C$ \\
\> $B$ := $\emptyset$; $S$ := $\emptyset$ \\ \> $B$ := $\emptyset$; $S$ := $\emptyset$ \\
\> \textbf{foreach} $c \in C$ \\ \> \textbf{foreach} $c \in C$ \\
@ -1261,13 +1270,13 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
= y', div(x,y',z) \}$ \\ = y', div(x,y',z) \}$ \\
\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full y \neq 0, b' \half \> \> \> \%HALF\% $S$ := $S \cup \{ b' \full y \neq 0, b' \half
div(x,y,z)\}$ \\ div(x,y,z)\}$ \\
\> \> \textbf{else if} $c \equiv \element(v,a,x)$ and $v$ can take a value outside the domain of $a$) \\ \> \> \textbf{else if} \(c \equiv \mzninline{element(v, a, x)}\) and $v$ can take a value outside the domain of $a$) \\
\> \> \> $B$ := $B \cup \{ \new b' \}$ \\ \> \> \> $B$ := $B \cup \{ \new b' \}$ \\
\> \> \> $S$ := $S \cup \{ \new v' \in \dom(a), \> \> \> $S$ := $S \cup \{ \new v' \in \dom(a),
b' \full v \in \dom(a), b' \full v = v', b' \full v \in \dom(a), b' \full v = v',
\element(v',a,x)\}$ \\ \mzninline{element(v', a, x)}\}$ \\
\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half \> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half
\element(v,a,x)\}$ \\ \mzninline{element(v, a, x)}\}$ \\
\> \> \textbf{else} $S$ := $S \cup \{c\}$ \\ \> \> \textbf{else} $S$ := $S \cup \{c\}$ \\
\> \> \textbf{return} $S \cup \{b \full \wedge_{b' \in B} b' \> \> \textbf{return} $S \cup \{b \full \wedge_{b' \in B} b'
\})$ \})$
@ -1279,7 +1288,7 @@ renamed-apart copies of already-generated constraints, but for simplicity of
presentation, we omit the algorithms we use to do this. presentation, we omit the algorithms we use to do this.
\section{Half Reification} \section{Half Reification}
\label{sec:halfreif} \label{sec:hr-halfreif}
Given a constraint $c$, the \emph{half-reified version} of $c$ is a constraint Given a constraint $c$, the \emph{half-reified version} of $c$ is a constraint
of the form $b \half c$ where $b \not\in vars(c)$ is a Boolean variable. of the form $b \half c$ where $b \not\in vars(c)$ is a Boolean variable.
@ -1288,11 +1297,11 @@ We can construct a propagator $f_{b \half c}$ for the half-reified version of
$c$, $b \half c$, using the propagator $f_c$ for $c$. $c$, $b \half c$, using the propagator $f_c$ for $c$.
$$ $$
\begin{array}{rcll} \begin{array}{rcll}
f_{b \half c}(D)(b) & = & \{ \false \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\ f_{b \half c}(D)(b) & = & \{ \mzninline{false} \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\
f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\ f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\
f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \false \in D(b) \\ f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \mzninline{false} \in D(b) \\
f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c) f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c)
\text{~and~} \false \not\in D(b) \text{~and~} \mzninline{false} \not\in D(b)
\end{array} \end{array}
$$ $$
@ -1325,27 +1334,28 @@ $$
% Given this separation we can improve the definition of $f_{b \half c}$ above by % Given this separation we can improve the definition of $f_{b \half c}$ above by
% replacing the check ``$f_c(D)$ is a false domain'' by ``$f_{check(c)}(D)$ is a % replacing the check ``$f_c(D)$ is a false domain'' by ``$f_{check(c)}(D)$ is a
% false domain''. In practice it means that the half-reified propagator can be % false domain''. In practice it means that the half-reified propagator can be
% implemented to only perform the checking part until $D(b) = \{\true\}$, when it % implemented to only perform the checking part until $D(b) = \{\mzninline{true}\}$, when it
% needs to perform both. % needs to perform both.
In practice most propagator implementations for $c$ first check whether $c$ is In practice most propagator implementations for \mzninline{c} first check
satisfiable, before continuing to propagate. For example, whether \mzninline{c} is satisfiable, before continuing to propagate. For
$\sum_i a_i x_i \leq a_0$ determines $L = \sum_i min_D(a_i x_i) - a_0$ and fails example, \mzninline{sum(i in N)(a[i] * x[i]) <= C} determines \mzninline{L =
if $L > 0$ before propagating; Regin's domain propagator for sum(i in N)(lb(a[i] * x[i])) - C} and fails if \mzninline{L > 0} before
\alldiff$([x_1, \ldots, x_n]$) determines a maximum matching between variables propagating; Regin's domain propagator for \mzninline{all_different(X)}
and values first, if this is not of size $n$ it fails before propagating; the determines a maximum matching between variables and values first, if this is not
timetable \texttt{cumulative} constraint determines a profile of necessary of size \mzninline{length(X)} it fails before propagating; the timetable
resource usage, and fails if this breaks the resource limit, before considering \texttt{cumulative} constraint determines a profile of necessary resource usage,
propagation. We can implement the propagator for $f_{b \half c}$ by only and fails if this breaks the resource limit, before considering propagation. We
performing the checking part until $D(b) = \{\true\}$. can implement the propagator for $f_{\mzninline{b -> c}}$ by only performing the
checking part until $D(\texttt{b}) = \{\mzninline{true}\}$.
Half reification naturally encodes the relational semantics for partial function Half reification naturally encodes the relational semantics for partial function
applications in positive contexts. We associate a Boolean variable $b$ with each applications in positive contexts. We associate a Boolean variable \texttt{b} with each
Boolean term in an expression, and we ensure that all unsafe constraints are Boolean term in an expression, and we ensure that all unsafe constraints are
half-reified using the variable of the nearest enclosing Boolean term. half-reified using the variable of the nearest enclosing Boolean term.
\begin{example} \begin{example}
Consider flattening of the constraint of \cref{ex:cons}. First we will convert Consider flattening of the constraint of \cref{ex:hr-cons}. First we will convert
it to an equivalent expression with only positive contexts it to an equivalent expression with only positive contexts
\begin{mzn} \begin{mzn}
@ -1364,10 +1374,10 @@ half-reified using the variable of the nearest enclosing Boolean term.
constraint b1 \/ b2; constraint b1 \/ b2;
\end{mzn} \end{mzn}
The unsafe $\element$ constraint is half reified with the name of its nearest The unsafe \mzninline{element} constraint is half reified with the name of its nearest
enclosing Boolean term. Note that if $i = 7$ then the second constraint makes enclosing Boolean term. Note that if $i = 7$ then the second constraint makes
$b2 = \false$. Given this, the final constraint requires $b1 = \true$, which $b2 = \mzninline{false}$. Given this, the final constraint requires $b1 = \mzninline{true}$, which
in turn requires $i > 4$. Since this holds, the whole constraint is $\true$ in turn requires $i > 4$. Since this holds, the whole constraint is $\mzninline{true}$
with no restrictions on $x$. with no restrictions on $x$.
\end{example} \end{example}
@ -1376,7 +1386,7 @@ assume that each global constraint predicate $p$ is available in half-reified
form. Recall that this places no new burden on the solver implementer. form. Recall that this places no new burden on the solver implementer.
\begin{example} \begin{example}
Consider the constraint of \cref{ex:alldiff}. Half reification results in Consider the constraint of \cref{ex:hr-alldiff}. Half reification results in
\begin{mzn} \begin{mzn}
constraint b1 -> i > 4; constraint b1 -> i > 4;
@ -1385,14 +1395,15 @@ form. Recall that this places no new burden on the solver implementer.
constraint b1 \/ b2 % b1 or b2 constraint b1 \/ b2 % b1 or b2
\end{mzn} \end{mzn}
We can easily modify any existing propagator for \alldiff to support the We can easily modify any existing propagator for \mzninline{all_different} to
half-reified form, hence this model is executable by our constraint solver. support the half-reified form, hence this model is executable by our
constraint solver.
\end{example} \end{example}
Half reification can lead to more efficient constraint solving, since it does Half reification can lead to more efficient constraint solving, since it does
not propagate unnecessarily. not propagate unnecessarily.
\begin{example}\label{ex:cumul} \begin{example}\label{ex:hr-cumul}
Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\ Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\
\autocite{schutt-2009-cumulative}) which includes constraints of the form \autocite{schutt-2009-cumulative}) which includes constraints of the form
@ -1415,7 +1426,7 @@ not propagate unnecessarily.
\end{mzn} \end{mzn}
Whenever the start time of task $i$ is constrained so that it does not overlap Whenever the start time of task $i$ is constrained so that it does not overlap
time $s[j]$, then $b3[i]$ is fixed to $\false$ and $a[i]$ to 0, and the long time $s[j]$, then $b3[i]$ is fixed to $\mzninline{false}$ and $a[i]$ to 0, and the long
linear sum is awoken. But this is useless, since it cannot cause failure. linear sum is awoken. But this is useless, since it cannot cause failure.
% Half-reification of this expression which appears in a negative context produces % Half-reification of this expression which appears in a negative context produces
@ -1442,7 +1453,7 @@ not propagate unnecessarily.
\pjs{Add linearization example here!} \pjs{Add linearization example here!}
Half reification can cause propagators to wake up less frequently, since Half reification can cause propagators to wake up less frequently, since
variables that are fixed to $\true$ by full reification will never be fixed by variables that are fixed to $\mzninline{true}$ by full reification will never be fixed by
half reification. This is advantageous, but a corresponding disadvantage is that half reification. This is advantageous, but a corresponding disadvantage is that
variables that are fixed can allow the simplification of the propagator, and variables that are fixed can allow the simplification of the propagator, and
hence make its propagation faster. We can reduce this disadvantage by fully hence make its propagation faster. We can reduce this disadvantage by fully
@ -1463,7 +1474,7 @@ rewriting used with full reification.
The procedure $\halfc(b,c)$ defined below returns a set of constraints The procedure $\halfc(b,c)$ defined below returns a set of constraints
implementing the half-reification $b \half c$. We flatten a constraint item implementing the half-reification $b \half c$. We flatten a constraint item
$\texttt{constraint}~c$ using $\halfc(\true, c)$. The half-reification $\texttt{constraint}~c$ using $\halfc(\mzninline{true}, c)$. The half-reification
flattening transformation uses half reification whenever it is in a positive flattening transformation uses half reification whenever it is in a positive
context. If it encounters a constraint $c_1$ in a negative context, it negates context. If it encounters a constraint $c_1$ in a negative context, it negates
the constraint if it is safe, thus creating a new positive context. If this is the constraint if it is safe, thus creating a new positive context. If this is
@ -1541,8 +1552,8 @@ $\tuple{h,\rootc}$; \textbf{return} $h$
\> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\ \> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\
\> \textbf{else} \\ \> \textbf{else} \\
\> \> \textbf{switch} $c$ \\ \> \> \textbf{switch} $c$ \\
%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ %\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ %\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
\> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\ \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $b$ := $b'$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\ \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\
\> \> \> \textbf{switch} $r$ \\ \> \> \> \textbf{switch} $r$ \\
@ -1586,7 +1597,7 @@ $S$ \cupp $\{ \new b \half (\flatc(c_1,\mix) \full
%\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'),
%b'' \full v \in \{1,..,n\} \} $ \\ %b'' \full v \in \{1,..,n\} \} $ \\
\>\>\> \textbf{if} ($\ctxt = \rootc$) \>\>\> \textbf{if} ($\ctxt = \rootc$)
$S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \true), \new b\}$ \\ $S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}$ \\
\>\>\> \textbf{else} \>\>\> \textbf{else}
$S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half $S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half
\texttt{element}(v, [b_1, \ldots, b_n], b') \}$ \\ \texttt{element}(v, [b_1, \ldots, b_n], b') \}$ \\
@ -1601,7 +1612,7 @@ $S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ :=
$\halft(t_j,\ctxt,\iboth)$; \\ $\halft(t_j,\ctxt,\iboth)$; \\
\> \> \> \textbf{if} ($\ctxt = \rootc$) \> \> \> \textbf{if} ($\ctxt = \rootc$)
$b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
\}$ \}$
\\ \\
\>\>\> \textbf{else} %($\ctxt = \pos$) \\ \> \> \> \> \>\>\> \textbf{else} %($\ctxt = \pos$) \\ \> \> \> \>
@ -1626,7 +1637,7 @@ b_j\}$
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\ \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}) built-in predicate: \\
\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ \> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ \> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
\>\> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ \>\> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$
\\ \\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\ \>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{<pred>}): user-defined predicate \\
\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\ \>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
@ -1689,8 +1700,8 @@ $\tuple{h,\rootc}$; \textbf{return} $h$\\
\> \textbf{if} ($\fixed(c)$) $b$ := $\neg \eval(c)$ \\ \> \textbf{if} ($\fixed(c)$) $b$ := $\neg \eval(c)$ \\
\> \textbf{else} \\ \> \textbf{else} \\
\> \> \textbf{switch} $c$ \\ \> \> \textbf{switch} $c$ \\
%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ %\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ %\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\
\> \> \textbf{case} $b'$ (\syntax{<bvar>}): $S$ \cupp $\{\new b \half \neg b'\}$; \\ \> \> \textbf{case} $b'$ (\syntax{<bvar>}): $S$ \cupp $\{\new b \half \neg b'\}$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\ \> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{<relop>}): \\
\> \> \> \textbf{if} ($t_1$ and $t_2$ are safe) \\ \> \> \> \textbf{if} ($t_1$ and $t_2$ are safe) \\
@ -1786,7 +1797,7 @@ bounds. If the previous context was root or the context are the same we examine
the bounds. If they are the same we reuse the result, otherwise we set the the bounds. If they are the same we reuse the result, otherwise we set the
$\bnds$ to $\iboth$ and reflatten since we require both bounds (perhaps in $\bnds$ to $\iboth$ and reflatten since we require both bounds (perhaps in
different situations). Otherwise the new context is $\rootc$ and the previous different situations). Otherwise the new context is $\rootc$ and the previous
$\pos$, we force $b'$ to be $\true$ in $S$, and then reuse the result if the $\pos$, we force $b'$ to be $\mzninline{true}$ in $S$, and then reuse the result if the
bounds are the same, or set $\bnds$ to $\iboth$ and reflatten. We store the bounds are the same, or set $\bnds$ to $\iboth$ and reflatten. We store the
result found at the end of flattening, note that we only need one entry: context result found at the end of flattening, note that we only need one entry: context
can move from $\pos$ to $\rootc$ and bounds can move from one of $\iabove$ or can move from $\pos$ to $\rootc$ and bounds can move from one of $\iabove$ or
@ -1853,13 +1864,13 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\> \> \> \textbf{if} ($pbnds = \bnds$) hhash[$t$] := $\tuple{h,b',\rootc,\bnds}$; \textbf{return} $\tuple{h,b'}$ \> \> \> \textbf{if} ($pbnds = \bnds$) hhash[$t$] := $\tuple{h,b',\rootc,\bnds}$; \textbf{return} $\tuple{h,b'}$
\\ \\
\> \> \> \textbf{else} $\bnds$ := $\iboth$ \\ \> \> \> \textbf{else} $\bnds$ := $\iboth$ \\
\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\ \> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\mzninline{true}$ \\
\> \textbf{else} %\\ \> \textbf{else} %\\
%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ %% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
%\> \> %\> \>
\textbf{switch} $t$ \\ \textbf{switch} $t$ \\
%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\ %\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\
\> \> \textbf{case} $v'$ (\syntax{<ivar>}): $v$ := $v'$; $b$ := $\true$\\ \> \> \textbf{case} $v'$ (\syntax{<ivar>}): $v$ := $v'$; $b$ := $\mzninline{true}$\\
\> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\ \> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{<arithop>}): \\
\> \> \> \textbf{switch} $a$ \\ \> \> \> \textbf{switch} $a$ \\
\> \> \> \textbf{case} $+$: \> \> \> \textbf{case} $+$:
@ -1957,8 +1968,8 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$
% context, negates $c_1$ and half-reifies the result if $c_1$ is safe and in a % context, negates $c_1$ and half-reifies the result if $c_1$ is safe and in a
% negative context, and uses full flattening otherwise. % negative context, and uses full flattening otherwise.
\begin{example}\label{ex:half} \begin{example}\label{ex:hr-half}
Now lets consider half reifying the expression of \cref{ex:flat}. Now lets consider half reifying the expression of \cref{ex:hr-flat}.
The result of flattening with half reification is: The result of flattening with half reification is:
@ -2029,7 +2040,7 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$
transformation will construct many implications of the form $b \half b'$, note transformation will construct many implications of the form $b \half b'$, note
that the constraint $b \half b_1 \wedge \cdots \wedge b_n$ is equivalent to that the constraint $b \half b_1 \wedge \cdots \wedge b_n$ is equivalent to
$b \half b_1, b \half b_2, \ldots, b \half b_n$. Just as in $b \half b_1, b \half b_2, \ldots, b \half b_n$. Just as in
Example~\ref{ex:half} above we can simplify the result of half reification. For \cref{ex:hr-half} above we can simplify the result of half reification. For
each $b'$ which appears only on the right of one constraint of the form each $b'$ which appears only on the right of one constraint of the form
$b \half b'$ and other constraints of the form $b' \half c_i$ we remove the $b \half b'$ and other constraints of the form $b' \half c_i$ we remove the
first constraint and replace the others by $b \half c_i$. first constraint and replace the others by $b \half c_i$.
@ -2047,17 +2058,17 @@ To do so independent of propagation strength, we define the behaviour of the
propagators of the half-reified forms in terms of the full reified propagator. propagators of the half-reified forms in terms of the full reified propagator.
$$ $$
\begin{array}{rcll} \begin{array}{rcll}
f_{b \half c}(D)(b) & = & D(b) \cap ( \{ \false \} \cup f_{b \full c}(D)(b)) \\ f_{b \half c}(D)(b) & = & D(b) \cap ( \{ \mzninline{false} \} \cup f_{b \full c}(D)(b)) \\
f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\false \in D(b) \\ f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b) \\
f_{b \half c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise} f_{b \half c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
\end{array} \end{array}
$$ $$
and and
$$ $$
\begin{array}{rcll} \begin{array}{rcll}
f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \false \} \in f_{b \full c}(D)(b) \\ f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \mzninline{false} \} \in f_{b \full c}(D)(b) \\
f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \false\} & \text{otherwise}\\ f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \mzninline{false}\} & \text{otherwise}\\
f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\false \in D(b') \\ f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b') \\
f_{b' \half \neg c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise} f_{b' \half \neg c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
\end{array} \end{array}
$$ $$
@ -2067,7 +2078,7 @@ half reified split versions of the propagator should act.
In order to prove the same behaviour of the split reification versions we must In order to prove the same behaviour of the split reification versions we must
assume that $f_{b \full c}$ is \emph{reified-consistent} which is defined as assume that $f_{b \full c}$ is \emph{reified-consistent} which is defined as
follows: suppose $f_{b \full c}(D)(v) \neq D(v), v \not\equiv b$, then follows: suppose $f_{b \full c}(D)(v) \neq D(v), v \not\equiv b$, then
$f_{b \full c}(D)(b) \neq \{ \false, \true\}$. That is if the propagator ever $f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true}\}$. That is if the propagator ever
reduces the domain of some variable, then it must also fix the Boolean variable reduces the domain of some variable, then it must also fix the Boolean variable
$b$. This is sensible since if $b$ is not fixed then every possible value of $v$ $b$. This is sensible since if $b$ is not fixed then every possible value of $v$
is consistent with constraint $b \full c$ regardless of the domain $D$. This is is consistent with constraint $b \full c$ regardless of the domain $D$. This is
@ -2105,14 +2116,14 @@ the usual case for such a trivial propagator.
% $D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$. % $D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$.
% The proof is by cases of $D$. % The proof is by cases of $D$.
% \textbf{(a)} Suppose $D(b) = \{\true,\false\}$. \textbf{(a-i)} Suppose % \textbf{(a)} Suppose $D(b) = \{\mzninline{true},\mzninline{false}\}$. \textbf{(a-i)} Suppose
% $f_{b \full c}(D) = D$. Then clearly $f_{b \half c}(D) = D$ by definition, and % $f_{b \full c}(D) = D$. Then clearly $f_{b \half c}(D) = D$ by definition, and
% similarly $f_{b' \half \neg c}(D) = D$. Hence $D_1 = D_2 = D$. Note that since % similarly $f_{b' \half \neg c}(D) = D$. Hence $D_1 = D_2 = D$. Note that since
% $f_{b \full c}$ is reified consistent, then $f_{b \full c}(D) \neq D$ implies % $f_{b \full c}$ is reified consistent, then $f_{b \full c}(D) \neq D$ implies
% that $f_{b \full c}(D)(b) \neq \{ \false, \true \}$. \textbf{(a-ii)} Suppose % that $f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}$. \textbf{(a-ii)} Suppose
% $f_{b \full c}(D)(b) = \{ \true \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then % $f_{b \full c}(D)(b) = \{ \mzninline{true} \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then
% $D_1(b') = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$. % $D_1(b') = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$.
% Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \true \}$ and % Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \mzninline{true} \}$ and
% $D_2(v) = D(v), v \not\in \{b,b'\}$. Then % $D_2(v) = D(v), v \not\in \{b,b'\}$. Then
% $D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)$ by definition, and by % $D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)$ by definition, and by
% idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and % idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and
@ -2121,9 +2132,9 @@ the usual case for such a trivial propagator.
% $f_{b \half c}$, $f_{b' \full \neg b}$ and $f_{b' \half \neg c}$ and hence % $f_{b \half c}$, $f_{b' \full \neg b}$ and $f_{b' \half \neg c}$ and hence
% $D'' = D_3$. But also $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since % $D'' = D_3$. But also $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since
% $D_3$ and $f_{b \full c}(D)$ only differ on $b'$. \textbf{(a-iii)} Suppose % $D_3$ and $f_{b \full c}(D)$ only differ on $b'$. \textbf{(a-iii)} Suppose
% $f_{b \full c}(D)(b) = \{ \false \}$. Let $D_1 = f_{b \half c}(D)$, then % $f_{b \full c}(D)(b) = \{ \mzninline{false} \}$. Let $D_1 = f_{b \half c}(D)$, then
% $D_1(b) = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let % $D_1(b) = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let
% $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \true \}$ and % $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \mzninline{true} \}$ and
% $D_2(v) = D(v), v \not\in \{b,b'\}$. Then % $D_2(v) = D(v), v \not\in \{b,b'\}$. Then
% $D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)$ by definition, and by % $D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)$ by definition, and by
% idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and % idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and
@ -2132,10 +2143,10 @@ the usual case for such a trivial propagator.
% $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since $D_3$ and % $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since $D_3$ and
% $f_{b \full c}(D)$ only differ on $b'$. % $f_{b \full c}(D)$ only differ on $b'$.
% \textbf{(b)} If $D(b) = \{\true\}$ then clearly $f_{b \full c}$ and % \textbf{(b)} If $D(b) = \{\mzninline{true}\}$ then clearly $f_{b \full c}$ and
% $f_{b \half c}$ act identically on variables in $vars(c)$. % $f_{b \half c}$ act identically on variables in $vars(c)$.
% \textbf{(c)} If $D(b) = \{\false\}$ then $D(b') = \{\true\}$ and clearly % \textbf{(c)} If $D(b) = \{\mzninline{false}\}$ then $D(b') = \{\mzninline{true}\}$ and clearly
% $f_{b \full c}$ and $f_{b' \half \neg c}$ act identically on variables in % $f_{b \full c}$ and $f_{b' \half \neg c}$ act identically on variables in
% $vars(c)$. \qed % $vars(c)$. \qed
% \end{proof} % \end{proof}
@ -2181,7 +2192,7 @@ still fixed at the same time, but there is less overhead.
Implementing half-reification within the \minizinc\ distribution consists of two Implementing half-reification within the \minizinc\ distribution consists of two
parts: the \minizinc\ compiler needs to be extended with an implementation of parts: the \minizinc\ compiler needs to be extended with an implementation of
the half-reification flattening algorithm as described in \cref{sec:halfreif} the half-reification flattening algorithm as described in \cref{sec:hr-halfreif}
and for any target solver that supports half-reification its library needs to be and for any target solver that supports half-reification its library needs to be
appended with definitions for the predicates that are half-reified. Because the appended with definitions for the predicates that are half-reified. Because the
\minizinc\ language allows for the definition of new predicates, we allow any \minizinc\ language allows for the definition of new predicates, we allow any
@ -2220,35 +2231,34 @@ has propagators for half-reified constraints we have declared the corresponding
predicates as solver builtins. Gecode provides half-reified propagators for predicates as solver builtins. Gecode provides half-reified propagators for
almost all \flatzinc\ builtins. The other targeted solvers use the linear almost all \flatzinc\ builtins. The other targeted solvers use the linear
library. The linear library \jip{,as seen before + reference???,} already has library. The linear library \jip{,as seen before + reference???,} already has
redefinition for their fully reified predicates, \(b \full c\). These generally redefinition for their fully reified predicates, \mzninline{b <-> c}. These
consist of two parts which are equivalent to the implications generally consist of two parts which are equivalent to the implications
\(b \half c \land \lnot b \half \lnot c \). Because of this, the implementations \mzninline{b -> c /\ not b -> not c}. Because of this, the implementations of
of the half-reified version of the same predicates usually consist of using only the half-reified version of the same predicates usually consist of using only
one of these two parts, which will eliminate the need of many constraints. We one of these two parts, which will eliminate the need of many constraints. We
added half-reified versions for all predicates for which a full reification was added half-reified versions for all predicates for which a full reification was
provided. provided.
\subsection{Implication Chain Compression} \subsection{Implication Chain Compression}
As shown in \cref{ex:half}, flattening with half reification will in many cases As shown in \cref{ex:hr-half}, flattening with half reification will in many
result in implication chains: \((b \half b') \land (b' \half c)\), where \(b'\) cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where
has no other occurrences. In this case the conjunction can be replaced by \texttt{b2} has no other occurrences. In this case the conjunction can be
\(b \half c\) and \(b'\) can be removed from the model. The case shown in the replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the model.
example can be generalised to The case shown in the example can be generalised to \mzninline{b1 -> b2 /\
\((b \half b') \land \left(\forall_{i \in N} b' \half c_i \right)\), which, if forall(i in N)(b2 -> c[i])}, which, if \texttt{b2} has no other usage in the
\(b'\) has no other usage in the instance, can be resolved to instance, can be resolved to \mzninline{forall(i in N)(b1 -> c[i])} after which
\(\forall_{i \in N} b \half c_i\) after which \(b'\) can be removed from the \texttt{b1} can be removed from the model.
model.
An algorithm to remove these chains of implications is best visualised through 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 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 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 and an edge \(\tuple{x,y} \in E\) represents the presence of an implication
\(x \half y\) in the instance. Additionally, for the benefit of the algorithm, a \mzninline{x -> y} in the instance. Additionally, for the benefit of the
vertex is marked when it is used in other constraints in the constraint model. algorithm, a vertex is marked when it is used in other constraints in the
The goal of the algorithm is now to identify and remove vertices that are not constraint model. The goal of the algorithm is now to identify and remove
marked and have only one incoming edge. The following pseudo code provides a vertices that are not marked and have only one incoming edge. The following
formal specification for this algorithm. pseudo code provides a formal specification for this algorithm.
\newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~} \newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~}
\begin{tabbing} \begin{tabbing}
@ -2266,12 +2276,12 @@ formal specification for this algorithm.
\jip{Here we could actually show an example using a drawn graph} \jip{Here we could actually show an example using a drawn graph}
The algorithm can be further improved by considering implied conjunctions. These The algorithm can be further improved by considering implied conjunctions. These
can be split up into multiple implications: \(b' \half \forall_{i \in N} b_i\) can be split up into multiple implications: \mzninline{b -> forall(i in
is equivalent to \(\forall_{i \in N} (b' \half b_i)\). This transformation both N)(bs[i])} is equivalent to \mzninline{forall(i in N)(b -> bs[i])}. This
simplifies a complicated constraint and possibly allows for the further transformation both simplifies a complicated constraint and possibly allows for
compression of implication chains. It should however be noted that although this the further compression of implication chains. It should however be noted that
transformation can result in an increase in the number of constraints, it although this transformation can result in an increase in the number of
generally increases the propagation efficiency. constraints, it generally increases the propagation efficiency.
To adjust the algorithm to simplify implied conjunctions more introspection from 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 the \minizinc\ compiler is required. The compiler must be able to tell if a
@ -2289,8 +2299,8 @@ available \jip{Insert new link} has our experimental \minizinc\ instances and
the infrastructure that performs the benchmarks. the infrastructure that performs the benchmarks.
The first experiment considers ``QCP-max'' problems which are defined as The first experiment considers ``QCP-max'' problems which are defined as
quasi-group completion problems where the \alldiff constraints are soft, and the quasi-group completion problems where the \mzninline{all_different} constraints
aim is to satisfy as many of them as possible. are soft, and the aim is to satisfy as many of them as possible.
\begin{mzn} \begin{mzn}
int: n; % size int: n; % size
@ -2308,20 +2318,21 @@ predicate all_different(array[int] of var int: x) =
forall(i,j in index_set(x) where i < j)(x[i] != x[j]); forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
\end{mzn} \end{mzn}
Note that this is not the same as requiring the maximum number of Note that this is not the same as requiring the maximum number of disequality
disequality constraints to be satisfied. The \alldiff constraints, while constraints to be satisfied. The \mzninline{all_different} constraints, while
apparently in a mixed context, are actually in a positive context, since the apparently in a mixed context, are actually in a positive context, since the
maximization in fact is implemented by inequalities forcing at least some number maximisation in fact is implemented by inequalities forcing at least some number
to be true. to be true.
In Table~\ref{tab:qcp} we compare three different resulting programs on QCP-max In \cref{tab:hr-qcp} we compare three different resulting programs on QCP-max
problems: full reification of the model above, using the \alldiff decomposition problems: full reification of the model above, using the
defined by the predicate shown (\textsf{full}), half reification of the model \mzninline{all_different} decomposition defined by the predicate shown
using the \alldiff decomposition (\textsf{half}), and half reification using a (\textsf{full}), half reification of the model using the
half-reified global \alldiff (\textsf{half-g}) implementing arc consistency \mzninline{all_different} decomposition (\textsf{half}), and half reification
(thus having the same propagation strength as the decomposition). \jip{is this using a half-reified global \mzninline{all_different} (\textsf{half-g})
still correct??} We use standard QCP examples from the literature, and group implementing arc consistency (thus having the same propagation strength as the
them by size. decomposition). \jip{is this still correct??} We use standard QCP examples from
the literature, and group them by size.
% and whether they are satisfiable or unsatisfiable as QCP problems. % and whether they are satisfiable or unsatisfiable as QCP problems.
We compare both a standard finite domain solver (FD) and a learning lazy clause We compare both a standard finite domain solver (FD) and a learning lazy clause
generation solver (FD + Explanations). We use the same fixed search strategy of generation solver (FD + Explanations). We use the same fixed search strategy of
@ -2329,7 +2340,7 @@ labeling the matrix in order left-to-right from highest to lowest value for all
approaches to minimize differences in search. approaches to minimize differences in search.
\begin{table} [tb] \begin{center} \begin{table} [tb] \begin{center}
\caption{\label{tab:qcp} QCP-max problems: \caption{\label{tab:hr-qcp} QCP-max problems:
Average time (in seconds), number of solved instances (300s timeout).} Average time (in seconds), number of solved instances (300s timeout).}
\begin{tabular}{|l||rr|rr|rr|} \begin{tabular}{|l||rr|rr|rr|}
\hline \hline
@ -2359,7 +2370,7 @@ The second experiment shows how half reification can reduce the overhead of
handling partial functions correctly. Consider the following model for handling partial functions correctly. Consider the following model for
determining a prize collecting path, a simplified form of prize collecting determining a prize collecting path, a simplified form of prize collecting
travelling salesman problem travelling salesman problem
\autocite{balas-1989-pctsp}, %shown in Figure~\ref{fig:pct} \autocite{balas-1989-pctsp}, %shown in \cref{fig:hr-pct}
where the aim is define an acyclic path from node 1 along weighted edges to where the aim is define an acyclic path from node 1 along weighted edges to
collect the most weight. Not every node needs to be visited ($pos[i] = 0$). collect the most weight. Not every node needs to be visited ($pos[i] = 0$).
@ -2382,12 +2393,12 @@ constraint alldifferent_except_0(next) /\ pos[1] = 1;
solve minimize sum(i in 1..n)(prize[i]); solve minimize sum(i in 1..n)(prize[i]);
\end{mzn} \end{mzn}
It uses the global constraint \texttt{alldifferent\_except\_0} which constrains It uses the global constraint \mzninline{alldifferent_except_0} which constrains
each element in the $next$ array to be different or equal 0. The model has one each element in the \mzninline{next} array to be different or equal 0. The model
unsafe array lookup $pos[next[i]]$. We compare using full reification has one unsafe array lookup \mzninline{pos[next[i]]}. We compare using full
(\textsf{full}) and half reification (\textsf{half}) to model this problem. Note reification (\textsf{full}) and half reification (\textsf{half}) to model this
that if we extend the $pos$ array to have domain $0..n$ then the model becomes problem. Note that if we extend the $pos$ array to have domain $0..n$ then the
safe, by replacing its definition with the following two lines model becomes safe, by replacing its definition with the following two lines
\begin{mzn} \begin{mzn}
array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin
@ -2397,18 +2408,18 @@ safe, by replacing its definition with the following two lines
We also compare against this model (\textsf{extended}). We also compare against this model (\textsf{extended}).
We use graphs with both positive and negative weights for the tests. The search We use graphs with both positive and negative weights for the tests. The search
strategy fixes the $next$ variables in order of their maximum value. First we strategy fixes the \mzninline{next} variables in order of their maximum value.
note that \textsf{extended} is slightly better than \textsf{full} because of the First we note that \textsf{extended} is slightly better than \textsf{full}
simpler translation, while \textsf{half} is substantially better than because of the simpler translation, while \textsf{half} is substantially better
\textsf{extended} since most of the half reified \texttt{element} constraints than \textsf{extended} since most of the half reified \texttt{element}
become redundant. Learning increases the advantage because the half reified constraints become redundant. Learning increases the advantage because the half
formulation focusses on propagation which leads to failure which creates more reified formulation focuses on propagation which leads to failure which creates
reusable nogoods. more reusable nogoods.
\begin{table} [tb] \begin{center} \begin{table} [tb] \begin{center}
\caption{\label{tab:pctsp} Prize collecting paths: \caption{\label{tab:hr-pctsp} Prize collecting paths: Average time (in seconds)
Average time (in seconds) and number of solved and number of solved instances with a 300s timeout for various number of
instances with a 300s timeout for various number of nodes.} nodes.}
\begin{tabular}{|l||rr|rr|rr||rr|rr|rr|} \begin{tabular}{|l||rr|rr|rr||rr|rr|rr|}
\hline \hline
& \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\ & \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\
@ -2457,11 +2468,11 @@ Nodes &
In the final experiment we compare resource constrained project scheduling In the final experiment we compare resource constrained project scheduling
problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task
decomposition as in \cref{ex:cumul} above, using both full reification and decomposition as in \cref{ex:hr-cumul} above, using both full reification and
half-reification. We use standard benchmark examples from PSPlib half-reification. We use standard benchmark examples from PSPlib
\autocite{kolisch-1997-psplib}. \Cref{tab:rcpsp} compares RCPSP instances using \autocite{kolisch-1997-psplib}. \Cref{tab:hr-rcpsp} compares RCPSP instances
\textsf{full} reification and \textsf{half} reification. We compare using J30 using \textsf{full} reification and \textsf{half} reification. We compare using
instances (\textsf{J30} ) and instances due to Baptiste and Le Pape J30 instances (\textsf{J30} ) and instances due to Baptiste and Le Pape
(\textsf{BL}). Each line in the table shows the average run time and number of (\textsf{BL}). Each line in the table shows the average run time and number of
solved instances. The search strategy tries to schedule the task with the solved instances. The search strategy tries to schedule the task with the
earliest possible start time. We find a small and uniform speedup for earliest possible start time. We find a small and uniform speedup for
@ -2469,7 +2480,7 @@ earliest possible start time. We find a small and uniform speedup for
learning, again because learning is not confused by propagations that do not learning, again because learning is not confused by propagations that do not
lead to failure. lead to failure.
\begin{table} [tb] \caption{\label{tab:rcpsp} RCPSP: \begin{table} [tb] \caption{\label{tab:hr-rcpsp} RCPSP:
Average time (in seconds) and number of solved instances with a 300s timeout.} Average time (in seconds) and number of solved instances with a 300s timeout.}
\begin{center} \begin{center}
\begin{tabular}{|l||rr|rr||rr|rr|} \begin{tabular}{|l||rr|rr||rr|rr|}
@ -2494,15 +2505,13 @@ To verify the effectiveness of the half reification implementation within the
\minizinc{} translator (rev. \jip{add revision}) against the equivalent version \minizinc{} translator (rev. \jip{add revision}) against the equivalent version
for which we have implemented half reification. We use the model instances used for which we have implemented half reification. We use the model instances used
by the \minizinc{} challenges by the \minizinc{} challenges
\autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2012 until 2017. \autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2019 and 2020. The
Note that the instances that the instances without any reifications have been
excluded from the experiment as they would not experience any change. The
performance of the generated \flatzinc{} models will be tested using Gecode, performance of the generated \flatzinc{} models will be tested using Gecode,
flattened with its own library, and Gurobi and CBC, flattened with the linear flattened with its own library, and Gurobi and CBC, flattened with the linear
library. library.
\begin{table} [tb] \begin{table} [tb]
\caption{\label{tab:flat_results} Flattening results: Average changes in the \caption{\label{tab:hr-flat-results} Flattening results: Average changes in the
generated the \flatzinc{} models} generated the \flatzinc{} models}
\begin{center} \begin{center}
\begin{tabular}{|l|r||r|r|r||r|} \begin{tabular}{|l|r||r|r|r||r|}
@ -2517,9 +2526,9 @@ library.
\end{tabular} \end{tabular}
\end{center} \end{center}
\end{table} \end{table}
\jip{Better headers for \cref{tab:flat_results} and update with current results} \jip{Better headers for \cref{tab:hr-flat-results} and update with current results}
\Cref{tab:flat_results} shows the average change on the number of full \Cref{tab:hr-flat-results} shows the average change on the number of full
reification, constraints, and variables between the \flatzinc\ models generated reification, constraints, and variables between the \flatzinc\ models generated
by the different versions of the translator using the different libraries. We by the different versions of the translator using the different libraries. We
find that the number full reifications is reduced by a significant amount. find that the number full reifications is reduced by a significant amount.
@ -2535,8 +2544,7 @@ of memory running the Ubuntu 16.04.3 LTS operating system.
\jip{Scatter plot of the runtimes + discussion!} \jip{Scatter plot of the runtimes + discussion!}
%=============================================================================% %=============================================================================%
\section{Related Work and Conclusion} \section{Related Work and Conclusion}\label{sec:hr-conclusion}
\label{conclusion}
%=============================================================================% %=============================================================================%
Half reification on purely Boolean constraints is well understood, this is the Half reification on purely Boolean constraints is well understood, this is the
@ -2546,33 +2554,28 @@ clausal representation of the circuit (see \eg\
total) and the calculation of polarity for Booleans terms inside total) and the calculation of polarity for Booleans terms inside
\texttt{bool2int} do not arise in pure Boolean constraints. \texttt{bool2int} do not arise in pure Boolean constraints.
Half reified constraints have been used in constraint modeling but are typically Half reified constraints have been used in constraint modelling but are
not visible as primitive constraints to users, or produced through flattening. typically not visible as primitive constraints to users, or produced through
Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to implement flattening. Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to
reified constraints by specifying how to propagate a constraint implement reified constraints by specifying how to propagate a constraint,
$c$, %($prop(c)$), propagate its negation, check disentailment, and check entailment, and this is
propagate its negation, implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A half reified
%$prop(\neg c)$, propagator simply omits entailment and propagating the negation.
check disentailment, % $check(c)$,
and check entailment, %$check(\neg c)$,
and this is implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A
half reified propagator simply omits entailment and propagating the negation.
% $prop(\neg c)$ and $check(\neg c)$. Half reification was briefly discussed in
% our earlier work \autocite{cp2009d}, in terms of its ability to reduce
% propagation.
Half reified constraints appear in some constraint systems, for example SCIP Half reified constraints appear in some constraint systems, for example SCIP
\autocite{gamrath-2020-scip} supports half-reified real linear constraints of \autocite{gamrath-2020-scip} supports half-reified real linear constraints of
the form $b \half \sum_i a_i x_i \leq a_0$ exactly because the negation of the the form \mzninline{b -> sum(i in N)(a[i] * x[i]) <= C} exactly because the
linear constraint $\sum_i a_i x_i > a_0$ is not representable in an LP solver so negation of the linear constraint \mzninline{sum(i in N)(a[i] * x[i]) > C} is
full reification is not possible. not representable in an LP solver so full reification is not possible.
While flattening is the standard approach to handle complex formula involving While flattening is the standard approach to handle complex formula involving
constraints, there are a number of other approaches which propagate more constraints, there are a number of other approaches which propagate more
strongly. Schulte proposes a generic implementation of $b \full c$ propagating strongly. Schulte proposes a generic implementation of \mzninline{b <-> c}
(the flattened form of) $c$ in a separate constraint space which does not affect propagating (the flattened form of) \mzninline{c} in a separate constraint space
the original variables \autocite*{schulte-2000-deep}; entailment and which does not affect the original variables \autocite*{schulte-2000-deep};
disentailment of $c$ fix the $b$ variable appropriately, although when $b$ is entailment and disentailment of \mzninline{c} fix the \mzninline{b} variable
made $\false$ the implementation does not propagate $\neg c$. This can also be appropriately, although when \mzninline{b} is made \mzninline{false} the
implementation does not propagate \mzninline{not c}. This can also be
implemented using propagator groups \autocite{lagerkvist-2009-groups}. Brand and implemented using propagator groups \autocite{lagerkvist-2009-groups}. Brand and
Yap define an approach to propagating complex constraint formulae called Yap define an approach to propagating complex constraint formulae called
controlled propagation which ensures that propagators that cannot affect the controlled propagation which ensures that propagators that cannot affect the