2568 lines
124 KiB
TeX
2568 lines
124 KiB
TeX
%************************************************
|
|
\chapter{TEMP: Half Reification Journal Paper}\label{ch:half-reif-journal}
|
|
%************************************************
|
|
%
|
|
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{<cons>} nonterminal defines constraints (Boolean terms),
|
|
\syntax{<term>} defines integer terms, \syntax{<barray>} defines Boolean arrays,
|
|
and \syntax{<iarray>} defines integer arrays:
|
|
|
|
\begin{grammar}
|
|
<cons> ::= "true" | "false" | <bvar> | <term> <relop> <term> | "not" <cons>
|
|
\alt <cons> "/\\" <cons> | <cons> "\\/" <cons> | <cons> "->" <cons> | <cons> "<->" <cons>
|
|
\alt "forall(" <barray> ")" | <barray> | <barray>"[" <term> "]"
|
|
| pred(<term>, \ldots, <term>)
|
|
\alt "if" <cons> "then" <cons> "else" <cons> "endif"
|
|
\alt "let" "{"<decls> <ocons> "}" "in" <cons>
|
|
|
|
<term> ::= <int> | <ivar> | <term> <arithop> <term> | <iarray>"[" <term> "]"
|
|
\alt "sum(" <iarray> ")" \alt "if" <cons> "then" <term> "else" <term> "endif"
|
|
\alt "bool2int(" <cons> ")" \alt "let" "{"<decls> <ocons> "}" "in" <term>
|
|
|
|
<barray> ::= "[" <cons>, \ldots, <cons> "]" \alt "["<cons> "|" <ivar> "in" <term> ".." <term> "]"
|
|
|
|
<iarray> ::= "[" <term>, \ldots, <term> "]" \alt "["<term> "|" <ivar> "in" <term> ".." <term> "]"
|
|
|
|
<relop> ::= "==" | "<=" | "<" | "!=" | ">=" | ">"
|
|
|
|
<arithop> ::= "+" | "-" | "*" | "div"
|
|
\end{grammar}
|
|
|
|
The grammar uses the symbols \syntax{<bvar>} for Boolean variables,
|
|
\syntax{<pred>} for names of predicates, \syntax{<int>} for integer constants,
|
|
and \syntax{<ivar>} for integer variables.
|
|
|
|
In the \texttt{let} constructs we make use of the nonterminal \syntax{<decls>}
|
|
for declarations. We define this below using \syntax{<idecls>} for integer
|
|
variable declarations, \syntax{<bdecls>} for Boolean variable declarations. We
|
|
use \syntax{<ocons>} for optional constraint items appearing in let
|
|
declarations. We also define \syntax{<args>} as a list of integer variable
|
|
declarations, an \syntax{<fndecl>} as either a predicate declaration or a
|
|
function declaration, \syntax{<solve>} as a solve directive either satisfaction
|
|
or an objective, and a model \syntax{<model>} as some declarations followed by
|
|
items followed by a solve item. Note that \syntax{<empty>} represents the empty
|
|
string.
|
|
|
|
\begin{grammar}
|
|
<idecl> ::= "int" ":" <ivar> | "var" "int" ":" <ivar> | "var" <term> ".." <term> ":" <ivar>
|
|
|
|
<bdecl> ::= "bool" ":" <ivar> | "var" "bool" ":" <ivar>
|
|
|
|
<decls> ::= <idecls> [ "=" <term>] ";" <decls> | <bdecls> [ "=" <cons>] ";" <decls> | <empty>
|
|
|
|
<ocons> ::= "constraint" <cons> ";" <ocons> | <empty>
|
|
|
|
<args> ::= "int" ":" <ivar> ["," <args>] | "var" "int" ":" <ivar> ["," <args>]
|
|
|
|
<fndecl> ::= "predicate" <pred> "(" <args> ")" "=" <cons> ";"
|
|
\alt "function" "var" "int" ":" <func> "(" <args> ")" "=" <term> ";"
|
|
|
|
<solve> ::= "satisfy" | "maximize" <term> | "minimize" <term>
|
|
|
|
<model> ::= <fndecl>* <decls> <ocons> "solve" <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{<cons>} term defining the constraints of the model we can split
|
|
its \syntax{<cons>} 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{<bvar>}): \(b\) := \(b'\); \\
|
|
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}): \\
|
|
\>\>\> \(\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{<pred>}) 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{<pred>}): 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{<ivar>}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\
|
|
\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}): \\
|
|
\> \> \>
|
|
\(\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{<func>}): 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{<bvar>}): \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{<pred>}): \\
|
|
% \> \> \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{<ivar>}): \textbf{return} \(\{ v = v' \}\) \\
|
|
% \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}):
|
|
% \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{<bvar>}): \(b\) := \(b'\); \\
|
|
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}): \\
|
|
\> \> \> \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{<pred>}) 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{<pred>}): 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{<bvar>}): \(S\) \cupp \(\{\new b \half \neg b'\}\); \\
|
|
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}): \\
|
|
\> \> \> \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{<pred>}) built-in predicate: \\
|
|
\> \> \> \(b\) := \(\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)\) \\
|
|
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}): user-defined predicate \\
|
|
\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\
|
|
\> \> \> \textbf{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{<ivar>}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\
|
|
\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}): \\
|
|
\> \> \> \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{<func>}): 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.
|