Work on HR

assets/glossary.tex

@@ -169,6 +169,11 @@
   description={},
 }
 
+\newglossaryentry{half-reif}{
+  name={half reification},
+  description={},
+}
+
 \newglossaryentry{indicator-var}{
   name={indicator variable},
   description={},

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}}

chapters/4_half_reif.tex

@@ -2,14 +2,23 @@
 \chapter{Context Analysis and Half Reification}\label{ch:half-reif}
 %************************************************
 
-\section{Context Analysis}%
+In this chapter we study the usage of \gls{half-reif}. When a constraint \mzninline{pred(...)} is reified a
-\label{sec:half-context}
+
 
 \begin{itemize}
-  \item What (again) are the contexts?
+  \item Flattening with half reification can naturally produce the relational
-  \item Why are they important
+        semantics when flattening partial functions in positive contexts.
-  \item When can we use half-reification
+  \item Half reified constraints add no burden to the solver writer; if they
-  \item How does the analysis work?
+        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}
 

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
+\(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
+\(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
+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
+\( 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
+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,
+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
+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
+\(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),
+\> \> \> \(S\) := \(S \cup \{ \new v' \in dom(a),
-b' \full v \in \dom(a), b' \full v = v',
+b' \full v \in dom(a), b' \full v = v',
 \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