diff --git a/chapters/A3_temp_hr.tex b/chapters/A3_temp_hr.tex deleted file mode 100644 index 49cd2b2..0000000 --- a/chapters/A3_temp_hr.tex +++ /dev/null @@ -1,2617 +0,0 @@ -%************************************************ -\chapter{TEMP: Half Reification Journal Paper}\label{ch:half-reif-journal} -%************************************************ -% -% Half-reification math things - -\newcommand{\VV}{{\cal\ V}} -\newcommand{\PP}{{\cal\ P}} -\newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]} -\newcommand{\gfp}{\textup{gfp}} -\newcommand{\lfp}{\textup{lfp}} -\newcommand{\iter}{\mathit{iter}} - -\newcommand{\half}{\Rightarrow} -\newcommand{\full}{\Leftrightarrow} -\renewcommand{\half}{\rightarrow} -\renewcommand{\full}{\leftrightarrow} - -\newcommand{\entails}{\models} -% \newcommand{\bigsqcap}{\mathop{\lower.1ex\hbox{\Large$\sqcap$}}} - -% \DeclareMathOperator{\rules}{\mathit{rules}} -% \DeclareMathOperator{\lazy}{\mathit{lazy}} -% \DeclareMathOperator{\events}{\mathit{events}} -% \DeclareMathOperator{\domain}{\mathit{domain}} -% \DeclareMathOperator{\bc}{\mathit{bc}} -% \DeclareMathOperator{\lbc}{\mathit{lbc}} -% \DeclareMathOperator{\ubc}{\mathit{ubc}} -% \DeclareMathOperator{\dmc}{\mathit{dmc}} -% \DeclareMathOperator{\fix}{\mathit{fix}} -% \DeclareMathOperator{\event}{\mathit{event}} -% \DeclareMathOperator{\minassign}{\mathit{minassign}} -% \DeclareMathOperator{\assign}{\mathit{assign}} -% \DeclareMathOperator{\cl}{\mathit{cl}} -% \DeclareMathOperator{\UP}{\mathit{UP}} -% \DeclareMathOperator{\up}{\mathit{up}} -% \DeclareMathOperator{\DOM}{\mathit{DOM}} -% \DeclareMathOperator{\setb}{\mathit{sb}} -% \DeclareMathOperator{\bnd}{\mathit{bnd}} -% \DeclareMathOperator{\dsb}{\mathit{dsb}} -% \DeclareMathOperator{\vars}{\mathit{vars}} -% \DeclareMathOperator{\ivars}{\mathit{input}} -% \DeclareMathOperator{\ovars}{\mathit{output}} - -% \DeclareMathOperator{\solns}{\mathit{solns}} -% \DeclareMathOperator{\solv}{\mathit{solv}} -% \DeclareMathOperator{\isolv}{\mathit{isolv}} -% \DeclareMathOperator{\conv}{\mathit{conv}} -% \DeclareMathOperator{\ran}{\mathit{ran}} -% \DeclareMathOperator{\ite}{\mathit{ite}} -% \DeclareMathOperator{\VAR}{\mathit{VAR}} - -% \DeclareMathOperator{dom}{\mathit{idx}} -% -Discrete optimisation solvers solve constraint optimisation problems of the form -\(\min o \text{~subject to~} \wedge_{c \in C} c\), that is minimising an -objective \(o\) subject to an (existentially quantified) conjunction of -primitive constraints \(c\). But modelling languages such as OPL -\autocite{van-hentenryck-1999-opl}, Zinc/\minizinc\ -\autocite{marriott-2008-zinc, nethercote-2007-minizinc} and Essence -\autocite{frisch-2007-essence} allow much more expressive problems to be -formulated. Modelling languages map the more expressive formulations to -existentially quantified conjunction through a combination of loop unrolling, -and flattening using reification. - -\begin{example}\label{ex:hr-cons} - Consider the following ``complex constraint'' written in \minizinc\ syntax - - \begin{mzn} - constraint i <= 4 -> a[i] * x >= 6; - \end{mzn} - - which requires that if \mzninline{i \leq 4} then the value in the - \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x} - must be at least 6. This becomes the following existentially quantified - conjunction through flattening and reification:\footnote{Actually the result - is in \flatzinc\ but we show an equivalent \minizinc\ form for easy of - readability.} - - \begin{mzn} - constraint b1 <-> i <= 4; % b1 holds iff i <= 4 - constraint element(i, a, t1); % t1 is the ith element of a - constraint mult(t1, x, t2); % t2 is t1 * x - constraint b2 <-> t2 >= 6; % b2 holds iff t2 >= 6 - constraint b1 -> b2 % b1 implies b2 - \end{mzn} - - The complex logic (implication) is encoded by ``reifying'' the arguments and - in effect naming their truth value using new Boolean variables \texttt{b1} and - \texttt{b2}. The term structure is encoded by ``flattening'' the terms and - converting the functions to relations, introducing the new integer variables - \texttt{t1} and \texttt{t2}. Note that the newly introduced variables are - existentially quantified. -\end{example} - -The translation given in the above example is well understood, but potentially -flawed, for three reasons. The first is that the flattening may not give the -intuitive meaning when functions are partial. - -\begin{example} - Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i} - takes the value \texttt{7}. The constraint \mzninline{element(i, a, t1)} will - fail and no solution will be found. Intuitively if \mzninline{i = 7} the - constraint should be trivially true. -\end{example} - -The simple flattening used above treats partial functions in the following -manner. Application of a partial function to a value for which it is not defined -gives value \undefined, and this \undefined\ function percolates up through -every expression to the top level conjunction, making the model unsatisfiable. -For the example - -\begin{mzn} -/* t1 @\(\equiv\)@ */ a[7] = @\undefined{}@; -/* t2 @\(\equiv\)@ */ @\undefined{}@ * x = @\undefined{}@; -/* b2 @\(\equiv\)@ */ @\undefined{}@ >= 6 = @\undefined{}@; -/* b1 @\(\equiv\)@ */ 7 <= 4 = false; -false -> @\undefined{}@ = @\undefined{}@; -\end{mzn} - -This is known as the \emph{strict} semantics -\autocite{frisch-2009-undefinedness} for modelling languages. - -The usual choice for modeling partial functions in modelling languages is the -\emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the -relational semantics the value \undefined\ percolates up through the term until it -reaches a Boolean subterm where it becomes \(\mzninline{false}\). For the example - -\begin{mzn} -/* t1 @\(\equiv\)@ */ a[7] = @\undefined{}@; -/* t2 @\(\equiv\)@ */ @\undefined{}@ * x = @\undefined{}@; -/* b2 @\(\equiv\)@ */ @\undefined{}@ >= 6 = false; -/* b1 @\(\equiv\)@ */ 7 <= 4 = false; -false -> false = true; -\end{mzn} - -But in order to implement the relational semantics, the translation of the -original complex constraint needs to be far more complex. - -\begin{example} - The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models - 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 - translation of the constraint in \cref{ex:hr-cons} is - - \begin{mzn} - constraint b1 <-> i <= 4; % b1 holds iff i <= 4 - constraint element(t3,a,t1);% t1 is the t3'th element of a - constraint mult(t1,x,t2); % t2 is t1 * x - constraint b2 <-> t2 >= 6; % b2 holds iff t2 >= 6 - constraint t3 in 1..5 % t3 in index set of a - constraint b3 <-> i = t3; % b3 holds iff i = t3 - constraint b3 <-> i <= 5; % b3 holds iff i in index set of a - constraint b4 <-> b2 /\ b3 % b4 holds iff b2 and b3 hold - constraint b1 -> b4 % b1 implies b4 - \end{mzn} - - The translation forces the partial function application \texttt{element} to be - ``safe'' since \texttt{t3} is constrained to only take values in the index set - of \texttt{a}. The reified constraints defining \texttt{b3} force \texttt{t3} - to equal \texttt{i} if and only if \texttt{i} takes a value in the index set - of \texttt{a}. - % Finally the Boolean - % \(b4\) defines when the rhs condition holds \(b2\) - % and the \element{} constraint was safe \(b3\). -\end{example} - -A second weakness of reification, independent of the problems with partial -functions, is that each reified version of a constraint requires further -implementation to create, and indeed most solvers do not provide any reified -versions of their global constraints. - -\begin{example}\label{ex:hr-alldiff} - Consider the complex constraint - - \begin{mzn} - constraint i <= 4 -> all_different([i,x-i,x]); - \end{mzn} - - The usual flattened form would be - - \begin{mzn} - constraint b1 <-> i <= 4; % b1 holds iff i <= 4 - constraint minus(x,i,t1); % t1 = x - i - constraint b2 <-> all_different([i,t1,x]); - constraint b1 -> b2 % b1 implies b2 - \end{mzn} - - but no solver we are aware of implements the third primitive - constraint.\footnote{Although there are versions of soft - \mzninline{all_different}, they do not define this form.} -\end{example} - -Reified global constraints are not implemented because a reified constraint -\mzninline{b <-> pred(@\ldots{}@)} must also implement a propagator for -\mzninline{not pred(@\ldots{}@)} (in the case that \mzninline{b = false}). While -for some global constraints, \eg\ \mzninline{all_different}, this may be -reasonable to implement, for most, such as \texttt{cumulative}, the task seems -to be very difficult. - -A third weakness of the full reification is that it may keep track of more -information than is required. In a typical finite domain solver, the first -reified constraint \mzninline{b1 <-> i <= 4} will wake up whenever the upper -bound of \texttt{i} changes in order to check whether it should set \texttt{b1} -to \mzninline{true}. But setting \mzninline{b1} to \mzninline{true} will -\emph{never} cause any further propagation. There is no reason to check this. - -This is particularly important when the target solver is a mixed integer -programming solver. In order to linearise a reified linear constraint we need to -create two linear constraints, but if we are only interested in half of the -behaviour we can manage this with one linear constraint. - -\begin{example} - Consider the constraint \mzninline{b1 <-> i <= 4}, where \texttt{i} can take - values in the domain \mzninline{0..10} then its linearisation is - - \begin{mzn} - constraint i <= 10 - 6 * b1; % b1 -> i <= 4 - constraint i >= 5 - 5 * b1; % not b1 -> i >= 5 - \end{mzn} - - But in the system of constraints where this constraint occurs knowing that - \texttt{b1} is 0 will never cause the system to fail, hence we do not need to - keep track of it. We can simply use the second constraint in the - linearisation, which always allows that \texttt{b1} takes the value 0. -\end{example} - -Flattening with half-reification is an approach to mapping complex constraints -to existentially quantified conjunctions that improves upon all these weaknesses -of flattening with full reification. - -\begin{itemize} - \item Flattening with half reification can naturally produce the relational - semantics when flattening partial functions in positive contexts. - \item Half reified constraints add no burden to the solver writer; if they - have a propagator for constraint \mzninline{pred(@\ldots{}@)} then they - can straightforwardly construct a half reified propagator for - \mzninline{b -> pred(@\ldots{}@)}. - \item Half reified constraints \mzninline{b -> pred(@\ldots{}@)} can implement - fully reified constraints without any loss of propagation strength - (assuming reified constraints are negatable). - \item Flattening with half reification can produce more efficient propagation - when flattening complex constraints. - \item Flattening with half reification can produce smaller linear models when - used with a mixed integer programming solver. -\end{itemize} - -Our conclusion is that propagation solvers \emph{only} need to provide half -reified version of all constraints. This does not burden the solver writer at -all, yet it provides more efficient translation of models, and more -expressiveness in using global constraints. - -\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 -\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 -\(b\) for Booleans. -% -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 -\(\{\mzninline{true},\mzninline{false}\}\) (for the variables in \(\VV_b\)). -% -We can understand a \gls{domain} \(D\) as a formula -\(\wedge_{v \in \VV} (v \in D(v))\) stating for each variable \(v\) that its value -is in its domain. A \emph{false domain} \(D\) is a domain where -\(\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 -\emph{stronger} than \(D_2\), written \(D_1 \sqsubseteq D_2\), if -\(D_1(v) \subseteq D_2(v)\) for all \(v \in \VV\). -%% and that \(D_1\) and \(D_2\) -%% are \emph{equivalent modulo \(V\)}, written \(D_1 =_V D_2\), if \(D_1(v) = -%% D_2(v)\) for all \(v \in V\). \pjs{Equivelant modulo never used???} -%% -The \emph{intersection} of \(D_1\) and \(D_2\), denoted \(D_1 \sqcap D_2\), is defined -by the domain \(D_1(v) \cap D_2(v)\) for all \(v\in\VV\). -% -%We use \emph{range} notation: -% -%For integers \(l\) and \(u\), \(\range{l}{u}\) denotes the set of integers -%\(\{ d ~|~ l \leq d \leq u\}\). -% -We assume an \emph{initial domain} \(D_{init}\) such that all domains \(D\) that -occur will be stronger i.e.~\(D \sqsubseteq D_{init}\). - - -A \emph{valuation} \(\theta\) is a mapping of integer and Boolean variables to -correspondingly typed values, written -\(\{x_1 \mapsto d_1, \ldots, x_n \mapsto d_n, b_1 \mapsto u_1, \ldots, b_m \mapsto u_m\}\). -% PJS (not true unless \theta is in D) -% where \(d_i \in D(x_i)\) and \(A_j \in D(S_j)\). -We extend the valuation \(\theta\) to map expressions or constraints involving the -variables in the natural way. Let vars be the function that returns the set -of variables appearing in an expression, constraint or valuation. - -In an abuse of notation, we define a valuation \(\theta\) to be an element of a -domain \(D\), written \(\theta \in D\), if \(\theta(v) \in D(v)\) for all -\(v \in vars(\theta)\). - - -%\paragraph{Constraints, Propagators and Propagation Solvers} - -A constraint is a restriction placed on the allowable values for a set of -variables. -%% We shall be interested in constraints -%PJS over integer, set and Boolean variables. -%% over integer and set variables. -We define the \emph{solutions} of a constraint \(c\) to be the set of valuations -\(\theta\) that make that constraint true, i.e. -\(solns(c) = \{ \theta \ |\ (vars(\theta) = vars(c))\ \wedge\ (\entails \theta(c))\}\) - -%%MC check this para that my changes are ok -We associate with every constraint \(c\) a \emph{propagator} \(f_c\). A propagator -\(f_c\) is a monotonically decreasing function on domains that maintains solutions -of the constraint. That is, for all domains \(D \sqsubseteq D_{init}\): - -\(f_c(D) \sqsubseteq D\) (decreasing), and -\(\{\theta\in D \,|\ \theta \in solns(c)\} = \{\theta \in f_c(D)\,|\ \theta \in solns(c)\}\) -(preserves solutions), and for domains -\(D_1 \sqsubseteq D_2 \sqsubseteq D_{init}\): \(f(D_1) \sqsubseteq f(D_2)\) -(monotonic). This is a weak restriction since, for example, the identity mapping -is a propagator for any constraint. - -A domain \(D\) is \emph{domain consistent} for constraint \(c\) if -\(D(v) = \{ \theta(v)~|~\theta \in solns(c)~\wedge~\theta \in D \}\), for all -\(v \in vars(c)\). - -A domain \(D\) is \emph{bounds(Z) consistent} for constraint \(c\) over variables -\(v_1, \ldots v_n\) if for each \(i \in \{1, \ldots, n\}\) there exists -\(\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 -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 -Boolean variables \(v\) we assume \(\mzninline{false} < \mzninline{true}\). - -% 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 -% \(c'\) is the \emph{real relaxation} of \(c\). - -A domain \(D\) is \emph{bounds(R) consistent} for constraint \(c\) over integer -variables \(x_1, \ldots x_n\) and Boolean variables \(b_1, \ldots, b_m\) if \(c'\) is -the real relaxation of \(c\) (where \(x_1, \ldots, x_n\) can take real values, -rather than just integer values) and for each \(i \in \{1, \ldots, n\}\) there -exists \(\theta \in solns(c') \cap D\) s.t. \(\theta(x_i) = \min D(x_i)\) and -\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n\) and -\(\theta(b_j) \in D(b_j), 1 \leq j \leq m\), and similarly exists -\(\theta \in solns(c') \cap D\) s.t. \(\theta(x_i) = \max D(x_i)\) and -\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n\) and -\(\theta(b_j) \in D(b_j), 1 \leq j \leq m\). Also for each \(i in \{1,\ldots, m\}\) -and \(tf \in D(b_i)\) there exists \(\theta \in solns(c') \cap D\) s.t. -\(\theta(b_i) = tf\) and -\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \leq n\) and -\(\theta(b_j) \in D(b_j), 1 \leq j \neq i \leq m\). - -Note that we assume Booleans can only take Boolean values in the real -relaxation. - -Note that for the pure Boolean constraints domain, bounds(Z) and bounds(R) -consistency coincide. - -A propagator \(f_c\) is \(X\)-consistent if \(f(D)\) is always \(X\) consistent for \(c\), -where \(X\) could be domain, bounds(Z) or bounds(R). - -A \emph{propagation solver} for a set of propagators \(F\) and current domain \(D\), -\(solv(F,D)\), repeatedly applies all the propagators in \(F\) starting from domain -\(D\) until there is no further change in the resulting domain. \(solv(F,D)\) is -the weakest domain \(D' \sqsubseteq D\) which is a fixpoint (i.e.~\(f(D') = D'\)) -for all \(f \in F\). In other words, \(solv(F,D)\) returns a new domain defined by -\( solv(F,D) = \gfp(\lambda d.\iter(F,d))(D)\) where -\(\iter(F,D) = \bigsqcap_{f \in F} f(D)\), where \(\gfp\) denotes the greatest -fixpoint w.r.t \(\sqsubseteq\) lifted to functions. -% (We use the greatest fixpoint because we are coming down from a full domain, -% not going up from an empty one.) - - -\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{\subs}[1]{[\![ #1 ]\!] } -\newcommand{\flatc}{\nonterm{flatc}} -\newcommand{\flatt}{\nonterm{flatt}} -\newcommand{\new}{\textbf{new}~} -\newcommand{\evalb}{\nonterm{evala}} -\newcommand{\evali}{\nonterm{evali}} - -Below is a grammar for a subset of \minizinc\, with enough complexity to -illustrate all the main challenges in flattening. - -The \syntax{} nonterminal defines constraints (Boolean terms), -\syntax{} defines integer terms, \syntax{} defines Boolean arrays, -and \syntax{} defines integer arrays: - -\begin{grammar} - ::= "true" | "false" | | | "not" - \alt "/\\" | "\\/" | "->" | "<->" - \alt "forall(" ")" | | "[" "]" - | pred(, \ldots, ) - \alt "if" "then" "else" "endif" - \alt "let" "{" "}" "in" - - ::= | | | "[" "]" - \alt "sum(" ")" \alt "if" "then" "else" "endif" - \alt "bool2int(" ")" \alt "let" "{" "}" "in" - - ::= "[" , \ldots, "]" \alt "[" "|" "in" ".." "]" - - ::= "[" , \ldots, "]" \alt "[" "|" "in" ".." "]" - - ::= "==" | "<=" | "<" | "!=" | ">=" | ">" - - ::= "+" | "-" | "*" | "div" -\end{grammar} - -The grammar uses the symbols \syntax{} for Boolean variables, -\syntax{} for names of predicates, \syntax{} for integer constants, -and \syntax{} for integer variables. - -In the \texttt{let} constructs we make use of the nonterminal \syntax{} -for declarations. We define this below using \syntax{} for integer -variable declarations, \syntax{} for Boolean variable declarations. We -use \syntax{} for optional constraint items appearing in let -declarations. We also define \syntax{} as a list of integer variable -declarations, an \syntax{} as either a predicate declaration or a -function declaration, \syntax{} as a solve directive either satisfaction -or an objective, and a model \syntax{} as some declarations followed by -items followed by a solve item. Note that \syntax{} represents the empty -string. - -\begin{grammar} - ::= "int" ":" | "var" "int" ":" | "var" ".." ":" - - ::= "bool" ":" | "var" "bool" ":" - - ::= [ "=" ] ";" | [ "=" ] ";" | - - ::= "constraint" ";" | - - ::= "int" ":" ["," ] | "var" "int" ":" ["," ] - - ::= "predicate" "(" ")" "=" ";" - \alt "function" "var" "int" ":" "(" ")" "=" ";" - - ::= "satisfy" | "maximize" | "minimize" - - ::= * "solve" - -\end{grammar} - -The main missing things are floats, long linear constraints, and set and array -variables. It misses many built-in operators and functions, but their treatment -is analogous to those we include. To simplify presentation, we assume all -predicate and function arguments are integers, but the translation can be -extended to arbitrary arguments in a straightforward way. - -\subsection{Further Notation} - -Given an expression \(e\) that contains the subexpression \(x\), we denote by -\(e\subs{x/y}\) the expression that results from replacing all occurrences of -subexpression \(x\) by expression \(y\). We will also use the notation for -multiple simultaneous replacements \(\subs{\bar{x}/\bar{y}}\) where each -\(x_i \in \bar{x}\) is replaced by the corresponding \(y_i \in \bar{y}\). - -Given a \syntax{} term defining the constraints of the model we can split -its \syntax{} subterms as occurring in different kinds of places: root -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 -solution of \(c\subs{t/\mzninline{false}}\), that is \(c\) with subterm \(t\) -replaced by \(\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 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 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/\mzninline{false}}\). The remaining -Boolean subterms of \(c\) are in \emph{mixed} contexts. While determining -contexts according to these definitions is hard, there are simple syntactic -rules which can determine the correct context for most terms, and the rest can -be treated as mixed. - -Consider the constraint expression - -\begin{mzn} - constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5); -\end{mzn} - -then \mzninline{x > 0} is in the root context, \mzninline{i <= 4} is in a -negative context, \mzninline{x + bool2int(b) = 5} is in a positive context, and -\mzninline{b} is in a mixed context. If the last equality were \mzninline{x + - bool2int(b) >= 5} then \mzninline{b} would be in a positive context. - -We assume each integer variable \(x\) is separately declared with a finite initial -set of possible values \(D_{init}(x)\). We assume each array constant is -separately declared as a mapping \(\{ i \mapsto d~|~i \in dom(a) \}\) where its -index set \(dom(a)\) is a finite integer range. Given these initial declarations, -we can determine the set of possible values \(poss(t)\) of any term \(t\) in the -language as \(poss(t) = \{ \theta(t)~|~\theta \in D_{init} \}\). Note also while -it may be prohibitive to determine the set of possible values for any term \(t\), -we can efficiently determine a superset of these values by building a superset -for each subterm bottom up using approximation. - -% Given a \cons{} term defining the constraints of the model we can split its -% \cons{} subterms as occurring in kinds of places: positive contexts, negative -% 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\) -% then \(\theta\) is also a solution of \(c[\mzninline{true}]\), that is \(c\) with subterm \(t\) -% 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 -% also a solution of \(c[\mzninline{false}]\). The remaining Boolean subterms of \(c\) are in -% mixed contexts. - -% \begin{example} -% Consider the constraint expression \(c\) \negspace -% \begin{mzn} -% constraint i <= 4 -> x + bool2int(b) = 5; -% \end{mzn} -% then \(i \leq 4\) is in a negative context, \(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\) would be in a positive -% context. \qed -% \end{example} - -% One can classify most contexts as positive or negative using a simple top-down -% analysis of the form of the expression. The remaining contexts can be -% considered mixed without compromising the correctness of the rest of the -% paper. - -Our small language contains two partial functions: \mzninline{div} returns -\undefined\ if the divisor is zero, while \mzninline{a[i]} returns \undefined\ -if the value of \mzninline{i} is outside the domain of \mzninline{a}. We can -categorise the \emph{safe} terms and constraints of the language, as those where -no \undefined\ can ever arise in any subterm. A term or constraint is -\emph{safe} if all its arguments are safe and: either the term is not a division -or array access; or it is a division term \mzninline{t1 div t2} and the set of -possible values of \mzninline{t_2} does not include 0, \mzninline{not 0 in - dom(t2)}; or it is an array access term \mzninline{a[t]} and the set of -possible values of \mzninline{t} are included in the domain of \mzninline{a}, -\mzninline{dom(t) subset dom(a)}. - -\section{Flattening with Full Reification} -\label{sec:hr-translation} - -Constraint problems formulated in \minizinc\ are solved by translating them to a -simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc\ -consists only of a sequence of variables declarations and a conjunction of -constraints. This section shows how to translate our extended \minizinc\ to -\flatzinc. The usual method for flattening complex formula of constraints is -full reification. Given a constraint \(c\) the \emph{full reified form} for -\(c\) is \(b \full c\), where \(b \not\in vars(c)\) is a Boolean variable naming -the satisfied state of the constraint \(c\). - -% The complexities in the translation arise from the need to simultaneously (a) -% unroll array comprehensions (and other loops), (b) replace predicate and -% function applications by their body, and (c) flatten expressions. - -% Once we take into account CSE, we cannot perform these separately. -% In order to have names for common subexpressions we need to flatten -% expressions. And in order to take advantage of functions -% for CSE we cannot replace predicate and function applications without -% flattening to generate these names. And without replacing predicate and -% function application by their body we are unable to see all the loops to -% unroll. - -\newcommand{\ctxt}{\ensuremath{\mathit{ctxt}}} -% \newcommand{\rootc}{\textsl{root}} -\newcommand{\pos}{\textsl{pos}} -% \newcommand{\negc}{\textsl{neg}} -\newcommand{\mix}{\textsl{mix}} -\newcommand{\cupp}{\ensuremath{\cup}\text{:=}~} -\newcommand{\posop}{\ensuremath{+}} -\newcommand{\negop}{\ensuremath{-}} -\newcommand{\fixed}{\textsf{fixed}} -\newcommand{\eval}{\textsf{eval}} - -The translation algorithm presented below generates a flat model equivalent to -the original model as a global set of constraints \(S\). We ignore the -collection of variable declarations, which is also clearly important, but quite -straightforward. The translation uses full reification to create the model. - -Common subexpression elimination is implemented using a technique similar to -\emph{hash-consing} in Lisp \autocite{allen-1978-lisp}. For simplicity we only -show syntactic CSE, which eliminates expressions that are identical after -parameter replacement. The extension to semantic CSE, using commutativity and -other equivalences, is well understood (see \autocite{rendl-2010-thesis} for a -detailed discussion) but makes the pseudo-code much longer. - -The complex part of flattening arises in flattening the constraints, we shall -ignore the declarations part for flattening and assume that any objective -function term \mzninline{e} is replaced by a new variable \mzninline{obj} and a -constraint item \mzninline{constraint obj = e} which will then be flattened as -part of the model. - -\subsection{Flattening Constraints} - -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 of constraints (the flattening) \(S\) to the store such that -\(S \models b \full c\). - -It uses the context (\(\ctxt\)) to decide how to translate, where possible -contexts are: \rootc, at the top level conjunction; \pos, positive context, -\negc, negative context, and \mix, mixed context. We use the context operations -\(\posop\) and \(\negop\) defined as: - -\centerline{% - \begin{tabular}{ccc} - \( - \begin{array}{lcl} - \posop \rootc & = & \pos \\ - \posop \pos & = & \pos \\ - \posop \negc & = & \negc, \\ - \posop \mix & = & \mix - \end{array} - \) - & ~ & - \( - \begin{array}{lcl} - \negop \rootc & = & \negc \\ - \negop \pos & = & \negc \\ - \negop \negc & = & \pos, \\ - \negop \mix & = & \mix - \end{array} - \) - \end{tabular} -} - -% \centerline{ -% \begin{tabular}{ccccccc} -% \( -% \begin{array}{lcl} -% \posop \rootc & = &\pos \\ -% \posop \pos & =& \pos -% \end{array} -% \) -% & ~~~ & -% \( -% \begin{array}{lcl} -% \posop \negc & =& \negc, \\ -% \posop \mix & =& \mix -% \end{array} -% \) -% & ~~~ & -% \( -% \begin{array}{lcl} -% \negop \rootc & = &\negc \\ -% \negop \pos & =& \negc -% \end{array} -% \) -% & ~~~ & -% \( -% \begin{array}{lcl} -% \negop \negc & =& \pos, \\ -% \negop \mix & =& \mix -% \end{array} -% \) -% \end{tabular} -% } - -% \(\negop\) and \(\posop\) as \(\negop \rootc = \negc\), \(\negop \pos = \negc\), -% \(\negop \negc = \pos\), \(\negop \mix = \mix\); and -% \(\posop \rootc = \pos\), -% \(\posop \pos = \pos\), -% \(\posop \negc = \negc\), -% \(\posop \mix = \mix\), - -Note that flattening in a \mix\ context is the most restrictive case, and the -actual flattening rules only differentiate between \rootc\ and other contexts. -The importance of the \pos\ context is that \mzninline{let} expressions within a -\pos\ context can declare new variables. The important of the \negc\ context is -to track \pos\ context arising under double negations. Note that flattening in -the root context always returns a Boolean \mzninline{b} made equivalent to -\mzninline{true} by the constraints in \(S\). For succinctness we use the -notation \mzninline{@\new{}@ b} (or \mzninline{@\new{}@ v}) to introduce a fresh -Boolean (resp.\ integer) variable and return the name of the variable. - -The Boolean result of flattening \(c\) is stored in a hash table, along with the -context and reused if an identical constraint expression is ever flattened -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 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 \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 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 cases we set the context to \mix\ since the -remaining cases require at least both a \pos\ and \negc\ or a \mix\ context. -Note that if an expression introduces a fresh variable and it appears first in a -negative context and only later in the root context, the translation aborts. -This could be fixed in a preprocessing step that sorts expressions according to -their context. - -The flattening proceeds by evaluating fixed Boolean expressions and returning -the value. We assume \fixed\ checks if an expression is fixed (determined during -\minizinc{}'s type analysis), and \eval\ evaluates a fixed expression. For -simplicity of presentation, we assume that fixed expressions are never undefined -(such as \mzninline{3 div 0}). We can extend the algorithms to handle this case, -but it complicates the presentation. Our implementation aborts in this -case.\pjs{CHECK and FIX!} While this does not agree with the relational -semantics it likely indicates a modelling error since a fixed part of the model -must be undefined. The abort forces the user to redefine the model to avoid -this. - -For non-fixed expressions we treat each form in turn. Boolean literals and -variables are simply returned. Basic relational operations flatten their terms -using the function \flatt\, which for a term \(t\) returns a tuple -\(\tuple{v,b}\) of an integer variable/value \(v\) and a Boolean literal \(b\) -such that \(b \full (v = t)\) (described in detail below). The relational -operations then return a reified form of the relation. -% If in the root context this can be simplified. -The logical operators recursively flatten their arguments, passing in the -correct context. The logical array operators evaluate their array argument, then -create an equivalent term using \textsf{foldl} and either \mzninline{/\ -}\xspace{}or \mzninline{\/} which is then flattened. A Boolean array lookup -flattens its arguments, and creates an \mzninline{element} constraint. If the -context is root this is simple, otherwise it creates a new index variable \(v'\) -guaranteed to only give correct answers, and uses this in the -\mzninline{element} constraint to avoid undefinedness. Built-in predicates abort -if not in the root context.\footnote{Using half reification this can be relaxed - to also allow positive contexts.} They flatten their arguments and add an -appropriate built-in constraint. User defined predicate applications flatten -their arguments and then flatten a renamed copy of the body.\emph{if-then-else} -evaluates the condition (which must be fixed) and flattens the \emph{then} or -\emph{else} branch appropriately. \pjs{Use the same restriction, but explain its - not all required} The handling of \mzninline{let} is the most complicated. The -expression is renamed with new copies of the let variables. We extract the -constraints from the \mzninline{let} expression using function \textsf{flatlet} -which returns the extracted constraint and a rewritten term (not used in this -case, but used in \flatt{}). 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 must be \mzninline{true} by adding \(b\) -to \(S\). - - { - \begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \flatc(\(c\),\(\ctxt\)) \\ - \> \(\tuple{h,prev}\) := hash[\(c\)]; \\ - \> \textbf{if} (\(h \neq \undefined{}\)) \\ - \>\> \textbf{if} (\(prev =\rootc\)) \textbf{return} \(h\) \\ - \>\> \textbf{if} (\(ctxt = \rootc\)) \(S\) \cupp \(\{ h \}\); hash[\(c\)] := - \(\tuple{h,\rootc}\); \textbf{return} \(h\) - \\ - \>\> \textbf{if} (\(prev = \mix \vee prev = \ctxt\)) - \textbf{return} \(h\) \\ - \>\> \(\ctxt\) := \(\mix\) \\ - \> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\ - \> \textbf{else} \\ - \> \> \textbf{switch} \(c\) \\ - %\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ - %\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ - \> \> \textbf{case} \(b'\) (\syntax{}): \(b\) := \(b'\); \\ - \> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ - \>\>\> \(\tuple{v_1, b_1}\) := \(\flatt(t_1,\ctxt)\); - \(\tuple{v_2, b_2}\) := \(\flatt(t_2,\ctxt)\); \\ - \> \> \> \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge \new b'), b' \full v_1~r~v_2\}\) \\ - \> \> \textbf{case} \texttt{not} \(c_1\): - \(b\) := \(\neg \flatc(c_1, \negop \ctxt)\) \\ - \> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \(S\) \cupp \(\{ \new b \full (\flatc(c_1, \ctxt) \wedge \flatc(c_2, \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\): - \(S\) \cupp \(\{ \new b \full (\flatc(c_1,\posop \ctxt) \vee \flatc(c_2,\posop \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\): - \(S\) \cupp \(\{ \new b \full (\flatc(c_1,\negop \ctxt) \half \flatc(c_2,\posop \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): - \(S\) \cupp \(\{ \new b \full (\flatc(c_1,\mix) \full - \flatc(c_2,\mix))\}\) - \\ - \> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, \ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \full \bigwedge_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, +\ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \full \bigvee_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}: \\ - \>\>\> - \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, \posop \ctxt)\); \\ - \>\>\> \(\tuple{v, b_{n+1}}\) := \(\flatt(t, \ctxt)\); \\ - %\>\>\> \(S\) \cupp - %\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), - %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), - %b'' \full v \in \{1,..,n\} \} \) \\ - \>\>\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{\texttt{element}(v', [b_1, \ldots, b_n], - \mzninline{true})\}\); \(b\) := \(\mzninline{true}\) \\ - \>\>\> \textbf{else} \\ - \>\>\>\> \(S\) \cupp - \(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, - \ldots, n\},\) \\ - \>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n], b'), - b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} \) - \\ - \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ - \> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \\ - \> \> \> \> \textbf{if} (\(p\_reif\) does not exist) \textbf{abort} \\ - \> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'), - \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ - \> \> \> \textbf{else} \\ - \>\> \> \> \(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{}): user-defined predicate \\ - \>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ - \>\> \> \(\new b'\) := \(\flatc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\) - \\ - \> \>\> \(S\) \cupp \(\{ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n - b_j\}\) - \\ - \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else} - \(c_2\) \texttt{endif}: - % \\ \> \> \> - \textbf{if} (\(\eval(c_0)\)) \(b\) := \(\flatc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\flatc(c_2,\ctxt)\) \\ - \>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\ - \>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined - in \(d\) \\ - \> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, - c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)\) \\ - \> \> \> \(b\) := \(\flatc(c',\ctxt)\); - \\ - \> \> \textbf{endswitch} \\ - \> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ - \> hash[\(c\)] := \(\tuple{b,\ctxt}\) \\ - \> \textbf{return} \(b\) - \end{tabbing} - } - -The function \evalb{} replaces an array comprehension by the resulting array. -Note that terms \(\mathit{lt}\) and \(\mathit{ut}\) must be fixed in a correct -\minizinc\ model. - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \evalb(\(t\)) \\ - \> \textbf{switch} \(t\) \\ - \> \textbf{case} \verb+[+ \(t_1, \ldots, t_n\) \verb+]+: - \textbf{return} \verb+[+ \(t_1, \ldots, t_n\) \verb+]+ - \\ - \> \textbf{case} \verb+[+ \(e\) \verb+|+ \(v\) \texttt{in} \(\mathit{lt}\) \texttt{..} \(\mathit{ut}\) - \verb+]+: - \\ \> \> - \textbf{let} \(l = \eval(\mathit{lt})\), \(u = \eval(\mathit{ut})\) - \\ \> \> - \textbf{return} \verb+[+ \(e\subs{v/l}\), \(e\subs{v/l+1}\), - \ldots \(e\subs{v/u}\) \verb+]+ -\end{tabbing} - -\subsection{Handling \texttt{let} Expressions} - -Much of the handling of a \mzninline{let} is implemented by -\textsf{flatlet}\((d,c,t,\ctxt)\) which takes the declarations \(d\) inside the -\mzninline{let}, the constraint \(c\) or term \(t\) of the scope of the -\mzninline{let} expression, as well as the context type. First \textsf{flatlet} -replaces parameters defined in \(d\) by their fixed values. Then it collects in -\(c\) all the constraints that need to stay within the Boolean context of the -\mzninline{let}: the constraints arising from the variable and constraint items, -as well as the Boolean variable definitions. Integer variables that are defined -have their right hand side flattened, and a constraint equating them to the -right hand side \(t'\) added to the global set of constraints \(S\). If -variables are not defined and the context is negative or mixed the translation -aborts. - - {%\small - \begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \textsf{flatlet}(\(d\),\(c\),\(t\),\(\ctxt\)) \\ - \> \textbf{foreach} (\(item \in d\)) \\ - \> \> \textbf{switch} \(item\) \\ - \> \> \textbf{case} \texttt{var bool :} \(b = c'\) : \= \kill - \> \> \textbf{case} \texttt{bool :} \(b = c'\) : \> \(d\) := - \(d\subs{b/\eval(c')}\); \= \(c\) := \(c\subs{b/\eval(c')}\); \= \kill - %\> \> \textbf{case} \texttt{\(l\) .. \(u\) :} \(v = t'\) : \> \(d\) := - %\(d\subs{v/\eval(t')}\); \> \(c\) := \(c\subs{v/\eval(t')}\); \> \(t\) := \(t\subs{v/\eval(t')}\) \\ - \> \> \textbf{case} \texttt{int :} \(v = t'\) : \> \(d\) := \(d\subs{v/\eval(t')}\); - \> \(c\) := \(c\subs{v/\eval(t')}\); \> \(t\) := \(t\subs{v/\eval(t')}\)\\ - \> \> \textbf{case} \texttt{bool :} \(b = c'\) : \> \(d\) := - \(d\subs{b/\eval(c')}\); \> \(c\) := \(c\subs{b/\eval(c')}\); \> \(t\) := \(t\subs{b/\eval(c')}\) - \\ - %\> \textbf{endfor} \\ - \> \textbf{foreach} (\(item \in d\)) \\ - \> \> \textbf{switch} \(item\) \\ - %\> \> \textbf{case} \texttt{\(l\) .. \(u\) :} \(v = t'\) : \> \(c\) := \(c\) \verb+/\+ \(l\) - %\texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\) \\ - \> \> \textbf{case} \texttt{var int :} \(v\) : \> \textbf{if} (\(\ctxt \in - \{\negc,\mix\}\)) \textbf{abort} \\ - \> \> \textbf{case} \texttt{var int :} \(v = t'\) : - \> \(\tuple{v',b'}\) := \(\flatt(t',\ctxt)\); - \(S\) \cupp \(\{v = v'\}\); \(c\) := \(c\) \verb+/\+ \(b'\) - \\ - \> \> \textbf{case} \texttt{var} \(l\) \texttt{..} \(u\) \texttt{:} \(v\) : \> - \textbf{if} (\(\ctxt \in - \{\negc,\mix\}\)) \textbf{abort} \textbf{else} \(c\) := \(c\) - \verb+/\+ \(l\) \texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\) - \\ - \> \> \textbf{case} \texttt{var} \(l\) \texttt{..} \(u\) \texttt{:} \(v = t'\) : - \> \(\tuple{v',b'}\) := \(\flatt(t',\ctxt)\); - \(S\) \cupp \(\{v = v'\}\); \\ - \> \> \> \(c\) := \(c\) \verb+/\+ \(b'\) - \verb+/\+ \(l\) \texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\); - \\ - \> \> \textbf{case} \texttt{var bool :} \(b\) : \> \textbf{if} (\(\ctxt \in - \{\negc,\mix\}\)) \textbf{abort} \\ - \> \> \textbf{case} \texttt{var bool :} \(b = c'\) : \> - \(c\) := \(c\) - \verb+/\+ (\(b\) \verb+<->+ \(c'\)) \\ - \> \> \textbf{case} \texttt{constraint} \(c'\) : \> \(c\) := \(c\) - \verb+/\+ \(c'\) \\ - \> \> \textbf{endswitch} \\ - \> \textbf{return} \(\tuple{c,t}\) - \end{tabbing} - } - -\subsection{Flattening Integer Expressions} - -\(\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\), 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 -always returns a Boolean \(b\) made equivalent to \mzninline{true} by the -constraints in \(S\). - -Flattening first checks if the same expression has been flattened previously and -if so returns the stored result. \flatt{} evaluates fixed integer expressions -and returns the result. -% For non-fixed integer expressions \(t\), if \(t\) -% is determined to be total, it changes the context to -% \(\rootc\) since this is safe. -For non-fixed integer expressions \(t\) each form is treated in turn. Simple -integer expressions are simply returned. Operators have their arguments -flattened and the new value calculated on the results. A safe form of division -is used, introducing a new variable \(v'2\) as the divisor which can never be -zero, and a new Boolean \(b'\) captures when the division is defined. Array -lookup flattens all the integer expressions involved and creates a -\mzninline{element} constraint with a new index variable \(v'\) which is -guaranteed to be in the domain of the array (\mzninline{1..n}), and a new -Boolean \(b'\) which captures when the lookup is safe. \pjs{This is not the - usual ``lazy'' relational semantics!} \texttt{sum} expressions evaluate the -array argument, and then replace the sum by repeated addition using -\textsf{foldl} and flatten that. \emph{if-then-else} simply evaluates the -\emph{if} condition (which must be fixed) and flattens the \emph{then} or -\emph{else} branch appropriately. \pjs{Fix for variable conditions, or state we - ignore them for simplicity!} Functions are simply handled by flattening each -of the arguments, the function body is then renamed to use the variables -representing the arguments, and the body is then flattened. Importantly, if the -function is declared total it is flattened \emph{in the root context}. Let -constructs are handled analogously to \flatc. We rename the scoped term \(t_1\) -to \(t'\) and collect the constraints in the definitions in \(c'\). The result -is the flattening of \(t'\), with \(b\) capturing whether anything inside the -let leads to failure. - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \flatt(\(t\),\(\ctxt\)) \\ - \> \(\tuple{h,b',prev}\) := hash[\(t\)]; \\ - \> \textbf{if} (\(h \neq \undefined{}\)) \\ - \>\> \textbf{if} (\(prev =\rootc\)) - \textbf{return} \(\tuple{h,b'}\) \\ - \>\> \textbf{if} (\(ctxt = \rootc\)) \(S\) \cupp \(\{ b' \}\); hash[\(t\)] := - \(\tuple{h,b',\rootc}\); \textbf{return} \(\tuple{h,b'}\) - \\ - \>\> \textbf{if} (\(prev = \mix \vee prev = \ctxt\)) - \textbf{return} \(\tuple{h,b'}\) \\ - \>\> \(\ctxt\) := \(\mix\) \\ - \> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\ - \> \textbf{else} %\\ - %% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\ - %\> \> - \textbf{switch} \(t\) \\ - %\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\ - \> \> \textbf{case} \(v'\) (\syntax{}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\ - \> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): \\ - \> \> \> - \(\tuple{v_1,b_1}\) := \(\flatt(t_1,\ctxt)\); - \(\tuple{v_2,b_2}\) := \(\flatt(t_2,\ctxt)\); \\ - \> \> \> \textbf{if} (\(a \not\equiv \texttt{div} \vee \ctxt = \rootc\)) - \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2), a(v_1,v_2,\new v) \}\) \\ - %\> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge - %\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}\) \\ - \> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge - \new b'), \new v_2' \neq 0,\) \\ - \> \> \> \> \> \>\>\> \(\texttt{div}(v_1,v_2',\new v), b' \full v_2 \neq 0, b' \full - v_2 = v_2' \}\) \\ - \> \> \textbf{case} \([t_1, \ldots, t_n]\) \texttt{[} \(t_{0}\) \texttt{]}: \\ - \> \> \> - \textbf{foreach}(\(j \in 0..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ - %\>\> \> \(S\) := - %\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), - %\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n], \new v), - %b' \full v_0 \in \{1,...,n\} \}\) - %\\ - \>\>\> \textbf{if} (\(\ctxt \neq \rootc\)) \\ - \>\>\>\> \(S\) \cupp - \(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), \new v' \in \{1, - \ldots, n\},\) \\ - \>\>\>\>\>\>\> \(\texttt{element}(v', [v_1, \ldots, v_n], \new v), - b' \full v_0 = v', b' \full v_0 \in \{1,\ldots,n\} \} \) - \\ - \>\>\> \textbf{else} \(S\) \cupp \(\{\new b, \texttt{element}(v', [v_1, \ldots, v_n], - \new v) \}\) \\ - \> \> \textbf{case} \texttt{sum(} \(\mathit{ia}\) \texttt{)}: \\ - \> \> \> \textbf{let} \([t_1, \ldots, t_n] = \evalb(ia)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := - \(\flatt(t_j,\ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \full \bigwedge_{j=1}^n b_j, - \new v = \sum_{j=1}^n v_j \}\) \\ - %\> \> \> - %\(\tuple{v,b}\) := \flatt( - %\textsf{foldl}(\(\evalb(ia)\), \texttt{0}, \texttt{+}), \(\ctxt\)) - %\\ - \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(t_1\) \texttt{else} - \(t_2\) \texttt{endif}: - % \\ \> \> \> - \textbf{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\flatt(t_1,\ctxt)\) \textbf{else} - \(\tuple{v,b}\) := \(\flatt(t_2,\ctxt)\) - \\ - \>\> \textbf{case} \texttt{bool2int(} \(c_0\) \texttt{)}: - \(b_0\) := \(\flatc(c_0, \mix)\); - \(S\) \cupp \(\{ \texttt{bool2int}(b_0, \new v), \new b \}\) \\ - \>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): function \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ - \>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\ - \> \> \> \textbf{if} (\(f\) is declared total) \(\ctxt' = \rootc\) \textbf{else} - \(\ctxt' = \ctxt\) \\ - \>\> \> \(\tuple{v,b'}\) := \(\flatt(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt')\) \\ - \> \> \> \(S\) \cupp \(\{ \new b \full b' \wedge \bigwedge_{j=1}^n b_j \}\) - \\ - %\> \> \> \textbf{THINK we can go bakc to the other one now?} \\ - %\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ - %\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\new w_i\); \\ - %\>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t'\) be defn of \(p\) \\ - %\>\> \> \(\tuple{v,b}\) := \(\flatt(t'\subs{x_1/w_1, \ldots, x_n/w_n},\rootc)\) - %\\ - %\>\> \> \(S\) \cupp \(\{ b \half (v_1=w_1 \wedge \ldots \wedge v_n=w_n)\}\)\\ - \>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(t_1\): \\ - \>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined - in \(d\) \\ - \> \> \> \(\tuple{c',t'}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true}, - t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ - \>\> \> \(\tuple{v,b_1}\) := \(\flatt(t',\ctxt)\); - \(b_2\) := \(\flatc(c',\ctxt)\); - \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2)\}\) - \\ - \> \> \textbf{endswitch} \\ - \> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ - \> hash[\(t\)] := \(\tuple{v,b,\ctxt}\) \\ - \> \textbf{return} \(\tuple{v,b}\) -\end{tabbing} - -\begin{example}\label{ex:hr-flat} - Consider the flattening of the expression - - \[ - a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee - (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b)) - \] - - The different terms and subterms of the expression are illustrated and - numbered as follows - - \[ - \xymatrix@R=1em@C=0.6em{ - &&&&&~\vee^{(0)} \ar[dll] \ar[drr] \\ - &&&~\geq^{(1)} \ar[dl] \ar[dr] &&&&~\wedge^{(2)} \ar[dl] \ar[drr] \\ - &&~-^{(3)} \ar[dl]\ar[dr] && 4 &&~\wedge^{(4)} \ar[dl]\ar[dr] &&& - \rightarrow^{(5)} \ar[d]\ar[dr] &&& \\ - &~+^{(6)} \ar[dr]\ar[dl] && bool2int^{(7)} \ar[d] && - \leq^{(8)}\ar[dr]\ar[d] &&~>^{(9)}\ar[dr]\ar[d] &&~>^{(10)}\ar[dr]\ar[d] & - b \\ - []^{(11)}\ar[dr]\ar[d] &&bool2int^{(12)}\ar[d] &~>^{(13)}\ar[dr]\ar[d] && - []^{(14)} \ar[dr]\ar[d] & 2 &x &y &x &z &&&&& \\ - a &x &~>^{(15)}\ar[dr]\ar[d]& x&z &a &x \\ - & & x & y && \\ - } - \] - - 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 - in a \pos\ context. - - The result of flattening with full reification is: - - \begin{mzn} - constraint b0 <-> b1 \/ b2; - constraint b0; - constraint b1 <-> b2 /\ b1'; - constraint b1' <-> v3 >= 4; - constraint b2 <-> b4 /\ b5; - constraint b3 <-> b6 /\ b7; - constraint minus(v6, v7, v3); - constraint b4 <-> b8 /\ b9; - constraint b5 <-> (b10 -> b); - constraint b6 <-> b11 /\ b12; - constraint plus(v11, v12, v6); - constraint b7; - constraint bool2int(b10, v7); - constraint b8 <-> b11 /\ b8' - constraint b8' <-> v11 <= 2; - constraint b9 <-> x > y; - constraint b10 <-> x > z; - constraint b11 <-> b11'; - constraint v11' in 1..n; - constraint element(v11', a, v11); - constraint b11' <-> v11' = x; - constraint b11' <-> x in 1..n; - constraint b12; - constraint bool2int(b9, v12); - \end{mzn} - - % \(b_0 \full b_1 \vee b_2\), \(b_0\), - % \(b_1 \full b_2 \wedge b_1'\), \(b_1' \full v_3 \geq 4\), - % \(b_2 \full b_4 \wedge b_5\), - % \(b_3 \full b_6 \wedge b_7\), \(minus(v_6,v_7,v_3)\), - % \(b_4 \full b_8 \wedge b_9\), - % \(b_5 \full (b_{10} \rightarrow b)\), - % \(b_6 \full b_{11} \wedge b_{12}\), \(plus(v_{11},v_{12},v_6)\), - % \(b_7\), \(bool2int(b_{10},v_7)\), - % \(b_8 \full b_{11} \wedge b'_8\), \(b'_8 \full v_{11} \leq 2\), - % \(b_9 \full x > y\), - % \(b_{10} \full x > z\), - % \(b_{11} \full b'_{11}\), \(v'_{11} \in \{1, \ldots, n\}\), - % \(element(v'_{11}, a, v_{11})\), \(b'_{11} \full - % v'_{11} = x\), \(b'_{11} \full x \in \{1, \ldots, n\}\), - % \(b_{12}\), \(bool2int(b_{9}, v_{12})\) - where we use the position as underscore on the variable. Note that we use CSE - to reuse variables from position 11 for position 14, position 9 for position - 15, and position 10 for position 13. We dont expand the array \(a\) for - simplicity, we assume it has \(n\) entries. We can simplify the resulting - formulae by removing always true literals and replacing equivalent literals, - resulting in - - \begin{mzn} - constraint b1 \/ b2; - constraint b1 <-> b3 /\ b1'; - constraint b1' <-> v3 >= 4; - constraint b2 <-> b4 /\ b5; - constraint minus(v6, v7, v3); - constraint b4 <-> b8 /\ b9; - constraint b5 <-> (b10 -> b); - constraint plus(v11, v12, v6); - constraint bool2int(b10, v7); - constraint b8 <-> b3 /\ b8' - constraint b8' <-> v11 <= 2; - constraint b9 <-> x > y; - constraint b10 <-> x > z; - constraint v11' in 1..n; - constraint element(v11', a, v11); - constraint b3 <-> v11' = x; - constraint b3 <-> x in 1..n; - constraint bool2int(b9, v12); - \end{mzn} - - % \(b_1 \vee b_2\), - % \(b_1 \full b_3 \wedge b_1'\), \(b_1' \full v_3 \geq 4\), - % \(b_2 \full b_4 \wedge b_5\), - % \(minus(v_6,v_7,v_3)\), - % \(b_4 \full b_8 \wedge b_9\), - % \(b_5 \full (b_{10} \rightarrow b)\), - % \(plus(v_{11},v_{12},v_6)\), - % \(bool2int(b_{10},v_7)\), - % \(b_8 \full b_{3} \wedge b'_8\), \(b'_8 \full v_{11} \leq 2\), - % \(b_9 \full x > y\), - % \(b_{10} \full x > z\), - % \(v'_{11} \in \{1, \ldots, n\}\), \(element(v'_{11}, a, v_{11})\), \(b_{3} \full - % v'_{11} = x\), \(b_{3} \full x \in \{1, \ldots, n\}\), - % \(bool2int(b_{9}, v_{12})\); - a total of 18 primitive constraints and 14 intermediate variables introduced. -\end{example} -\jip{Maybe make this fit better} - -% Since the constraint solver only deals with a flat conjunction of constraints, -% modelling languages that support more complex constraint forms need to -% \emph{flatten} them into a form acceptable to the solver. The usual method for -% flattening complex formula of constraints is full reification. Given a -% constraint \(c\) the \emph{full reified form} for \(c\) is \(b \full c\), where -% \(b \not\in vars(c)\) is a Boolean variable naming the satisfied state of the -% constraint \(c\). - -%\newcommand{\new}{\textbf{new}~} -%\newcommand{\flatc}{\textsf{flatc}} -%\newcommand{\flatt}{\textsf{flatt}} -\newcommand{\safen}{\textsf{safen}} - -% 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 -% 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 -% respectively. - -% The code assumes there are reified versions of the basic relational -% constraints \(r\) available, as well as reified versions of the Boolean -% connectives. Flattening of arbitrary constraint predicates aborts if not at -% the top level of conjunction. The code handles unsafe terms by capturing them -% when they first arrive at a Boolean context using \safen. - -% {\small -% \begin{tabbing} -% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \flatc(\(b\),\(c\)) \\ -% \> \textbf{switch} \(c\) \\ -% \> \textbf{case} \texttt{true}: \textbf{return} \(\{ b \}\) \\ -% \> \textbf{case} \texttt{false}: \textbf{return} \(\{ \neg b \}\) \\ -% \> \textbf{case} \(b'\) (\syntax{}): \textbf{return} \(\{ b \full b' \}\) \\ -% \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\relop): \textbf{return} \(\safen(b, \flatt(\new i_1, t_1) \cup \flatt(\new i_2, t_2)) \cup \{ b \full i_1~r~i_2 \}\) \\ -% \> \textbf{case} \texttt{not} \(c_1\): -% \textbf{return} \(\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}\) \\ -% \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \= -% \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(\flatc(\mzninline{true}, c_1) \cup -% \flatc(\mzninline{true}, c_2)\) \\ -% \> \> \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)\}\) \\ -% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \> \textbf{case} \(c_1\) \verb+\/+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup -% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \vee -% b_2)\}\) \\ -% \> \textbf{case} \(c_1\) \verb+->+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup -% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \half -% b_2)\}\) \\ -% \> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup -% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full -% b_2)\}\) \\ -% \> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): \\ -% \> \> \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) \}\) \\ -% \> \> \textbf{else} \textbf{abort} -% \end{tabbing} -% } - -% The code \(\flatt(v,t)\) flattens an integer term \(t\), creating constraints -% that equate the term with variable \(v\). It creates new variables to store -% the values of subterms, replaces integer operations by their relational -% versions, and array lookups by \element. - -% \begin{tabbing} -% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \flatt(\(v\),\(t\)) \\ -% \> \textbf{switch} \(t\) \\ -% \> \textbf{case} \(i\) (\intc): \textbf{return} \(\{v = i\}\) \\ -% \> \textbf{case} \(v'\) (\syntax{}): \textbf{return} \(\{ v = v' \}\) \\ -% \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): -% \textbf{return} \(\flatt(\new v_1, t_1) \cup \flatt(\new v_2, t_2) \cup \{ a(v_1, v_2, v) \}\) \\ -% \> \textbf{case} \(a\) \texttt{[} \(t_1\) \texttt{]}: -% \textbf{return} \(\flatt(\new v_1, t_1) \cup \{ \texttt{element}(v_1, a, v) \}\) \\ -% \> \textbf{case} \texttt{bool2int(} \(c_1\) \texttt{)}: -% \textbf{return} \(\flatc(\new b_1, c_1) \cup \{ \texttt{bool2int}(b_1,v) \})\) -% \end{tabbing} - -The procedure \safen(\(b, C\)) enforces the relational semantics for unsafe -expressions, by ensuring that the unsafe relational versions of partial -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 \(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 -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 -constraint \(div(x,y',z)\) never reflects a partial function application. The -new variable \(b'\) captures whether the partial function application returns a -non \undefined{} value. For \mzninline{element(v, a, x)}, it introduces a new -variable \(v'\) which only takes values in \(dom(a)\) and forces it to equal -\(v\) if \(v \in dom(a)\). A partial function application forces -\(b = \mzninline{false}\) since it is the conjunction of the new variables -\(b'\). The \%HALF\% comments will be explained later. - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \safen(\(b\),\(C\)) \\ - \> \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(C\) \\ - \> \textbf{if} (\(C\) is a set of safe constraints) \textbf{return} \(C\) \\ - \> \(B\) := \(\emptyset\); \(S\) := \(\emptyset\) \\ - \> \textbf{foreach} \(c \in C\) \\ - \> \> \textbf{if} (\(c \equiv div(x,y,z)\) and \(y\) can take value 0) \\ - \> \> \> \(B\) := \(B \cup \{ \new b' \}\) \\ - \> \> \> \(S\) := \(S \cup \{ \new y' \neq 0, b' \full y \neq 0, b' \full y - = y', div(x,y',z) \}\) \\ - \> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full y \neq 0, b' \half - div(x,y,z)\}\) \\ - \> \> \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' \}\) \\ - \> \> \> \(S\) := \(S \cup \{ \new v' \in dom(a), - b' \full v \in dom(a), b' \full v = v', - \mzninline{element(v', a, x)}\}\) \\ - \> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full v \in dom(a), b' \half - \mzninline{element(v, a, x)}\}\) \\ - \> \> \textbf{else} \(S\) := \(S \cup \{c\}\) \\ - \> \> \textbf{return} \(S \cup \{b \full \wedge_{b' \in B} b' - \})\) -\end{tabbing} - -The flattening algorithms above can produce suboptimal results in special cases, -such as input with common subexpressions. Our implementation avoids generating -renamed-apart copies of already-generated constraints, but for simplicity of -presentation, we omit the algorithms we use to do this. - -\section{Half Reification} -\label{sec:hr-halfreif} - -Given a constraint \mzninline{pred(@\ldots{}@)}, the \emph{half-reified version} -of \mzninline{pred(@\ldots{}@)} is a constraint of the form \mzninline{b -> - pred(@\ldots{}@)} where \(\mzninline{b} \not\in vars(c)\) is a Boolean -variable. - -We can construct a propagator \(f_{\mzninline{b -> pred(@\ldots{}@)}}\) for the -half-reified version of \mzninline{pred(@\ldots{}@)}, \mzninline{b -> - pred(@\ldots{}@)}, using the propagator \(f_{\mzninline{pred(@\ldots{}@)}}\) -for \mzninline{pred(@\ldots{}@)}. - -\[ - \begin{array}{rcll} - 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)(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) - \text{~and~} \mzninline{false} \not\in D(b) - \end{array} -\] - -% In reality most propagator implementations for \(c\) can be thought of as -% a sequence of two propagators \(f_c = f_{prop(c)} \cdot f_{check(c)}\) -% where -% \[ -% \begin{array}{rcll} -% f_{check(c)}(D)(v) & = & \emptyset & f_c(D) \text{~is a false domain} \\ -% f_{check(c)}(D)(v) & = & D(v) & \text{otherwise} \\ -% f_{prop(c)}(D)(v) & = & D & \(D\) \text{~is a false domain} \\ -% f_{prop(c)}(D)(v) & = & f_c(D)(v) & \text{otherwise} \\ -% \end{array} -% \] -% that is first we check whether constraint is satisfiable \(check(c)\) -% and if so we propagate changes in variable domains \(prop(c)\). - -% \begin{example} -% Most propagators check consistency before propagating: e.g. -% \(\sum_i a_i x_i \leq a_0\) determines \(L = \sum_i min_D(a_i x_i) - a_0\) and -% fails if \(L > 0\) before propagating \autocite{harveyschimpf}; Regin's domain -% propagator \autocite{reginalldifferent} for \alldiff\(([x_1, \ldots, x_n])\) -% determines a maximum matching between variables and values first, if this is -% not of size \(n\) it fails before propagating; and the timetable -% \texttt{cumulative} constraint~\autocite{cumulative} determines a profile of -% necessary resource usage, and fails if this breaks the resource limit, -% before considering propagation. \qed -% \end{example} - -% 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 -% false domain''. In practice it means that the half-reified propagator can be -% implemented to only perform the checking part until \(D(b) = \{\mzninline{true}\}\), when it -% needs to perform both. - -In practice most propagator implementations for \mzninline{pred(@\ldots{}@)} -first check whether \mzninline{pred(@\ldots{}@)} is satisfiable, before -continuing to propagate. For example, \mzninline{sum(i in N)(a[i] * x[i]) <= C} -determines \mzninline{L = sum(i in N)(lb(a[i] * x[i])) - C} and fails if -\mzninline{L > 0} before propagating; Regin's domain propagator for -\mzninline{all_different(X)} determines a maximum matching between variables and -values first, if this is not of size \mzninline{length(X)} it fails before -propagating; the timetable \texttt{cumulative} constraint determines a profile -of necessary resource usage, and fails if this breaks the resource limit, before -considering propagation. We can implement the propagator for -\(f_{\mzninline{b -> pred(@\ldots{}@)}}\) by only performing the checking part -until \(D(\texttt{b}) = \{\mzninline{true}\}\). - -Half reification naturally encodes the relational semantics for partial function -applications in positive contexts. We associate a Boolean variable \mzninline{b} -with each Boolean term in an expression, and we ensure that all unsafe -constraints are half-reified using the variable of the nearest enclosing Boolean -term. - -\begin{example} - Consider flattening of the constraint of \cref{ex:hr-cons}. First we will convert - it to an equivalent expression with only positive contexts - - \begin{mzn} - i > 4 \/ a[i] * x >= 6 - \end{mzn} - - There are three Boolean terms: the entire constraint, \mzninline{i > 4} and - \mzninline{a[i] * x >= 6}, which we name \mzninline{b0}, \mzninline{b1}, and - \mzninline{b2} respectively. The flattened form using half reification is - - \begin{mzn} - constraint b1 -> i > 4; - constraint b2 -> element(i,a,t1); - constraint mult(t1,x,t2); - constraint b2 -> t2 >= 6; - constraint b1 \/ b2; - \end{mzn} - - The unsafe \mzninline{element} constraint is half reified with the name of its - nearest enclosing Boolean term. Note that if \mzninline{i = 7} then the second - constraint makes \mzninline{b2 = false}. Given this, the final constraint - requires \mzninline{b1 = true}, which in turn requires \mzninline{i > 4}. - Since this holds, the whole constraint is \mzninline{true} with no - restrictions on \mzninline{x}. -\end{example} - -Half reification can handle more constraint terms than full reification if we -assume that each global constraint predicate \(p\) is available in half-reified -form. Recall that this places no new burden on the solver implementer. - -\begin{example} - Consider the constraint of \cref{ex:hr-alldiff}. Half reification results in - - \begin{mzn} - constraint b1 -> i > 4; - constraint minus(i,x,t1); % t1 = i - x - constraint b2 -> all_different([i,t1,x]); - constraint b1 \/ b2 % b1 or b2 - \end{mzn} - - We can easily modify any existing propagator for \mzninline{all_different} to - support the half-reified form, hence this model is executable by our - constraint solver. -\end{example} - -Half reification can lead to more efficient constraint solving, since it does -not propagate unnecessarily. - -\begin{example}\label{ex:hr-cumul} - Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\ - \autocite{schutt-2009-cumulative}) which includes constraints of the form - - \begin{mzn} - constraint sum(i in Tasks where i != j) ( - bool2int(s[i] <= s[j] /\ s[i]+d[i] > s[j]) * r[i] - ) <= L-r[j]; - \end{mzn} - - which requires that at the start time \mzninline{s[j]} of task \mzninline{j}, - the sum of resources \mzninline{r} used by it and by other tasks executing at - the same time is less than the limit \mzninline{L}. Flattening with full - reification produces constraints like this: - - \begin{mzn} - constraint b1[i] <-> s[i] <= s[j]; - constraint plus(s[i],d[i],e[i]); % e[i] = s[i] + d[i] - constraint b2[i] <-> e[i] > s[j]; - constraint b3[i] <-> b1[i] /\ b2[i]; - constraint bool2int(b3[i], a[i]); % a[i] = bool2int(b3[i]) - constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j]; - \end{mzn} - - Whenever the start time of task \mzninline{i} is constrained so that it does - not overlap time \mzninline{s[j]}, then \mzninline{b3[i]} is fixed to - \mzninline{false} and \mzninline{a[i]} to 0, and the long linear sum is - awoken. But this is useless, since it cannot cause failure. - - The Boolean expression appears in a negative context, and half-reification - produces - - \begin{mzn} - constraint b1[i] -> s[i] > s[j]; - constraint plus(s[i],d[i],e[i]); % e[i] = s[i] + d[i] - constraint b2[i] -> e[i] <= s[j]; - constraint b3[i] -> b1[i] \/ b2[i]; - constraint b4[i] <-> not b3[i]; - constraint bool2int(b4[i], a[i]); % a[i] = bool2int(b4[i]) - constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j]; - \end{mzn} - - which may seem to be more expensive since there are additional variables (the - \mzninline{b4[i]}), but since both \mzninline{b4[i]} and \mzninline{a[i]} are - implemented by views \autocite{schulte-2005-views}, there is no additional - runtime overhead. This decomposition will only wake the linear constraint when - some task \mzninline{i} is guaranteed to overlap time \mzninline{s[j]}. -\end{example} - -\pjs{Add linearization example here!} - -Half reification can cause propagators to wake up less frequently, since -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 variables that are fixed can allow the simplification of -the propagator, and hence make its propagation faster. We can reduce this -disadvantage by fully reifying Boolean connectives (which have low overhead) -where possible in the half reification. \pjs{Do we do this?} - -\subsection{Flattening with Half Reification} - -\newcommand{\halfc}{\textsf{halfc}} -\newcommand{\halft}{\textsf{halft}} -\newcommand{\halfnc}{\textsf{halfnc}} - -We describe flattening using half reification in a manner analogous to -flattening using full reification. We concentrate once more on flattening -constraint items, although we shall treat objectives differently than the simple -rewriting used with full reification. - -The procedure \(\halfc(b,\mzninline{pred(@\ldots{}@)})\) defined below returns a -set of constraints implementing the half-reification \mzninline{b -> - pred(@\ldots{}@)}. We flatten a constraint item \mzninline{constraint - pred(@\ldots{}@)} using -\(\halfc(\mzninline{true}, \mzninline{pred(@\ldots{}@)})\). The half-reification -flattening transformation uses half reification whenever it is in a positive -context. If it encounters a constraint \mzninline{c1} in a negative context, it -negates the constraint if it is safe, thus creating a new positive context. If -this is not possible, it defaults to the usual flattening approach using full -reification. Note how for conjunction it does not need to introduce a new -Boolean variable. Negating a constraint expression is done one operator at a -time, and is defined in the obvious way. For example, negating \mzninline{t1 < - t2} yields \mzninline{t1 >= t2}, and negating \mzninline{c1 /\ c2} yields -\mzninline{not c1 \/ not c2}. Any negations on subexpressions will be processed -by recursive invocations of the algorithm. - -\newcommand{\bnds}{\mathit{bnds}} -\newcommand{\sign}{\textsf{sign}} -\newcommand{\iabove}{\textsf{ub}} -\newcommand{\ibelow}{\textsf{lb}} -\newcommand{\iboth}{\textsf{both}} -\newcommand{\negaterel}{\textsf{negaterel}} - -Halfreifying a constraint \(c\) in context \ctxt, \(\halfc(c,\ctxt)\), returns a -Boolean literal \(b\) representing the constraint and as a side effect adds a set -of constraints (the flattening) \(S\) to the store such that -\(S \models b \half c\). The half reification function is only called with -\(\ctxt = \rootc\) or \(\ctxt = \pos\) if negative or mixed contexts arise we use -\(\flatc\) instead. The procedure \(\halfc\) is very similar to \(\flatc\). The main -difference is that we use implication \((\half)\) to connect the Boolean literal -\(b\) of a constraint to its component parts, and use half reified versions of the -primitive constraints. We also can simplify most translations. - -The treatment of common subexpressions is simpler. We use a separate hash table. -If the previous context was the \(\rootc\), or the same we simply reuse the old -value. The remaining case is when the new context is \(\rootc\) and the previous -was \(\pos\). Then we force the variable to hold and update the hash table for -both half and full reification. When we store the result we construct for half -reification we also add an entry to the full reification hash table if the -context is \(\rootc\), in case we meet the same term in a negative or mxed context -later. - -The translation of relational operators is similar to \(\flatc\) except we use a -half reification specialized version of flattening terms \(\halft\). This takes as -an extra argument the \emph{bounds} of the term we are interested in, these -could be: \(\iabove\) we are only interested in the upper bound, \(\ibelow\) we are -only interested in the lower bound, or \(\iboth\) we are interested in both bounds -and interior values. For example for the constraint \(b \half x \leq y\) we are -only interested in the lower bound of \(x\) and the upper bound of \(y\) since these -are the only bounds that can cause failure. - -Half reifying constaints of the form \(\texttt{not}~c\) is handled by the -procedure \(\halfnc\), which pushes the negation through operations where this is -safe to do so. We discuss it in detail later. Half reification of the Boolean -connectives is very similar to full reification, it treats \(c_1~\verb+->+~c_2\) -and \(\texttt{not}~c_1 \vee c_2\) and full reification for \(c_1~\verb+<->+~c_2\). -\texttt{forall} and \texttt{exists} are treated analogously to \verb+/\+ and -\verb+\/+. - -Array lookup had to flatten the index term in a manner that is interested in -everything about its value (\(\iboth)\). The translation use a half reified -\mzninline{element} constraint which ensures safety, much simpler than in full -reification. All calls to built-in predicate \(p\) can be half reified assuming -we have the half reified version of the predicate \(p\_half\). Since this can be -created using the propagator for \(p\), this is a fair assumption. - -User defined predicates, if-then-else-endif and let are treated analogously to -full reification. - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \halfc(\(c\),\(\ctxt\)) \\ - \> \(\tuple{h,prev}\) := hhash[\(c\)]; \\ - \> \textbf{if} (\(h \neq \undefined{}\)) \\ - \>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \textbf{return} \(h\) \\ - \>\> \(S\) \cupp \(\{ h \}\); hhash[\(c\)] := - \(\tuple{h,\rootc}\); hash[\(c\)] := - \(\tuple{h,\rootc}\); \textbf{return} \(h\) - \\ - \> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\ - \> \textbf{else} \\ - \> \> \textbf{switch} \(c\) \\ - %\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ - %\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ - \> \> \textbf{case} \(b'\) (\syntax{}): \(b\) := \(b'\); \\ - \> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ - \> \> \> \textbf{switch} \(r\) \\ - \> \> \> \textbf{case} \(\leq\), \(<\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iabove)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\ibelow)\); \\ - \> \> \> \textbf{case} \(\geq\), \(>\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\ibelow)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iabove)\); \\ - \> \> \> \textbf{case} \(=\), \(\neq\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iboth)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\ - \> \> \> \textbf{endswitch} \\ - \> \> \> \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge \new b'), - b' \half v_1~r~v_2\}\) \\ - \> \> \textbf{case} \texttt{not} \(c_1\): - \(b\) := \(\halfnc(c_1, \ctxt)\) \\ - \> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \(S\) \cupp \(\{ \new b \half (\halfc(c_1, \ctxt) \wedge \halfc(c_2, \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\): - \(S\) \cupp \(\{ \new b \half (\halfc(c_1,\posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\): - \(S\) \cupp \(\{ \new b \half (\halfnc(c_1, \posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): - \(S\) \cupp \(\{ \new b \half (\flatc(c_1,\mix) \full - \flatc(c_2,\mix))\}\) - \\ - \> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \posop\ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \half \bigvee_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}: \\ - \>\>\> - \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \posop \ctxt)\); \\ - \>\>\> \(\tuple{v, b_{n+1}}\) := \(\halft(t, \ctxt, \iboth)\); \\ - %\>\>\> \(S\) \cupp - %\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), - %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), - %b'' \full v \in \{1,..,n\} \} \) \\ - \>\>\> \textbf{if} (\(\ctxt = \rootc\)) - \(S\) \cupp \(\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}\) \\ - \>\>\> \textbf{else} - \(S\) \cupp \(\{ \new b \half (b_{n+1} \wedge \new b'), b \half - \texttt{element}(v, [b_1, \ldots, b_n], b') \}\) \\ - %\>\>\> \textbf{else} \\ - %\>\>\>\> \(S\) \cupp \(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, - %\ldots, n\},\) \\ - %\>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n], b'), - %b'' \full v = v', b'' \full v \in \{1,..,n\} \} \) - %\\ - \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := - \(\halft(t_j,\ctxt,\iboth)\); \\ - \> \> \> \textbf{if} (\(\ctxt = \rootc\)) - \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j - \}\) - \\ - \>\>\> \textbf{else} %(\(\ctxt = \pos\)) \\ \> \> \> \> - \(S\) \cupp \(\{ p\_half(v_1,\ldots,v_n,\new b'), - \new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ - %\> \>\> \textbf{else} \\ - %\> \> \> \> \textbf{if} (\(p\_reif\) does not exist) \textbf{abort} \\ - %\> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'), - %\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ - %\\ - \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): user-defined predicate \\ - \>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := - \(\halft(t_j,\ctxt, \iboth)\); \\ - \>\> \> \(\new b'\) := \(\halfc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\) - \\ - \> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n - b_j\}\) - \\ - \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else} - \(c_2\) \texttt{endif}: - % \\ \> \> \> - \textbf{if} (\(\eval(c_0)\)) \(b\) := \(\halfc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\halfc(c_2,\ctxt)\) \\ - \>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\ - \>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined - in \(d\) \\ - \> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, - c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)\) \\ - \> \> \> \(b\) := \(\halfc(c',\ctxt)\); - \\ - \> \> \textbf{endswitch} \\ - \> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ - \> hhash[\(c\)] := \(\tuple{b,\ctxt}\); \textbf{if} (\(\ctxt = - \rootc\)) hash[\(c\)] := \(\tuple{b,\ctxt}\); \\ - \> \textbf{return} \(b\) -\end{tabbing} - -Since half reification has advantages rather than give up on using it when we -encounter a negation we instead try to effectively transform the term under the -negation as much as possible by pushing negations down. The procedure -\(\halfnc(c,\ctxt)\), returns a Boolean literal \(b\) representing the -constraint and as a side effect adds a set of constraints (the flattening) \(S\) -to the store such that \(S \models b \half \neg c\). The \(\ctxt\) argument -stores the context for the term \(\neg c\) and again is only ever \(\rootc\) or -\(\pos\). - -The procedure \(\halfnc\) use the same hash table but stores and looks up on the -key \(\texttt{not}~c\). When negating a basic relation we first check that the -subterms are safe, that is cannot involve partial functions, if this is the case -we can negate the relational operation and continue using half reification on -the terms. If not we use full reification. - -A term of the form \(\texttt{not}~c\) simply half reifies \(c\), the negations -cancel. Boolean connectives are inverted using De Morgan's laws when we can -still use half reification. Again full reification for \(c_1~\verb+<->+~c_2\) is -used after inserting the negation. \texttt{forall} and \texttt{exists} are -treated analogously to \verb+/\+ and \verb+\/+. - -Array lookup and built-in predicates are handled by full reification. User -defined predicates use full reification on the terms (since they occur in a -negative or mixed context) and negated half reification on the body. -If-then-else-endif and let are handled straightforwardly although note that the -context passed to \(\textsf{flatlet}\) is either \(\negc\) or \(\mix\). - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \halfnc(\(c\),\(\ctxt\)) \\ - \> \(\tuple{h,prev}\) := hhash[\(\texttt{not}~c\)];\\ - \> \textbf{if} (\(h \neq \undefined\)) \\ - \>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \textbf{return} \(h\) \\ - \>\> \(S\) \cupp \(\{ h \}\); hhash[\(\texttt{not}~c\)] := - \(\tuple{h,\rootc}\); hash[\(\texttt{not}~c\)] := - \(\tuple{h,\rootc}\); \textbf{return} \(h\)\\ - \> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\neg \eval(c)\) \\ - \> \textbf{else} \\ - \> \> \textbf{switch} \(c\) \\ - %\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ - %\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ - \> \> \textbf{case} \(b'\) (\syntax{}): \(S\) \cupp \(\{\new b \half \neg b'\}\); \\ - \> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ - \> \> \> \textbf{if} (\(t_1\) and \(t_2\) are safe) \\ - \> \> \> \> \(r'\) := \(\negaterel(r)\) \\ - \> \> \> \> \textbf{switch} \(r'\) \\ - \> \> \> \> \textbf{case} \(\leq\), \(<\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iabove)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\ibelow)\); \\ - \> \> \> \> \textbf{case} \(\geq\), \(>\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\ibelow)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iabove)\); \\ - \> \> \> \> \textbf{case} \(=\), \(\neq\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iboth)\); - \(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\ - \> \> \> \> \textbf{endswitch} \\ - \> \> \> \> \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge \new b'), - b' \half v_1 r' v_2\}\) \\ - \> \> \> \textbf{else} \\ - \> \> \> \> \(\new b\) := \(\flatc(\texttt{not} (t_1~r~t_2), \negop \ctxt)\) \\ - \> \> \textbf{case} \texttt{not} \(c_1\): - \(b\) := \(\halfc(c_1, \ctxt)\) \\ - \> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \(S\) \cupp \(\{ \new b \half (\halfnc(c_1, \posop\ctxt) \vee \halfnc(c_2, \posop\ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\): - \(S\) \cupp \(\{ \new b \half (\halfnc(c_1, \ctxt) \wedge \halfnc(c_2, \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\): - \(S\) \cupp \(\{ \new b \half (\halfc(c_1, \posop\ctxt) \vee \halfnc(c_2,\posop \ctxt))\}\) - \\ - \>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): - \(b\) := \(\flatc(\texttt{not}~c_1~\verb+<->+~c_2, \ctxt)\) - \\ - \> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfnc(c_j, \posop \ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \half \bigvee_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\ - \> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfnc(c_j, \ctxt)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j \}\) \\ - \>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}: \\ - \>\>\> \(b\) := \(\flatc(\texttt{not}~[c_1, \ldots, c_n]~\texttt{[}~t~\texttt{]}, \ctxt)\) \\ - \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ - \> \> \> \(b\) := \(\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)\) \\ - \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): user-defined predicate \\ - \>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := - \(\flatt(t_j,\negop \ctxt)\); \\ - \>\> \> \(\new b'\) := \(\halfnc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\) - \\ - \> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n - b_j\}\) - \\ - \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else} - \(c_2\) \texttt{endif}: - % \\ \> \> \> - \textbf{if} (\(\eval(c_0)\)) \(b\) := \(\halfnc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\halfnc(c_2,\ctxt)\) \\ - \>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\ - \>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined - in \(d\) \\ - \> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, - c_1\subs{\bar{v}/\bar{v}'},0,\negop \ctxt)\) \\ - \> \> \> \(b\) := \(\halfnc(c',\ctxt)\); - \\ - \> \> \textbf{endswitch} \\ - \> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ - \> hhash[\(\texttt{not}~c\)] := \(\tuple{b,\ctxt}\); \textbf{if} - (\(\ctxt = \rootc\)) hash[\(\texttt{not}~c\)] := \(\tuple{b,\ctxt}\) \\ - \> \textbf{return} \(b\) -\end{tabbing} - -\subsection{Flattening Integer Expressions with Half Reification} - -We use a specialized procedure to flatten terms for half reification. The -procedure \(\halft(t, \ctxt, \bnds)\) flattens term \(t\) in context \(\ctxt\) -(which again can only be \(\rootc\) or \(\pos\)) when we are interested in -\(\bnds\) of term \(t\). It returns a pair \(\tuple{v,b}\) and adds constraints -to \(S\) that enforce that \(b \half v = t\). The third argument is there to -create accurate context information when we meet terms of the form -\(\texttt{bool2int(} \)c\( \texttt{)}\). It acts independently of the context. - -We flatten objective functions \(e\) using this procedure also. The item -\mzninline{solve maximize e} using \(\halft(e, \rootc, \ibelow)\) since we are -interested only in the lower bounds of the expression (analogous to the -constraints we will place on the expression \(e > d\) for some constant \(d\)), -and similarly we flatten \mzninline{solve minimize e} is flattened using -\(\halft(e, \rootc, \iabove)\). The integer variable returned is used as the -objective in the flattened program. - -The common subexpression handling is somewhat complicated. The hash table for -terms stores the variable \(h\) holding the results, the Boolean \(b'\) -determining if the constraints arising from partial functions, and the previous -context and 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 \(\bnds\) to \(\iboth\) and reflatten since we require both bounds -(perhaps in different situations). Otherwise the new context is \(\rootc\) and -the previous \(\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 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 \(\ibelow\) to \(\iboth\). - -The case of arithmetic operators is interesting since we need to propagate the -interest in bounds. Addition leaves us interested in the same bounds of both -subterms, subtraction reverses the bound we are interested in for the second -argument. Multiplication is the most complex case. If one argument has a known -sign we can accurately determine the bounds of interest in the other argument, -otherwise we lose all information (\(\iboth\)). We assume \(\sign(t)\) returns -one of the context operators \(\posop\) if \(\forall d \in poss(t). d \geq 0\) -and \(\negop\) if \(\forall d \in poss(t). d \leq 0\), and returns \(\pm\) -otherwise. We extend the context operators to work on bounds information as -follows: - -\centerline{ - \begin{tabular}{ccc} - \( - \begin{array}{lcl} - \posop \iabove & = & \iabove \\ - \posop \ibelow & = & \ibelow \\ - \posop \iboth & = & \iboth, \\ - \end{array} - \) - & ~ & - \( - \begin{array}{lcl} - \negop \iabove & = & \ibelow \\ - \negop \ibelow & = & \iabove \\ - \negop \iboth & = & \iboth, \\ - \end{array} - \) - \end{tabular} -} - -For simplicity division simply loses all information. The half reification is -simpler for the partial function \texttt{div} requiring only the half reified -constraint. - -Array lookup is again simpler in half reification where we use half reified -\mzninline{element} constraint. Array sums and if-then-else-endif are -straightforward. - -The treatment of \mzninline{bool2int} is the reason for the complex bounds -analysis. If we are only interested in the lower bound of -\mzninline{bool2int(c)} we can half reify \(c\) since it is in a positive -context. If we are only interested in the upper bound of \mzninline{bool2int(c)} -we can negatively half reify \(c\) since \(c\) in a negative context, otherwise -we need to use full reification. The treatment of functions and let constructs -is analogous to that in \(\flatt\). - - -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \halft(\(t\),\(\ctxt\),\(\bnds\)) \\ - \> \(\tuple{h,b',prev,pbnds}\) := hhash[\(t\)]; \\ - \> \textbf{if} (\(h \neq \undefined{}\)) \\ - \>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \\ - \>\> \> \textbf{if} (\(pbnds = \bnds\)) \textbf{return} \(\tuple{h,b'}\) \\ - \>\> \> \textbf{else} \(\bnds\) := \(\iboth\) \\ - \>\> \textbf{else} \\ - \> \> \> \(S\) \cupp \(\{ b' \}\) \\ - \> \> \> \textbf{if} (\(pbnds = \bnds\)) hhash[\(t\)] := \(\tuple{h,b',\rootc,\bnds}\); \textbf{return} \(\tuple{h,b'}\) - \\ - \> \> \> \textbf{else} \(\bnds\) := \(\iboth\) \\ - \> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\ - \> \textbf{else} %\\ - %% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\ - %\> \> - \textbf{switch} \(t\) \\ - %\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\ - \> \> \textbf{case} \(v'\) (\syntax{}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\ - \> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): \\ - \> \> \> \textbf{switch} \(a\) \\ - \> \> \> \textbf{case} \(+\): - \(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\bnds)\); - \(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\bnds)\); \\ - \> \> \> \textbf{case} \(-\): - \(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\bnds)\); - \(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\negop \bnds)\); \\ - \> \> \> \textbf{case} \(\times\): \\ - \> \> \> \> \textbf{if} (\(\sign(t_2) \in \{\posop,\negop\}\)) - \(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\sign(t_2)~\bnds)\); \\ - \> \> \> \> \textbf{else} - \(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\iboth)\); \\ - \> \> \> \> \textbf{if} (\(\sign(t_1) \in \{\posop,\negop\}\)) - \(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\sign(t_1)~\bnds)\); \\ - \> \> \> \> \textbf{else} - \(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\ - \> \> \> \textbf{case} \(\texttt{div}\): - \(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\iboth)\); - \(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\ - \> \> \> \textbf{endswitch} \\ - \> \> \> \textbf{if} (\(a \not\equiv \texttt{div} \vee \ctxt = \rootc\)) - \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2), a(v_1,v_2,\new v) \}\) \\ - %\> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge - %\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}\) \\ - \> \> \> \textbf{else} - \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge - \new b'), b' \half \texttt{div}(v_1,v_2,\new v), \}\) \\ - \> \> \textbf{case} \([t_1, \ldots, t_n]\) \texttt{[} \(t_{0}\) \texttt{]}: \\ - \> \> \> - \textbf{foreach}(\(j \in 0..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\ - %\>\> \> \(S\) := - %\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), - %\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n], \new v), - %b' \full v_0 \in \{1,...,n\} \}\) - %\\ - \>\>\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{\new b, \texttt{element}(v', [v_1, \ldots, v_n], - \new v) \}\) \\ - \>\>\> \textbf{else} \\ - \>\>\>\> \(S\) \cupp - \(\{ \new b \half (\new b' \wedge \bigwedge_{j=0}^n b_j), - b' \half \texttt{element}(v_0, [v_1, \ldots, v_n], \new v), \} \) - \\ - \> \> \textbf{case} \texttt{sum(} \(\mathit{ia}\) \texttt{)}: \\ - \> \> \> \textbf{let} \([t_1, \ldots, t_n] = \evalb(ia)\); \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := - \(\halft(t_j,\ctxt,\bnds)\); \\ - \>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j, - \new v = \sum_{j=1}^n v_j \}\) \\ - %\> \> \> - %\(\tuple{v,b}\) := \flatt( - %\textsf{foldl}(\(\evalb(ia)\), \texttt{0}, \texttt{+}), \(\ctxt\)) - %\\ - \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(t_1\) \texttt{else} - \(t_2\) \texttt{endif}: - \\ \> \> \> - \textbf{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\halft(t_1,\ctxt,\bnds)\) \textbf{else} - \(\tuple{v,b}\) := \(\halft(t_2,\ctxt,\bnds)\) - \\ - \>\> \textbf{case} \texttt{bool2int(} \(c_0\) \texttt{)}: \\ - \> \> \> \textbf{if} \((\bnds = \ibelow\)) \(b_0\) := \(\halfc(c_0, \pos)\); \\ - \> \> \> \textbf{elseif} \((\bnds = \iabove\)) \(b'_0\) := \(\halfnc(c_0, - \pos)\); \(S\) \cupp \(\{\new b_0 \full \neg b'_0\}\) \\ - \> \> \> \textbf{else} \(b_0\) := \(\flatc(c_0, \mix)\); \\ - \> \> \> \(S\) \cupp \(\{ \texttt{bool2int}(b_0, \new v), \new b \}\) \\ - \>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): function \\ - \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\ - \>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\ - \> \> \> \textbf{if} (\(f\) is declared total) \(\ctxt' = \rootc\) \textbf{else} - \(\ctxt' = \ctxt\) \\ - \>\> \> \(\tuple{v,b'}\) := \(\halft(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt',\bnds)\) \\ - \> \> \> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n b_j \}\) - \\ - \>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(t_1\): \\ - \>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined - in \(d\) \\ - \> \> \> \(\tuple{c',t'}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true}, - t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ - \>\> \> \(\tuple{v,b_1}\) := \(\halft(t',\ctxt,\bnds)\); - \(b_2\) := \(\halfc(c',\ctxt)\); - \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2)\}\) - \\ - \> \> \textbf{endswitch} \\ - \> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ - \> hhash[\(t\)] := \(\tuple{v,b,\ctxt, \bnds}\) \\ - \> \textbf{return} \(\tuple{v,b}\) -\end{tabbing} - - -% Half reification of terms returns a set of constraints that enforce \(v = t\) if -% the term \(t\) is safe, and \(b \half v = t\) otherwise. The most complex case is -% \texttt{bool2int}\((c_1)\), which half-reifies \(c_1\) if it is in a positive -% context, negates \(c_1\) and half-reifies the result if \(c_1\) is safe and in a -% negative context, and uses full flattening otherwise. - -\begin{example}\label{ex:hr-half} - Now lets consider half reifying the expression of \cref{ex:hr-flat}. - - The result of flattening with half reification is: - - \begin{mzn} - constraint b0 -> b1 \/ b2; - constraint b0; - constraint b1 -> b2 /\ b1'; - constraint b1' -> v3 >= 4; - constraint b2 -> b4 /\ b5; - constraint b4 -> b8 /\ b9; - constraint b3 -> b6 /\ b7; - constraint minus(v6, v7, v3); - constraint b4 -> b8 /\ b9; - constraint b5 -> (b10 \/ b); - constraint b6 -> b11 /\ b12; - constraint plus(v11, v12, v6); - constraint b7; - constraint bool2int(b13, v7); - constraint b13 <-> not b10; - constraint b8 -> b11 /\ b8'; - constraint b8' -> v11 <= 2; - constraint b9 -> x > y; - constraint b10 -> x <= z; - constraint b11 -> b11'; - constraint b11' -> element(x, a, v11); - constraint b12; - constraint bool2int(b9, v12); - \end{mzn} - - Note that again we use CSE to reuse variables from position 11 for position - 14, position 9 for position 15, and position 10 for position 13. - - Half reification is significantly different from full reification in the - treatment of the partial function array access, as well as the treatment of - the negated context at 10 and 13. The bounds analysis finds the positions 1, - 3, 6, 11 are only interested in upper bounds, while positions 7 and 14 are - only interested in lower bounds. This means that the positions 13 and 15 are - reified using \halfnc{} and \halfc{} respectively even though they occur under - a \(bool2int\). \pjs{explain more!} - - We can simplify the resulting formulae by removing always true literals and - replacing literals \(b'\), which only occur in chains \(b'' \half b'\), - \(b' \half e_1\), \(b' \half e_2\) etc, by \(b''\) resulting in - - \begin{mzn} - constraint b1 \/ b2; - constraint b1 -> v3 >= 4; - constraint minus(v6, v7, v3); - constraint b2 -> b9; - constraint b2 -> (b10 \/ b); - constraint b1 -> b11; - constraint plus(v11, v12, v6); - constraint bool2int(b13, v7); - constraint b13 <-> not b10; - constraint b2 -> b11 /\ b8'; - constraint b8' -> v11 <= 2; - constraint b9 -> x > y; - constraint b10 -> x <= z; - constraint b11 -> element(x, a, v11); - constraint bool2int(b9, v12); - \end{mzn} - - with 15 primitive constraints and 12 intermediate variables. This reduces the - number of constraints by 3 and the number of intermediate variables by 2. -\end{example} - -\pjs{Extend and add section in implementation} As presented the half reification -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 -\(b \half b_1, b \half b_2, \ldots, b \half b_n\). Just as in \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 \(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\). - -\subsection{Full Reification using Half Reification} - -Usually splitting a propagator into two will reduce the propagation strength. We -show that modelling \(b \full c\) for primitive constraint \(c\) using -half-reified propagators as \(b \half c, b \full \neg b', b' \half \neg c\) does -not do so.%lose propagation strength. - -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. - -\[ - \begin{array}{rcll} - 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),~\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} - \end{array} -\] - -and - -\[ - \begin{array}{rcll} - 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 \{ \mzninline{false}\} & \text{otherwise} \\ - 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} - \end{array} -\] - -These definitions are not meant describe implementations, only to define how the -half reified split versions of the propagator should act. - -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 -follows: suppose \(f_{b \full c}(D)(v) \neq D(v), v \not\equiv b\), then -\(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 \(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 a very weak assumption, every -implementation of reified constraints we are aware of satisfies this property, -and indeed only a deliberately inaccurate propagator would not. - -For the sake of simplicity of proving the following theorem we also assume -\(f_{b \full c}\) is an \emph{idempotent} propagator, that is forall -\(D \sqsubseteq D_{init}\): -\(f_{b \full c}(D) = f_{b \full c}(f_{b \full c}(D))\). We assume the propagator -\(f_{b' \full \neg b}\) is domain consistent, which is the usual case for such a -trivial propagator. - -% Define -% \(f_{b \half c}(D) =_{vars(b \full c)} solv(\{f_{b'' \full c}, f_{b \half b''} \}, D)\), -% that is the half-reified version propagates on all variables only in the -% forward direction of the implication, by introducing the hidden variable -% \(b''\) which prevents propagation in the other direction. We assume a domain -% consistent propagator for \(b \half b''\). Similarly define -% \(f_{b' \half \neg c}(D) =_{vars(b' \full c)} solv(\{f_{b''' \full c}, f_{b' \half \neg b'''} \}, D)\) - -\jip{There is a proof here, but I don't have a proof environment yet} -% \begin{theorem} -% \(\forall D. solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D) = solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)\). -% \end{theorem} -% \begin{proof} -% Let \(V = vars(c)\). First w.l.o.g. we only consider domains \(D\) at a fixpoint -% of the propagators \(f_{b' \full \neg b}\), i.e. -% \(D(b') = \{ \neg d ~|~ d \in D(b)\}\), since both \(solv\) expressions include -% \(f_{b' \full \neg b}\). Let -% \(D' = solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D)\), now since -% \(f_{b \full c}\) and \(f_{b' \full \neg b}\) are idempotent and \(D\) is a fixpoint -% of \(f_{b' \full \neg b}\), then \(D' = f_{b' \full \neg b}(f_{b \full c}(D))\). -% Let -% \(D'' = solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)\). -% The proof is by cases of \(D\). - -% \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 -% 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 -% that \(f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}\). \textbf{(a-ii)} Suppose -% \(f_{b \full c}(D)(b) = \{ \mzninline{true} \}\). Let \(D_1 = f_{b' \half \neg c}(D)\), then -% \(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)= \{ \mzninline{true} \}\) and -% \(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 -% idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and -% \(b'\) this is a fixpoint of \(f_{b \full c}\) and -% \(D_3(v) = f_{b \full c}(D)(v), v \not \equiv b'\). \(D_3\) is also a fixpoint of -% \(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_3\) and \(f_{b \full c}(D)\) only differ on \(b'\). \textbf{(a-iii)} Suppose -% \(f_{b \full c}(D)(b) = \{ \mzninline{false} \}\). Let \(D_1 = f_{b \half c}(D)\), then -% \(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')= \{ \mzninline{true} \}\) and -% \(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 -% idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and -% \(b'\) this is a fixpoint for \(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_3\) and -% \(f_{b \full c}(D)\) only differ on \(b'\). - -% \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)\). - -% \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 -% \(vars(c)\). \qed -% \end{proof} - -The reason for the generality of the above theorem which defines the -half-reified propagation strength in terms of the full reified propagator is -that we can now show that for the usual notions of consistency, replacing a -fully reified propagator leads to the same propagation. - -Note that the additional variable \(b'\) can be implemented as a view -\autocite{schulte-2005-views} in the solver and hence adds no overhead. - -\jip{The corollary environment is also missing} -% \begin{corollary} -% A domain (resp. bounds(Z), bounds(R)) consistent propagator for \(b \full c\) -% propagates identically to domain (resp. bounds(Z), bounds(R)) consistent -% propagators for \(b \half c\), \(b \full \neg b'\), \(b' \half \neg c\). \qed -% \end{corollary} - - -\section{Propagation and Half Reification} - -\pjs{What happens to this section?} A propagation engine gains certain -advantages from half-reification, but also may suffer certain penalties. 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 half -reification. This is advantageous, but a corresponding disadvantage is that -variables that are fixed can allow the simplification of the propagator, and -hence make its propagation faster. - -When full reification is applicable (where we are not using half reified -predicates) an alternative to half reification is to implement full reification -\(b \full c\) by two half reified propagators -\(b \half c, b' \half \neg c, b' \full \neg b\). This does not lose propagation -strength. For Booleans appearing in a positive context we can make the the -propagator \(b' \half \neg c\) run at the lowest priority, since it will never -cause failure. Similarly in negative contexts we can make the propagator -\(b \half c\) run at the lowest priority. This means that Boolean variables are -still fixed at the same time, but there is less overhead. - - -\section{Implementation in the \glsentrytext{minizinc} Distribution} - -Implementing half-reification within the \minizinc\ distribution consists of two -parts: the \minizinc\ compiler needs to be extended with an implementation of -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 -appended with definitions for the predicates that are half-reified. Because the -\minizinc\ language allows for the definition of new predicates, we allow any -predicate to have an implemented half-reification, not just the predicates -defined as \flatzinc\ builtins. - -The implementation of half-reification in \minizinc\ requires little change to -the translator. As the translator was already aware of the context of -expressions, we can track the context of each expression using annotations to -the expressions, which are native to the \minizinc\ language. Through the use of -common subexpression elimination, we use the same generated \flatzinc\ for the -same expression and are able to update the context annotation if it should be -required. In the translator, reifications are delayed until the full model is -flattened because further processing might reveal that a constraint might not -need to be reified. Because of this delay, we know that if a reification still -has a positive context annotation, then we can use a half-reified version of -that constraint if it is available without having both a fully reified version -and a half-reified version of the same constraint. Note that this might not be -true if the flattening of the reifications requires the addition of a full -reification of which a half-reified version was already used. Because this -situation is so uncommon, no solution for this situation is implemented. Our -implementation currently does not implement the transformations shown in -\halfnc\, which push down negations to avoid negative context. Although this -would likely improve number of possible half-reifications, we believe that the -positive effects of half-reifications will already be noticeable without this -optimisation. - -Our implementation currently targets various linear solvers, including Gurobi -\autocite{gurobi-2021-gurobi} and Cbc (Coin-or branch and cut) -\autocite{lougee-heimer-2003-coin}, and Gecode \autocite{gecode-2021-gecode}. -Adding support for half-reification to the solver's \minizinc\ library can be -done in multiple ways: half-reified predicates can be be declared as solver -builtins, a redefinition using the \minizinc\ language can be provided for the -half-reified constraint, or a combination of the two can be used. Because Gecode -has propagators for half-reified constraints we have declared the corresponding -predicates as solver builtins. Gecode provides half-reified propagators for -almost all \flatzinc\ builtins. The other targeted solvers use the linear -library. The linear library \jip{,as seen before + reference???,} already has -redefinition for their fully reified predicates, \mzninline{b <-> c}. These -generally consist of two parts which are equivalent to the implications -\mzninline{b -> c /\ not b -> not c}. Because of this, the implementations of -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 -added half-reified versions for all predicates for which a full reification was -provided. - -\subsection{Implication Chain Compression} - -As shown in \cref{ex:hr-half}, flattening with half reification will in many -cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where -\texttt{b2} has no other occurrences. In this case the conjunction can be -replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the model. -The case shown in the example can be generalised to \mzninline{b1 -> b2 /\ - forall(i in N)(b2 -> c[i])}, which, if \texttt{b2} has no other usage in the -instance, can be resolved to \mzninline{forall(i in N)(b1 -> c[i])} after which -\texttt{b1} can be removed from the model. - -An algorithm to remove these chains of implications is best visualised through -the use of an implication graph. An implication graph \(\tuple{V,E}\) is a -directed graph where the vertices \(V\) represent the variables in the instance -and an edge \(\tuple{x,y} \in E\) represents the presence of an implication -\mzninline{x -> y} in the instance. Additionally, for the benefit of the -algorithm, a vertex is marked when it is used in other constraints in the -constraint model. The goal of the algorithm is now to identify and remove -vertices that are not marked and have only one incoming edge. The following -pseudo code provides a formal specification for this algorithm. - -\newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~} -\begin{tabbing} - xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill - \textsf{compress}(\(V\), \(E\)) \\ - \> \textbf{foreach} (\(x \in V\)) \\ - \> \> \textbf{if} \(|\{\tuple{a,x}| \tuple{a,x} \in E\}| = 1\) \(\land\) \(\lnot\) marked(\(x\)) \\ - \> \> \> \textbf{foreach} (\(\tuple{x, b} \in E\)) \\ - \> \> \> \> \(E\) \cupp \(\{ \tuple{a,b} \}\) \\ - \> \> \> \> \(E\) \setminusp \(\{ \tuple{x,b} \}\) \\ - \> \> \> \(E\) \setminusp \(\{\tuple{a,x}\}\) \\ - \> \> \> \(V\) \setminusp \(\{x\}\) \\ -\end{tabbing} - -\jip{Here we could actually show an example using a drawn graph} - -The algorithm can be further improved by considering implied conjunctions. These -can be split up into multiple implications: \mzninline{b -> forall(i in - N)(bs[i])} is equivalent to \mzninline{forall(i in N)(b -> bs[i])}. This -transformation both simplifies a complicated constraint and possibly allows for -the further compression of implication chains. It should however be noted that -although this transformation can result in an increase in the number of -constraints, it generally increases the propagation efficiency. - -To adjust the algorithm to simplify implied conjunctions more introspection from -the \minizinc\ compiler is required. The compiler must be able to tell if a -variable is (only) a control variable of a reified conjunction and what the -elements of that conjunction are. In the case where a variable has one incoming -edge, but it is marked as used in other constraint, we can now check if it is -only a control variable for a reified conjunction and perform the transformation -in this case. - -\section{Experiments} - -We ran our experiments on a server cluster using an Intel Xeon 8260. Each run -had exclusive access to 1 core of the CPU and 4 GB of RAM\@. The experiments are -available \jip{Insert new link} has our experimental \minizinc\ instances and -the infrastructure that performs the benchmarks. - -The first experiment considers ``QCP-max'' problems which are defined as -quasi-group completion problems where the \mzninline{all_different} constraints -are soft, and the aim is to satisfy as many of them as possible. - -\begin{mzn} -int: n; % size -array[1..n,1..n] of 0..n: s; % 0 = unfixed 1..n = fixed - -array[1..n,1..n] of var 1..n: q; % qcp array; - -constraint forall(i,j in 1..n where s[i,j] > 0)(q[i,j] = s[i,j]); - -solve maximize - sum(i in 1..n)(bool2int(all_different([q[i,j] | j in 1..n]))) + - sum(j in 1..n)(bool2int(all_different([q[i,j] | i in 1..n]))); - -predicate all_different(array[int] of var int: x) = - forall(i,j in index_set(x) where i < j)(x[i] != x[j]); -\end{mzn} - -Note that this is not the same as requiring the maximum number of disequality -constraints to be satisfied. The \mzninline{all_different} constraints, while -apparently in a mixed context, are actually in a positive context, since the -maximisation in fact is implemented by inequalities forcing at least some number -to be true. - -In \cref{tab:hr-qcp} we compare three different resulting programs on QCP-max -problems: full reification of the model above, using the -\mzninline{all_different} decomposition defined by the predicate shown -(\textsf{full}), half reification of the model using the -\mzninline{all_different} decomposition (\textsf{half}), and half reification -using a half-reified global \mzninline{all_different} (\textsf{half-g}) -implementing arc consistency (thus having the same propagation strength as the -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. -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 -labeling the matrix in order left-to-right from highest to lowest value for all -approaches to minimize differences in search. - -\begin{table} [tb] \begin{center} - \caption{\label{tab:hr-qcp} QCP-max problems: - Average time (in seconds), number of solved instances (300s timeout).} - \begin{tabular}{|l||rr|rr|rr|} - \hline - Instances & \multicolumn{2}{c|}{\textsf{half-g}} & \multicolumn{2}{c|}{\textsf{half}} & \multicolumn{2}{c|}{\textsf{full}} \\ - \hline - \texttt{qcp-10} (x15) & 17.12 & 15 & 21.17 & 14 & 21.09 & 14 \\ - \hline - \texttt{qcp-15} (x15) & 40.35 & 13 & 40.52 & 13 & 40.55 & 13 \\ - \hline - \texttt{qcp-20} (x15) & 27.50 & 14 & 64.05 & 14 & 65.55 & 14 \\ - \hline - \texttt{qcp-25} (x15) & 195.85 & 6 & 223.44 & 6 & 225.22 & 6 \\ - \hline - \end{tabular} - \end{center} -\end{table} - -\jip{adjust text to match new table}Half reification of the decomposition is -more efficient, principally because it introduces fewer Boolean variables, and -the direct implementation of the half reified constraint is more efficient -still. Note that learning can be drastically changed by the differences in the -model and \textsf{full} solves one more instance in \texttt{qcp-20}, thus -winning in that case. Apart from this instance, the half reified versions give -an almost uniform improvement. - -The second experiment shows how half reification can reduce the overhead of -handling partial functions correctly. Consider the following model for -determining a prize collecting path, a simplified form of prize collecting -travelling salesman problem -\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 -collect the most weight. Not every node needs to be visited (\(pos[i] = 0\)). - -\begin{mzn} -int: n; % size -array[1..n,0..n] of int: p; % prize for edge (i,j), p[i,0] = 0 - -array[1..n] of var 0..n: next; % next posn in tour -array[1..n] of var 0..n: pos; % posn on node i in path, 0=notin -array[1..n] of var int: prize = [p[i,next[i]] | i in 1..n]; - % prize for outgoing edge - -constraint forall(i in 1..n)( - (pos[i] = 0 <-> next[i] = 0) /\ - (next[i] > 1 -> pos[next[i]] = pos[i] + 1)); - -include "alldifferent_except_0.mzn"; -constraint alldifferent_except_0(next) /\ pos[1] = 1; - -solve minimize sum(i in 1..n)(prize[i]); -\end{mzn} - -It uses the global constraint \mzninline{alldifferent_except_0} which constrains -each element in the \mzninline{next} array to be different or equal 0. The model -has one unsafe array lookup \mzninline{pos[next[i]]}. We compare using full -reification (\textsf{full}) and half reification (\textsf{half}) to model this -problem. Note that if we extend the \(pos\) array to have domain \(0..n\) then the -model becomes safe, by replacing its definition with the following two lines - -\begin{mzn} - array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin - constraint pos[0] = 0; -\end{mzn} - -We also compare against this model (\textsf{extended}). - -We use graphs with both positive and negative weights for the tests. The search -strategy fixes the \mzninline{next} variables in order of their maximum value. -First we note that \textsf{extended} is slightly better than \textsf{full} -because of the simpler translation, while \textsf{half} is substantially better -than \textsf{extended} since most of the half reified \texttt{element} -constraints become redundant. Learning increases the advantage because the half -reified formulation focuses on propagation which leads to failure which creates -more reusable nogoods. - -\begin{table} [tb] \begin{center} - \caption{\label{tab:hr-pctsp} Prize collecting paths: Average time (in seconds) - and number of solved instances with a 300s timeout for various number of - nodes.} - \begin{tabular}{|l||rr|rr|rr||rr|rr|rr|} - \hline - & \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\ - Nodes & - \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} & - \multicolumn{2}{|c|}{\textsf{extended}} & \multicolumn{2}{|c|}{\textsf{full}} & - \multicolumn{2}{|c|}{\textsf{half}} & \multicolumn{2}{|c|}{\textsf{extended}} - \\ - \hline - 15-3-5 (x 10) & 0.31 & 10 & 0.25 & 10 & 0.26 & 10 & 0.21 & 10 & 0.17 & 10 & 0.17 & 10 \\ - \hline - 18-3-6 (x 10) & 1.79 & 10 & 1.37 & 10 & 1.52 & 10 & 0.70 & 10 & 0.51 & 10 & 0.58 & 10 \\ - \hline - 20-4-5 (x 10) & 5.30 & 10 & 4.04 & 10 & 4.51 & 10 & 1.28 & 10 & 0.97 & 10 & 1.17 & 10 \\ - \hline - 24-4-6 (x 10) & 46.03 & 10 & 34.00 & 10 & 40.06 & 10 & 7.28 & 10 & 4.91 & 10 & 6.37 & 10 \\ - \hline - 25-5-5 (x 10) & 66.41 & 10 & 50.70 & 10 & 57.51 & 10 & 9.75 & 10 & 6.58 & 10 & 8.28 & 10 \\ - \hline - 28-4-7 (x 10) & 255.06 & 5 & 214.24 & 8 & 241.10 & 6 & 38.54 & 10 & 23.27 & 10 & 34.83 & 10 \\ - \hline - 30-5-6 (x 10) & 286.48 & 1 & 281.00 & 2 & 284.34 & 1 & 100.54 & 10 & 60.65 & 10 & 92.19 & 10 \\ - \hline - 32-4-8 (x 10) & 300.00 & 0 & 297.12 & 1 & 300.00 & 0 & 229.86 & 5 & 163.73 & 10 & 215.16 & 8 \\ - \hline - - %15-3-5 (x 10) & 0.31&10& 0.31&10& 0.26&10 & 0.21&10 & 0.19&10 & 0.17&10 \\ - %\hline - %18-3-6 (x 10) & 1.79&10& 1.77&10& 1.52&10 & 0.70&10 & 0.57&10 & 0.58&10 \\ - %\hline - %20-4-5 (x 10) & 5.30&10& 5.31&10& 4.51&10 & 1.28&10 & 1.13&10 & 1.17&10 \\ - %\hline - %24-4-6 (x 10) & 46.03&10& 47.43&10& 40.06&10 & 7.28&10 & 6.00&10 & 6.37&10 \\ - %\hline - %25-5-5 (x 10) & 66.41&10& 70.03&10& 57.51&10 & 9.75&10 & 8.57&10 & 8.28&10 \\ - %\hline - %28-4-7 (x 10) & 255.06&5& 260.79&5& 241.10&6 & 38.54&10 & 28.05&10 & 34.83&10 \\ - %\hline - %30-5-6 (x 10) & 286.48 &0& 287.33 &0& 284.34 &0 & 100.54&10 & 83.50&10 & 92.19&10 \\ - %\hline - %32-4-8 (x 10) & 300.00 &0& 300.00 &0& 300.00 &0 & 229.86&5 & 187.40&9 & 215.16&8 \\ - %\hline - \end{tabular} - \end{center} -\end{table} - -In the final experiment we compare resource constrained project scheduling -problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task -decomposition as in \cref{ex:hr-cumul} above, using both full reification and -half-reification. We use standard benchmark examples from PSPlib -\autocite{kolisch-1997-psplib}. \Cref{tab:hr-rcpsp} compares RCPSP instances -using \textsf{full} reification and \textsf{half} reification. We compare using -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 -solved instances. The search strategy tries to schedule the task with the -earliest possible start time. We find a small and uniform speedup for -\textsf{half} over \textsf{full} across the suites, which improves with -learning, again because learning is not confused by propagations that do not -lead to failure. - -\begin{table} [tb] \caption{\label{tab:hr-rcpsp} RCPSP: - Average time (in seconds) and number of solved instances with a 300s timeout.} - \begin{center} - \begin{tabular}{|l||rr|rr||rr|rr|} - \hline - & \multicolumn{4}{|c||}{FD} & \multicolumn{4}{|c|}{FD + Explanations} \\ - Instances & - \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} - & \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} \\ - \hline - BL (x 40) & 277.2 & 5 & 269.3 & 5 & 17.1 & 39 & 15.4 & 39 \\ - \hline - J30 (x 480) & 116.1 & 300 & 114.3 & 304 & 16.9 & 463 & 12.9 & 468 \\ - \hline - \end{tabular} - \end{center} -\end{table} - -\subsection{MiniZinc Challenge} - -To verify the effectiveness of the half reification implementation within the -\minizinc{} distribution we compare the results of the current version of the -\minizinc{} translator (rev. \jip{add revision}) against the equivalent version -for which we have implemented half reification. We use the model instances used -by the \minizinc{} challenges -\autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2019 and 2020. The -performance of the generated \flatzinc{} models will be tested using Gecode, -flattened with its own library, and Gurobi and CBC, flattened with the linear -library. - -\begin{table} [tb] - \caption{\label{tab:hr-flat-results} Flattening results: Average changes in the - generated the \flatzinc{} models} - \begin{center} - \begin{tabular}{|l|r||r|r|r||r|} - \hline - Library & Nr. Instances & Full Reifications - & Constraints & Variables & Chains Compressed \\ - \hline - Gecode & 274 & -38.19\% & -6.29\% & -8.66\% & 21.35\% \\ - \hline - Linear & 346 & - 33.11\% & -13.77\% & -3.70\% & 11.63\% \\ - \hline - \end{tabular} - \end{center} -\end{table} -\jip{Better headers for \cref{tab:hr-flat-results} and update with current results} - -\Cref{tab:hr-flat-results} shows the average change on the number of full -reification, constraints, and variables between the \flatzinc\ models generated -by the different versions of the translator using the different libraries. We -find that the number full reifications is reduced by a significant amount. -Together with the chain compression mechanism this has a positive effect on the -number of constraints and the number of variables. - -\jip{Add something regarding the chain compression. Is this the right - statistic? (Compressions in terms of reifications)} - -We ran our experiments on a computer with a 3.40GHz Intel i7-3770 CPU and 16Gb -of memory running the Ubuntu 16.04.3 LTS operating system. - -\jip{Scatter plot of the runtimes + discussion!} - -%=============================================================================% -\section{Related Work and Conclusion}\label{sec:hr-conclusion} -%=============================================================================% - -Half reification on purely Boolean constraints is well understood, this is the -same as detecting the \emph{polarity} of a gate, and removing half of the -clausal representation of the circuit (see \eg\ -\autocite{plaisted-1986-polarity}). The flattening of functions (partial or -total) and the calculation of polarity for Booleans terms inside -\texttt{bool2int} do not arise in pure Boolean constraints. - -Half reified constraints have been used in constraint modelling but are -typically not visible as primitive constraints to users, or produced through -flattening. Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to -implement reified constraints by specifying how to propagate a constraint, -propagate its negation, check disentailment, and check entailment, and this is -implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A half reified -propagator simply omits entailment and propagating the negation. - -Half reified constraints appear in some constraint systems, for example SCIP -\autocite{gamrath-2020-scip} supports half-reified real linear constraints of -the form \mzninline{b -> sum(i in N)(a[i] * x[i]) <= C} exactly because the -negation of the linear constraint \mzninline{sum(i in N)(a[i] * x[i]) > C} is -not representable in an LP solver so full reification is not possible. - -While flattening is the standard approach to handle complex formula involving -constraints, there are a number of other approaches which propagate more -strongly. Schulte proposes a generic implementation of \mzninline{b <-> c} -propagating (the flattened form of) \mzninline{c} in a separate constraint space -which does not affect the original variables \autocite*{schulte-2000-deep}; -entailment and disentailment of \mzninline{c} fix the \mzninline{b} variable -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 -Yap define an approach to propagating complex constraint formulae called -controlled propagation which ensures that propagators that cannot affect the -satisfiability are not propagated \autocite*{brand-2006-propagation}. They note -that for a formula without negation, they could omit half their control rules, -corresponding to the case for half reification of a positive context. Jefferson -et al.\ similarly define an approach to propagating positive constraint formulae -by using watch literal technology to only wake propagators for reified -constraints within the formula when they can affect the final result -\autocite*{jefferson-2010-connectives}. They use half reified propagators, which -they call the ``reifyimplied'' form of a constraint, in some of their constraint -models, though they do not compare half reified models against full reified -models. We can straightforwardly fit these stronger propagation approaches to -parts of a constraint formula into the flattening approach by treating the whole -formula as a predicate, and the implementation of the stronger propagation as -its propagator. - -A passing contribution of this paper is a much simpler approach to enforcing the -relational semantics, by combining the ``safening'' of expressions with -flattening. The original approach of \autocite{frisch-2009-undefinedness} is a -source to source transformation without flattening and substantially more -complex. - -We suggest that all finite domain constraint solvers should move to supporting -half-reified versions of all constraints. This imposes no further burden on -solver implementors, it allows more models to be solved, it can be used to -implement full reification, and it can allow translation to more efficient -models.