%************************************************
\chapter{Context Analysis and Half Reification}\label{ch:half-reif}
%************************************************

In this chapter we study the usage of \gls{half-reif}. When a constraint \mzninline{pred(...)} is reified a


\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(....)} 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}%
\label{sec:half-propagation}

\begin{itemize}
      \item custom implemented half-reified propagations.
      \item benefits
      \item downside
      \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 \mzninline{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 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}
            \changeneg \rootc & = & \negc \\
            \changeneg \posc  & = & \negc \\
            \changeneg \negc  & = & \posc \\
            \changeneg \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}

\begin{itemize}
      \item cse
      \item chain compression
\end{itemize}