From a5c1fa012eb4640dfbca088a0698923eeac6044e Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 15 Mar 2021 11:54:53 +1100 Subject: [PATCH] Some work on half reification chapter --- Pipfile | 2 +- Pipfile.lock | 18 +- assets/packages.tex | 91 +++++- assets/shorthands.tex | 2 + chapters/4_rewriting.tex | 2 +- chapters/5_half_reif.tex | 669 ++++++++++++++++++--------------------- 6 files changed, 407 insertions(+), 377 deletions(-) diff --git a/Pipfile b/Pipfile index bd3486a..d09fd2d 100644 --- a/Pipfile +++ b/Pipfile @@ -4,7 +4,7 @@ verify_ssl = true name = "pypi" [packages] -tree-sitter-minizinc = {path = "/Users/dekker1/Code/github.com/Dekker1/tree-sitter-minizinc"} +tree-sitter-minizinc = {git = "https://github.com/Dekker1/tree-sitter-minizinc.git"} pygments = "*" [dev-packages] diff --git a/Pipfile.lock b/Pipfile.lock index 4175ebc..fd7ecaf 100644 --- a/Pipfile.lock +++ b/Pipfile.lock @@ -1,7 +1,7 @@ { "_meta": { "hash": { - "sha256": "5d0bd9f479dec0e41b809749ff8383832e28f12349cac501f086d673455a46c6" + "sha256": "dce9b5878ca21a8613ba71eed866396a1113aa9c8453b025e8eea89b90bc86ca" }, "pipfile-spec": 6, "requires": { @@ -18,23 +18,23 @@ "default": { "pygments": { "hashes": [ - "sha256:37a13ba168a02ac54cc5891a42b1caec333e59b66addb7fa633ea8a6d73445c0", - "sha256:b21b072d0ccdf29297a82a2363359d99623597b8a265b8081760e4d0f7153c88" + "sha256:2656e1a6edcdabf4275f9a3640db59fd5de107d88e8663c5d4e9a0fa62f77f94", + "sha256:534ef71d539ae97d4c3a4cf7d6f110f214b0e687e92f9cb9d2a3b0d3101289c8" ], "index": "pypi", - "version": "==2.8.0" + "version": "==2.8.1" }, "tree-sitter": { "hashes": [ - "sha256:15e7616f0e41127ca70880a40301a6ebfe58ce92db4f142eac775a38e9c38cec", - "sha256:2618b781b065d419237dcd234f7a7cd68920c4f15c6809a99ed2c2dfd6d15d01" + "sha256:03fd05fe099639d4aec1b59dec630a69d32e3d07a078d83bc060209a8dbb2132", + "sha256:861afcf39f957fdd75f8b93124bc403f2f3abe8b81f104c05b1a749e6dd33499" ], "markers": "python_version >= '3.3'", - "version": "==0.2.2" + "version": "==0.19.0" }, "tree-sitter-minizinc": { - "path": "/Users/dekker1/Code/github.com/Dekker1/tree-sitter-minizinc", - "version": "==0.1.dev35+gf70a60b" + "git": "https://github.com/Dekker1/tree-sitter-minizinc.git", + "ref": "d3ba544d2ffdb9babe0f6eaf117d259c05697791" } }, "develop": {} diff --git a/assets/packages.tex b/assets/packages.tex index e26d836..8d80607 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -8,7 +8,6 @@ % Fonts \usepackage{fontspec} -\usepackage{newunicodechar} %% Main font \setmainfont{ArchivoNarrow}[ Path=assets/fonts/ArchivoNarrow/, @@ -40,7 +39,6 @@ BoldFont=*-Bold, ItalicFont=*-Italic, BoldItalicFont=*-BoldItalic, ] -\newunicodechar{⊥}{\ensuremath{\bot}} %% Mathmatical font \usepackage{amsmath} \usepackage{amssymb} @@ -53,6 +51,9 @@ style=apa, ]{biblatex} \usepackage{cleveref} +% Tables +\usepackage{booktabs} + % Glossary / Acronyms \usepackage[acronym,toc]{glossaries} \usepackage{titlecaps} @@ -64,11 +65,6 @@ style=apa, \usepackage{graphicx} \usepackage{subcaption} -% Example environment -\newcounter{example}[chapter] -\newenvironment{example}[1][]{\refstepcounter{example}\par\medskip \noindent - \textbf{Example~\theexample. #1} \rmfamily}{\hfill \ensuremath{\square}} - % Algorithms % \usepackage[ruled,vlined]{algorithm2e} @@ -96,6 +92,38 @@ style=apa, \newcommand{\pjs}[1]{\textcolor{blue}{\Big[\textbf{Peter}: #1\Big]}} \newcommand{\jip}[1]{\textcolor{red}{\Big[\textbf{Jip}: #1\Big]}} +% Example environment +\usepackage[many]{tcolorbox} +\newcounter{example}[chapter] +\counterwithin{example}{chapter} +\newenvironment{example}[1][]{\refstepcounter{example}\begin{examplebox}#1}{\end{examplebox}} + +\newtcolorbox{examplebox}[1][]{ + breakable, + enhanced, + % skin=enhancedlast, + attach boxed title to top left={xshift=-4mm,yshift=-0.5mm}, + fonttitle=\bfseries\sffamily, + attach boxed title to top center, + boxed title style={empty,arc=0pt,outer arc=0pt,boxrule=0pt}, + underlay boxed title={ + \draw[#1] (title.north west) -- (title.north east) -- +(\tcboxedtitleheight,-\tcboxedtitleheight) + -- (title.south west) -- +(-\tcboxedtitleheight,0)-- cycle; + }, + overlay last={ + \draw[#1] ([xshift=-80pt]frame.south) -- ++ (160pt,0pt); + \fill[#1] ([xshift=-30pt,yshift=-1pt]frame.south) rectangle +(60pt,2pt); + }, + overlay unbroken={ + \draw[#1] ([xshift=-80pt]frame.south) -- ++ (160pt,0pt); + \fill[#1] ([xshift=-30pt,yshift=-1pt]frame.south) rectangle +(60pt,2pt); + }, + title={Example \theexample{}}, + colback=white, + coltitle=black, + colframe=white, +} + % Code formatting \usepackage[ cachedir=listings, @@ -103,15 +131,54 @@ outputdir=build, ]{minted} \usemintedstyle{borland} +\newtcolorbox{listingbox}[1][]{ + breakable, + enhanced, + arc=0pt, + boxrule=0pt, + outer arc=0pt, + overlay first={ + \draw[#1] (frame.north west) -- ++ (0,-5pt); + \draw[#1] (frame.north west) -- ++ (25pt, 0pt); + }, + overlay last={ + \draw[#1] (frame.south west) -- ++ (0, 5pt); + \draw[#1] (frame.south west) -- ++ (25pt,0pt); + }, + overlay unbroken={ + \draw[#1] (frame.north west) -- ++ (0,-5pt); + \draw[#1] (frame.north west) -- ++ (25pt, 0pt); + \draw[#1] (frame.south west) -- ++ (0, 5pt); + \draw[#1] (frame.south west) -- ++ (25pt,0pt); + }, + colback=white, + colframe=white, +} +\BeforeBeginEnvironment{minted}{\begin{listingbox}} +\AfterEndEnvironment{minted}{\end{listingbox}} + \newcommand{\ptinline}[1]{{\texttt{\small {#1}}}} \newcommand{\pyfile}[1]{\inputminted[autogobble=true,breaklines,breakindent=4em,numbers=left,escapeinside=@@,fontsize=\scriptsize]{python}{#1}} -% TODO: Fix the nanozinc sytax highlighting/formatting -\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{markdown}{#1}} - \newcommand{\mznfile}[1]{\inputminted[autogobble=true,breaklines,breakindent=4em,numbers=left,escapeinside=@@,fontsize=\scriptsize]{minizinc}{#1}} \newcommand{\mzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{minizinc}{#1}} +\newenvironment{mzn}{\VerbatimEnvironment{}\begin{minted}[ + autogobble=true, + breaklines, + breakindent=4em, + numbers=none, + escapeinside=@@, + fontsize=\scriptsize, +]{minizinc}}{\end{minted}} -\newenvironment{mzn}{\VerbatimEnvironment\begin{minted}[autogobble=true,breaklines,breakindent=4em,numbers=none,escapeinside=@@,fontsize=\scriptsize]{minizinc}}{\end{minted}} -\newenvironment{nzn}{\VerbatimEnvironment\begin{minted}[autogobble=true,breaklines,breakindent=4em,numbers=none,escapeinside=@@,fontsize=\scriptsize]{markdown}}{\end{minted}} +% TODO: Fix the nanozinc sytax highlighting/formatting +\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{markdown}{#1}} +\newenvironment{nzn}{\VerbatimEnvironment{}\begin{minted}[ + autogobble=true, + breaklines, + breakindent=4em, + numbers=none, + escapeinside=@@, + fontsize=\scriptsize, +]{markdown}}{\end{minted}} diff --git a/assets/shorthands.tex b/assets/shorthands.tex index 5574d76..810591e 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -16,6 +16,8 @@ \newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}} \newcommand{\Cbind}{\ensuremath{\wedge}} +\newcommand{\undefined}{\ensuremath{\bot}} + % Half-reification math things \newcommand{\VV}{{\cal\ V}} diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 8c38e4d..47626c9 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -682,7 +682,7 @@ auxiliary definitions (the \mzninline{@\(\sep\phi\)@} part). t @\(\mapsto\)@ z @\(\sep\)@ [b0] b2 @\(\mapsto\)@ bool_or(b1,c) @\(\sep\)@ [] true @\(\mapsto\)@ true @\(\sep\)@ [b2,c] - \end{mzn} + \end{nzn} Since \mzninline{c} is bound to \mzninline{true}, the disjunction \mzninline{b2} trivially holds, independent of the value of \mzninline{b1}. diff --git a/chapters/5_half_reif.tex b/chapters/5_half_reif.tex index 87297fd..e4eae4c 100644 --- a/chapters/5_half_reif.tex +++ b/chapters/5_half_reif.tex @@ -3,9 +3,9 @@ %************************************************ 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 +\(\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 @@ -56,16 +56,16 @@ intuitive meaning when functions are partial. 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 \texttt{⊥}, and this \texttt{⊥} function percolates up through every -expression to the top level conjunction, making the model unsatisfiable. For the -example +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] = ⊥; -/* t2 @\(\equiv\)@ */ ⊥ * x = ⊥; -/* b2 @\(\equiv\)@ */ ⊥ >= 6 = ⊥; +/* t1 @\(\equiv\)@ */ a[7] = @\undefined{}@; +/* t2 @\(\equiv\)@ */ @\undefined{}@ * x = @\undefined{}@; +/* b2 @\(\equiv\)@ */ @\undefined{}@ >= 6 = @\undefined{}@; /* b1 @\(\equiv\)@ */ 7 <= 4 = false; -false -> ⊥ = ⊥; +false -> @\undefined{}@ = @\undefined{}@; \end{mzn} This is known as the \emph{strict} semantics @@ -73,13 +73,13 @@ This is known as the \emph{strict} semantics 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 \(\bot\) percolates up through the term until it +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] = ⊥; -/* t2 @\(\equiv\)@ */ ⊥ * x = ⊥; -/* b2 @\(\equiv\)@ */ ⊥ >= 6 = false; +/* 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} @@ -142,10 +142,11 @@ versions of their global constraints. \end{example} Reified global constraints are not implemented because a reified constraint -\mzninline{b <-> c} must also implement a propagator for \mzninline{not c} (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. +\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 @@ -182,12 +183,12 @@ of flattening with full reification. \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 \texttt{c} then they can - straightforwardly construct a half reified propagator for \mzninline{b - -> c}. - \item Half reified constraints \mzninline{b -> c} can implement fully reified - constraints without any loss of propagation strength (assuming reified - constraints are negatable). + 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 @@ -412,25 +413,26 @@ extended to arbitrary arguments in a straightforward way. 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}\). +subexpression \(x\) by expression \(y\). We will also use the notation for +multiple simultaneous replacements \(\subs{\bar{x}/\bar{y}}\) where each +\(x_i \in \bar{x}\) is replaced by the corresponding \(y_i \in \bar{y}\). Given a \syntax{} term defining the constraints of the model we can split its \syntax{} subterms as occurring in different kinds of places: root contexts, positive contexts, negative contexts, and mixed contexts. A Boolean subterm \(t\) of constraint \(c\) is in a \emph{root context} iff there is no -solution of \(c\subs{t/\mzninline{false}}\), that is \(c\) with subterm \(t\) replaced by -\(\mzninline{false}\).\footnote{For the definitions of context we assume that the subterm \(t\) - is uniquely defined by its position in \(c\), so the replacement is of exactly - one subterm.} Similarly, a subterm \(t\) of constraint \(c\) is in a -\emph{positive context} iff for any solution \(\theta\) of \(c\) then \(\theta\) is -also a solution of \(c\subs{t/\mzninline{true}}\); and a \emph{negative context} iff for any -solution \(\theta\) of \(c\) then \(\theta\) is also a solution of \(c\subs{t/\mzninline{false}}\). -The remaining Boolean subterms of \(c\) are in \emph{mixed} contexts. While -determining contexts according to these definitions is hard, there are simple -syntactic rules which can determine the correct context for most terms, and the -rest can be treated as mixed. +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 @@ -438,11 +440,10 @@ Consider the constraint expression constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5); \end{mzn} -then \mzninline{x > 0} is in the root context, \(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. - +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 @@ -480,28 +481,29 @@ for each subterm bottom up using approximation. % considered mixed without compromising the correctness of the rest of the % paper. -Our small language contains two partial functions: \texttt{div} returns \(\bot\) -if the divisor is zero, while \(a[i]\) returns \(\bot\) if the value of \(i\) is -outside the domain of \(a\). We can categorize the \emph{safe} terms and -constraints of the language, as those where no \(\bot\) 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 -\(t_1~\texttt{div}~t_2\) and the set of possible values of \(t_2\) does not -include 0, \(0 \not\in poss(t_2)\); or it is an array access term \(a[t]\) and the -set of possible values of \(t\) are included in the domain of \(a\), -\(poss(t) \subseteq \dom(a)\). +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 +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\). +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 @@ -527,8 +529,8 @@ satisfied state of the constraint \(c\). \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 +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 @@ -547,8 +549,8 @@ 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 +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 @@ -617,37 +619,36 @@ contexts are: \rootc, at the top level conjunction; \pos, positive context, % \(\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 \texttt{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 \(b\) made equivalent to \(\mzninline{true}\) by -the constraints in \(S\). For succinctness we use the notation \(\new b\) (\(\new v\)) -to introduce a fresh Boolean (resp.\ integer) variable and return the name of -the variable. - +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. - +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 +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 @@ -656,47 +657,42 @@ 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. - -\newcommand{\callbyvalue}[1]{#1} -\newcommand{\callbyunroll}[1]{} - 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. +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 \verb+/\+ or \verb+\/+ -which is then flattened. A Boolean array lookup flattens its arguments, and -creates an \(\mathit{element}\) constraint. If the context is root this is simple, -otherwise it creates a new index varaible \(v'\) guaranteed to only give correct -answers, and uses this in the \(\mathit{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. \callbyvalue{ User defined predicate applications flatten - their arguments and then flatten a renamed copy of the body.} \callbyunroll{ - User defined predicate applications are replaced by a renamed and flattened - 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 resdtriction, but explain its not all required} The handling -of \texttt{let} is the most complicated. The expression is renamed with new -copies of the let variables. We extract the constraints from the \texttt{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\). +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 \bot\)) \\ +\> \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\) @@ -753,7 +749,6 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n], b'), b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} \) \\ -\callbyvalue{% \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ \> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \\ @@ -772,18 +767,6 @@ b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} \) \> \>\> \(S\) \cupp \(\{ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ -} -\callbyunroll{% -\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ -\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \textbf{abort} \\ -\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, \_}\) := \(\flatt(t_j,\rootc)\); \\ -\>\> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n)\}\) -\\ -\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): user-defined predicate \\ -\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\ -\>\> \> \(b\) := \(\flatc(c_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)\) -\\ -} \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else} \(c_2\) \texttt{endif}: % \\ \> \> \> @@ -824,17 +807,18 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \subsection{Handling \texttt{let} Expressions} -Much of the handling of a \texttt{let} is implemented by +Much of the handling of a \mzninline{let} is implemented by \textsf{flatlet}\((d,c,t,\ctxt)\) which takes the declarations \(d\) inside the -\texttt{let}, the constraint \(c\) or term \(t\) of the scope of the \texttt{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 \texttt{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. +\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} @@ -888,12 +872,12 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \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 +\(\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\). +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 @@ -905,35 +889,30 @@ 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 \(\texttt{element}\) -constraint with a new index variable \(v'\) which is guaranteed to be in the -domain of the array (\(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 tham for simplicity!} \callbyvalue{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}. } \callbyunroll{Partial functions are simply - handled by replacing the function application by the renamed body of the - function. Total functions are more interesting. Each of the arguments is - flattened, the function body is renamed to use the variables representing the - arguments, and then the body is flattened \emph{in the root context}. The - Boolean \(b\) created simply represents whether all the arguments were defined, - since the function itself is total. } 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. +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 \bot\)) \\ +\> \textbf{if} (\(h \neq \undefined{}\)) \\ \>\> \textbf{if} (\(prev =\rootc\)) \textbf{return} \(\tuple{h,b'}\) \\ \>\> \textbf{if} (\(ctxt = \rootc\)) \(S\) \cupp \(\{ b' \}\); hash[\(t\)] := @@ -997,7 +976,6 @@ b' \full v_0 = v', b' \full v_0 \in \{1,\ldots,n\} \} \) \>\> \textbf{case} \texttt{bool2int(} \(c_0\) \texttt{)}: \(b_0\) := \(\flatc(c_0, \mix)\); \(S\) \cupp \(\{ \texttt{bool2int}(b_0, \new v), \new b \}\) \\ -\callbyvalue{% \>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): function \\ \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ \>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\ @@ -1006,19 +984,6 @@ b' \full v_0 = v', b' \full v_0 \in \{1,\ldots,n\} \} \) \>\> \> \(\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 \}\) \\ -} -\callbyunroll{% -\>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): partial function \\ -\>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\ -\>\> \> \(\tuple{v,b}\) := \(\flatt(t_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)\) -\\ -\>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): declared total 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'\) be defn of \(f\) \\ -\>\> \> \(\tuple{v,\_}\) := \(\flatt(t'\subs{x_1/v_1, \ldots, x_n/v_n},\rootc)\) \\ -\> \> \> \(S\) \cupp \(\{ \new b \full \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\); \\ @@ -1043,16 +1008,16 @@ t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ \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)) + 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 in \cref{fig:hr-tree}. + numbered as follows - \begin{figure}[t] - \[ + \[ \xymatrix@R=1em@C=0.6em{ &&&&&~\vee^{(0)} \ar[dll] \ar[drr] \\ &&&~\geq^{(1)} \ar[dl] \ar[dr] &&&&~\wedge^{(2)} \ar[dl] \ar[drr] \\ @@ -1066,13 +1031,11 @@ t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ a &x &~>^{(15)}\ar[dr]\ar[d]& x&z &a &x \\ & & x & y && \\ } - \] - \caption{An expression to be flattened with non-leaf (sub-)terms - numbered.\label{fig:hr-tree}} - \end{figure} - 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. + \] + + 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: @@ -1244,18 +1207,18 @@ t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ 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 +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 -\(\bot\) 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. +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 @@ -1290,11 +1253,16 @@ presentation, we omit the algorithms we use to do this. \section{Half Reification} \label{sec:hr-halfreif} -Given a constraint \(c\), the \emph{half-reified version} of \(c\) is a constraint -of the form \(b \half c\) where \(b \not\in vars(c)\) is a Boolean variable. +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{}@)}. -We can construct a propagator \(f_{b \half c}\) for the half-reified version of -\(c\), \(b \half c\), using the propagator \(f_c\) for \(c\). \[ \begin{array}{rcll} f_{b \half c}(D)(b) & = & \{ \mzninline{false} \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\ @@ -1337,22 +1305,24 @@ f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c) % 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{c} first check -whether \mzninline{c} 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 -> c}}\) by only performing the -checking part until \(D(\texttt{b}) = \{\mzninline{true}\}\). +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 \texttt{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. +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 @@ -1362,9 +1332,9 @@ half-reified using the variable of the nearest enclosing Boolean term. i > 4 \/ a[i] * x >= 6 \end{mzn} - There are three Boolean terms: the entire constraint, \(i > 4\) and - \(a[i] \times x \geq 6\), which we name \(b_0\), \(b_1\) and \(b_2\) respectively. The - flattened form using half reification is + 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; @@ -1374,11 +1344,12 @@ half-reified using the variable of the nearest enclosing Boolean term. 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 \(i = 7\) then the second constraint makes - \(b2 = \mzninline{false}\). Given this, the final constraint requires \(b1 = \mzninline{true}\), which - in turn requires \(i > 4\). Since this holds, the whole constraint is \(\mzninline{true}\) - with no restrictions on \(x\). + 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 @@ -1408,13 +1379,15 @@ not propagate unnecessarily. \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]; + 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 \(s[j]\) of task \(j\), the sum of resources - \(r\) used by it and by other tasks executing at the same time is less than the - limit \(L\). Flattening with full reification produces constraints like this: + 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]; @@ -1425,11 +1398,11 @@ not propagate unnecessarily. constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j]; \end{mzn} - Whenever the start time of task \(i\) is constrained so that it does not overlap - time \(s[j]\), then \(b3[i]\) is fixed to \(\mzninline{false}\) and \(a[i]\) to 0, and the long - linear sum is awoken. But this is useless, since it cannot cause failure. + 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. - % Half-reification of this expression which appears in a negative context produces The Boolean expression appears in a negative context, and half-reification produces @@ -1444,21 +1417,21 @@ not propagate unnecessarily. \end{mzn} which may seem to be more expensive since there are additional variables (the - \(b4[i]\)), but since both \(b4[i]\) and \(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 \(i\) is - guaranteed to overlap time \(s[j]\). + \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?} +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} @@ -1471,20 +1444,21 @@ 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,c)\) defined below returns a set of constraints -implementing the half-reification \(b \half c\). We flatten a constraint item -\(\texttt{constraint}~c\) using \(\halfc(\mzninline{true}, c)\). The half-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 \(c_1\) 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 +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 \(t_1 < t_2\) -yields \(t_1 \geq t_2\), and negating \(c_1\) \verb+/\+ \(c_2\) yields -\(\texttt{not}~c_1\) \verb+\/+ \texttt{not}~\(c_2\). Any negations on -subexpressions will be processed by recursive invocations of the algorithm. +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}} @@ -1493,7 +1467,7 @@ subexpressions will be processed by recursive invocations of the algorithm. \newcommand{\iboth}{\textsf{both}} \newcommand{\negaterel}{\textsf{negaterel}} -Halfreifying a constraint \(c\) in context \(\ctxt\), \(\halfc(c,\ctxt)\), returns a +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 @@ -1531,9 +1505,9 @@ and \(\texttt{not}~c_1 \vee c_2\) and full reification for \(c_1~\verb+<->+~c_2\ 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 -\texttt{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 +\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 @@ -1543,7 +1517,7 @@ full reification. xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \halfc(\(c\),\(\ctxt\)) \\ \> \(\tuple{h,prev}\) := hhash[\(c\)]; \\ -\> \textbf{if} (\(h \neq \bot\)) \\ +\> \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\)] := @@ -1607,7 +1581,6 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill %\>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n], b'), %b'' \full v = v', b'' \full v \in \{1,..,n\} \} \) %\\ -\callbyvalue{% \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\ @@ -1632,18 +1605,6 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ -} -\callbyunroll{% -\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ -\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \textbf{abort} \\ -\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, \_}\) := \(\flatt(t_j,\rootc)\); \\ -\>\> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n)\}\) -\\ -\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): user-defined predicate \\ -\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\ -\>\> \> \(b\) := \(\flatc(c_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)\) -\\ -} \> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else} \(c_2\) \texttt{endif}: % \\ \> \> \> @@ -1665,10 +1626,11 @@ c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)\) \\ 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\). +\(\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 @@ -1676,13 +1638,13 @@ 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 riefies \(c\), the negations +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 refication. User +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 @@ -1692,7 +1654,7 @@ context passed to \(\textsf{flatlet}\) is either \(\negc\) or \(\mix\). xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \halfnc(\(c\),\(\ctxt\)) \\ \> \(\tuple{h,prev}\) := hhash[\(\texttt{not}~c\)];\\ -\> \textbf{if} (\(h \neq \bot\)) \\ +\> \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\)] := @@ -1741,7 +1703,6 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \>\>\> \(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)\) \\ -\callbyvalue{% \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ \> \> \> \(b\) := \(\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)\) \\ \>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): user-defined predicate \\ @@ -1753,7 +1714,6 @@ xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill \> \>\> \(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}: % \\ \> \> \> @@ -1775,44 +1735,44 @@ c_1\subs{\bar{v}/\bar{v}'},0,\negop \ctxt)\) \\ \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. +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 -\texttt{solve maximize}~\(e\) using \(\halft(e, \rootc, \ibelow)\) since we are +\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 \texttt{solve minimize}~\(e\) is flattened using +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\). - +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: +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} @@ -1839,23 +1799,23 @@ 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 -\texttt{element} constraint. Array sums and if-then-else-endif are +\mzninline{element} constraint. Array sums and if-then-else-endif are straightforward. -The treatment of \texttt{bool2int} is the reason for the complex bounds -analysis. If we are only interested in the lower bound of \(\texttt{bool2int}(c)\) -we can half reify \(c\) since it is in a positive context. If we are only -interested in the upper bound of \(\texttt{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\). +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 \bot\)) \\ +\> \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\) \\ @@ -1936,7 +1896,6 @@ b' \half \texttt{element}(v_0, [v_1, \ldots, v_n], \new v), \} \) \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 \}\) \\ -\callbyvalue{ \>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): function \\ \> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\ \>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\ @@ -1945,7 +1904,6 @@ b' \half \texttt{element}(v_0, [v_1, \ldots, v_n], \new v), \} \) \>\> \> \(\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\) \\ @@ -2039,58 +1997,61 @@ t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\ \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\). - - +\(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 modeling \(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. +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} + \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} + \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. +\(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. +\(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)\),