diff --git a/assets/glossary.tex b/assets/glossary.tex index 2b3e895..14b52b5 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -169,6 +169,11 @@ description={}, } +\newglossaryentry{half-reif}{ + name={half reification}, + description={}, +} + \newglossaryentry{indicator-var}{ name={indicator variable}, description={}, diff --git a/assets/shorthands.tex b/assets/shorthands.tex index 6671b95..ee55c30 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -18,7 +18,7 @@ \newcommand{\variable}{\gls{variable}\xspace{}} \newcommand{\zinc}{\gls{zinc}\xspace{}} - +% Semantic shorthands (rewriting) \renewcommand{\phi}{\varphi} \newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}} \newcommand{\Prog}{\ensuremath{\mathcal{P}}} @@ -27,54 +27,12 @@ \newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}} \newcommand{\Cbind}{\ensuremath{\wedge}} +% Context shorthands (half-reification) +\newcommand{\rootc}{\textit{root}} +\newcommand{\posc}{\textit{pos}} +\newcommand{\negc}{\textit{neg}} +\newcommand{\mixc}{\textit{mix}} +\newcommand{\changepos}{\ensuremath{+}} +\newcommand{\changeneg}{\ensuremath{-}} + \newcommand{\undefined}{\ensuremath{\bot}} - -% Half-reification math things - -\newcommand{\VV}{{\cal\ V}} -\newcommand{\PP}{{\cal\ P}} -\newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]} -\newcommand{\gfp}{\textup{gfp}} -\newcommand{\lfp}{\textup{lfp}} -\newcommand{\iter}{\mathit{iter}} - -\newcommand{\half}{\Rightarrow} -\newcommand{\full}{\Leftrightarrow} -\renewcommand{\half}{\rightarrow} -\renewcommand{\full}{\leftrightarrow} - -\newcommand{\entails}{\models} -\newcommand{\bigsqcap}{\mathop{\lower.1ex\hbox{\Large$\sqcap$}}} - -\DeclareMathOperator{\rules}{\mathit{rules}} -\DeclareMathOperator{\lazy}{\mathit{lazy}} -\DeclareMathOperator{\events}{\mathit{events}} -\DeclareMathOperator{\domain}{\mathit{domain}} -\DeclareMathOperator{\bc}{\mathit{bc}} -\DeclareMathOperator{\lbc}{\mathit{lbc}} -\DeclareMathOperator{\ubc}{\mathit{ubc}} -\DeclareMathOperator{\dmc}{\mathit{dmc}} -\DeclareMathOperator{\fix}{\mathit{fix}} -\DeclareMathOperator{\event}{\mathit{event}} -\DeclareMathOperator{\minassign}{\mathit{minassign}} -\DeclareMathOperator{\assign}{\mathit{assign}} -\DeclareMathOperator{\cl}{\mathit{cl}} -\DeclareMathOperator{\UP}{\mathit{UP}} -\DeclareMathOperator{\up}{\mathit{up}} -\DeclareMathOperator{\DOM}{\mathit{DOM}} -\DeclareMathOperator{\setb}{\mathit{sb}} -\DeclareMathOperator{\bnd}{\mathit{bnd}} -\DeclareMathOperator{\dsb}{\mathit{dsb}} -\DeclareMathOperator{\vars}{\mathit{vars}} -\DeclareMathOperator{\ivars}{\mathit{input}} -\DeclareMathOperator{\ovars}{\mathit{output}} - -\DeclareMathOperator{\solns}{\mathit{solns}} -\DeclareMathOperator{\solv}{\mathit{solv}} -\DeclareMathOperator{\isolv}{\mathit{isolv}} -\DeclareMathOperator{\conv}{\mathit{conv}} -\DeclareMathOperator{\ran}{\mathit{ran}} -\DeclareMathOperator{\ite}{\mathit{ite}} -\DeclareMathOperator{\VAR}{\mathit{VAR}} - -\DeclareMathOperator{\dom}{\mathit{idx}} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 60cdcf7..7293945 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -2,14 +2,23 @@ \chapter{Context Analysis and Half Reification}\label{ch:half-reif} %************************************************ -\section{Context Analysis}% -\label{sec:half-context} +In this chapter we study the usage of \gls{half-reif}. When a constraint \mzninline{pred(...)} is reified a + \begin{itemize} - \item What (again) are the contexts? - \item Why are they important - \item When can we use half-reification - \item How does the analysis work? + \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(....)} then they can + straightforwardly construct a half reified propagator for \mzninline{b + -> pred(...)}. + \item Half reified constraints \mzninline{b -> pred(...)} 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} \section{Propagation and Half Reification}% @@ -22,9 +31,58 @@ \item experimental results \end{itemize} +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 +\mzninline{x <-> pred(...)} by two half reified propagators \mzinline{x -> + pred(...)}, \mzninline{y \half \neg pred(...)}, \mzninline{x <-> not y}. This +does not lose propagation strength. For Booleans appearing in a positive context +we can make the the propagator \mzninline{y -> not pred(...)} run at the lowest +priority, since it will never cause failure. Similarly in negative contexts we +can make the propagator \mzninline{b -> pred(...)} run at the lowest priority. +This means that Boolean variables are still fixed at the same time, but there is +less overhead. + \section{Decomposition and Half Reification}% \label{sec:half-decomposition} +\section{Context Analysis}% +\label{sec:half-context} + +\begin{tabular}{ccc} +\( +\begin{array}{lcl} +\changepos \rootc & = &\posc \\ +\changepos \posc & =& \posc \\ +\changepos \negc & =& \negc \\ +\changepos \mixc & =& \mixc +\end{array} +\) +&~& +\( +\begin{array}{lcl} +\negop \rootc & = &\negc \\ +\negop \posc & = & \negc \\ +\negop \negc & = & \posc \\ +\negop \mixc & = & \mixc +\end{array} +\) +\end{tabular} + +\begin{itemize} + \item What (again) are the contexts? + \item Why are they important + \item When can we use half-reification + \item How does the analysis work? +\end{itemize} + + \section{Flattening and Half Reification}% \label{sec:half-flattening} diff --git a/chapters/A3_temp_hr.tex b/chapters/A3_temp_hr.tex index 86918e7..2b34d94 100644 --- a/chapters/A3_temp_hr.tex +++ b/chapters/A3_temp_hr.tex @@ -2,6 +2,56 @@ \chapter{TEMP: Half Reification Journal Paper}\label{ch:half-reif-journal} %************************************************ % +% Half-reification math things + +\newcommand{\VV}{{\cal\ V}} +\newcommand{\PP}{{\cal\ P}} +\newcommand{\range}[2]{\left[\,#1\,..\,#2\,\right]} +\newcommand{\gfp}{\textup{gfp}} +\newcommand{\lfp}{\textup{lfp}} +\newcommand{\iter}{\mathit{iter}} + +\newcommand{\half}{\Rightarrow} +\newcommand{\full}{\Leftrightarrow} +\renewcommand{\half}{\rightarrow} +\renewcommand{\full}{\leftrightarrow} + +\newcommand{\entails}{\models} +% \newcommand{\bigsqcap}{\mathop{\lower.1ex\hbox{\Large$\sqcap$}}} + +% \DeclareMathOperator{\rules}{\mathit{rules}} +% \DeclareMathOperator{\lazy}{\mathit{lazy}} +% \DeclareMathOperator{\events}{\mathit{events}} +% \DeclareMathOperator{\domain}{\mathit{domain}} +% \DeclareMathOperator{\bc}{\mathit{bc}} +% \DeclareMathOperator{\lbc}{\mathit{lbc}} +% \DeclareMathOperator{\ubc}{\mathit{ubc}} +% \DeclareMathOperator{\dmc}{\mathit{dmc}} +% \DeclareMathOperator{\fix}{\mathit{fix}} +% \DeclareMathOperator{\event}{\mathit{event}} +% \DeclareMathOperator{\minassign}{\mathit{minassign}} +% \DeclareMathOperator{\assign}{\mathit{assign}} +% \DeclareMathOperator{\cl}{\mathit{cl}} +% \DeclareMathOperator{\UP}{\mathit{UP}} +% \DeclareMathOperator{\up}{\mathit{up}} +% \DeclareMathOperator{\DOM}{\mathit{DOM}} +% \DeclareMathOperator{\setb}{\mathit{sb}} +% \DeclareMathOperator{\bnd}{\mathit{bnd}} +% \DeclareMathOperator{\dsb}{\mathit{dsb}} +% \DeclareMathOperator{\vars}{\mathit{vars}} +% \DeclareMathOperator{\ivars}{\mathit{input}} +% \DeclareMathOperator{\ovars}{\mathit{output}} + +% \DeclareMathOperator{\solns}{\mathit{solns}} +% \DeclareMathOperator{\solv}{\mathit{solv}} +% \DeclareMathOperator{\isolv}{\mathit{isolv}} +% \DeclareMathOperator{\conv}{\mathit{conv}} +% \DeclareMathOperator{\ran}{\mathit{ran}} +% \DeclareMathOperator{\ite}{\mathit{ite}} +% \DeclareMathOperator{\VAR}{\mathit{VAR}} + +% \DeclareMathOperator{dom}{\mathit{idx}} +% Discrete optimisation solvers solve constraint optimisation problems of the form \(\min o \text{~subject to~} \wedge_{c \in C} c\), that is minimising an objective \(o\) subject to an (existentially quantified) conjunction of @@ -244,12 +294,12 @@ correspondingly typed values, written % 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 +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)\). +\(v \in vars(\theta)\). %\paragraph{Constraints, Propagators and Propagation Solvers} @@ -261,7 +311,7 @@ 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))\}\) +\(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 @@ -269,7 +319,7 @@ We associate with every constraint \(c\) a \emph{propagator} \(f_c\). A propagat 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)\}\) +\(\{\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 @@ -316,11 +366,11 @@ A propagator \(f_c\) is \(X\)-consistent if \(f(D)\) is always \(X\) consistent 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 +\(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 +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, @@ -447,8 +497,8 @@ negative context, \mzninline{x + bool2int(b) = 5} is in a positive context, and 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, +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\), @@ -1215,8 +1265,8 @@ 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 +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. @@ -1235,10 +1285,10 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill 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', +\> \> \> \(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 +\> \> \> \%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' @@ -2054,27 +2104,27 @@ For the sake of simplicity of proving the following theorem we also assume trivial propagator. % Define -% \(f_{b \half c}(D) =_{vars(b \full c)} \solv(\{f_{b'' \full c}, f_{b \half b''} \}, D)\), +% \(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)\) +% \(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)\). +% \(\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 +% \(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 +% \(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)\). +% \(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