diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 3b7a600..7e92265 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -1,3 +1,12 @@ +@book{allen-1978-lisp, + author = {Allen, John}, + title = {Anatomy of LISP}, + year = 1978, + isbn = {007001115X}, + publisher = {McGraw-Hill, Inc.}, + address = {USA}, +} + @inproceedings{araya-2008-cse-numcsp, author = {Ignacio Araya and Bertrand Neveu and Gilles Trombettoni}, editor = {Peter J. Stuckey}, @@ -34,6 +43,21 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{balas-1989-pctsp, + author = {Egon Balas}, + title = {The prize collecting traveling salesman problem}, + journal = {Networks}, + volume = 19, + number = 6, + pages = {621--636}, + year = 1989, + url = {https://doi.org/10.1002/net.3230190602}, + doi = {10.1002/net.3230190602}, + timestamp = {Sun, 28 May 2017 13:19:52 +0200}, + biburl = {https://dblp.org/rec/journals/networks/Balas89.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{belin-2014-interactive, author = {Bruno Belin and Marc Christie and Charlotte Truchet}, editor = {Helmut Simonis}, @@ -90,6 +114,24 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@inproceedings{brand-2006-propagation, + author = {Sebastian Brand and Roland H. C. Yap}, + editor = {Sandro Etalle and Miroslaw Truszczynski}, + title = {Towards "Propagation = Logic + Control"}, + booktitle = {Logic Programming, 22nd International Conference, {ICLP} + 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 4079, + pages = {102--116}, + publisher = {Springer}, + year = 2006, + url = {https://doi.org/10.1007/11799573_10}, + doi = {10.1007/11799573_10}, + timestamp = {Tue, 14 May 2019 10:00:48 +0200}, + biburl = {https://dblp.org/rec/conf/iclp/BrandY06.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @article{chiarandini-2012-gbac, author = {Marco Chiarandini and Luca Di Gaspero and Stefano Gualandi and Andrea Schaerf}, @@ -196,6 +238,43 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@inproceedings{frisch-2007-essence, + author = {Alan M. Frisch and Matthew Grum and Christopher Jefferson + and Bernadette Mart{\'{\i}}nez Hern{\'{a}}ndez and Ian Miguel}, + editor = {Manuela M. Veloso}, + title = {The Design of {ESSENCE:} {A} Constraint Language for + Specifying Combinatorial Problems}, + booktitle = {{IJCAI} 2007, Proceedings of the 20th International Joint + Conference on Artificial Intelligence, Hyderabad, India, + January 6-12, 2007}, + pages = {80--87}, + year = 2007, + url = {http://ijcai.org/Proceedings/07/Papers/011.pdf}, + timestamp = {Tue, 20 Aug 2019 16:17:11 +0200}, + biburl = {https://dblp.org/rec/conf/ijcai/FrischGJHM07.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{frisch-2009-undefinedness, + author = {Alan M. Frisch and Peter J. Stuckey}, + editor = {Ian P. Gent}, + title = {The Proper Treatment of Undefinedness in Constraint + Languages}, + booktitle = {Principles and Practice of Constraint Programming - {CP} + 2009, 15th International Conference, {CP} 2009, Lisbon, + Portugal, September 20-24, 2009, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 5732, + pages = {367--382}, + publisher = {Springer}, + year = 2009, + url = {https://doi.org/10.1007/978-3-642-04244-7_30}, + doi = {10.1007/978-3-642-04244-7_30}, + timestamp = {Tue, 14 May 2019 10:00:45 +0200}, + biburl = {https://dblp.org/rec/conf/cp/FrischS09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @misc{gecode-2021-gecode, author = {{Gecode Team}}, title = {Gecode: A Generic Constraint Development Environment}, @@ -203,6 +282,13 @@ url = {http://www.gecode.org} } +@misc{gurobi-2021-gurobi, + author = "Gurobi Optimization, LLC", + title = "Gurobi Optimizer Reference Manual", + year = 2021, + url = "http://www.gurobi.com" +} + @inproceedings{hebrard-2005-diverse, author = {Emmanuel Hebrard and Brahim Hnich and Barry O'Sullivan and Toby Walsh}, @@ -251,6 +337,22 @@ publisher = {Springer US} } +@article{jefferson-2010-connectives, + author = {Christopher Jefferson and Neil C. A. Moore and Peter + Nightingale and Karen E. Petrie}, + title = {Implementing logical connectives in constraint programming}, + journal = {Artif. Intell.}, + volume = 174, + number = {16-17}, + pages = {1407--1429}, + year = 2010, + url = {https://doi.org/10.1016/j.artint.2010.07.001}, + doi = {10.1016/j.artint.2010.07.001}, + timestamp = {Sat, 16 Sep 2017 12:06:14 +0200}, + biburl = {https://dblp.org/rec/journals/ai/JeffersonMNP10.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @article{jones-2002-multi-objective, author = {Dylan F. Jones and S. Keyvan Mirrazavi and Mehrdad Tamiz}, title = {Multi-objective meta-heuristics: An overview of the current @@ -283,6 +385,23 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{lougee-heimer-2003-coin, + author = {Robin Lougee{-}Heimer}, + title = {The Common Optimization INterface for Operations Research: + Promoting open-source software in the operations research + community}, + journal = {{IBM} J. Res. Dev.}, + volume = 47, + number = 1, + pages = {57--66}, + year = 2003, + url = {https://doi.org/10.1147/rd.471.0057}, + doi = {10.1147/rd.471.0057}, + timestamp = {Fri, 13 Mar 2020 10:54:17 +0100}, + biburl = {https://dblp.org/rec/journals/ibmrd/Lougee-Heimer03.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{marinov-2005-sat-optimisations, author = {Darko Marinov and Sarfraz Khurshid and Suhabe Bugrara and Lintao Zhang and Martin C. Rinard}, @@ -317,6 +436,24 @@ programming}, } +@article{marriott-2008-zinc, + author = {Kim Marriott and Nicholas Nethercote and Reza Rafeh and + Peter J. Stuckey and Maria Garcia de la Banda and Mark + Wallace}, + title = {The Design of the Zinc Modelling Language}, + journal = {Constraints An Int. J.}, + volume = 13, + number = 3, + pages = {229--267}, + year = 2008, + url = {https://doi.org/10.1007/s10601-008-9041-4}, + doi = {10.1007/s10601-008-9041-4}, + timestamp = {Fri, 13 Mar 2020 10:58:29 +0100}, + biburl = + {https://dblp.org/rec/journals/constraints/MarriottNRSBW08.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{mears-2014-option, author = {Christopher Mears and Andreas Schutt and Peter J. Stuckey and Guido Tack and Kim Marriott and Mark Wallace}, @@ -480,6 +617,44 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@inproceedings{schulte-2000-deep, + author = {Christian Schulte}, + editor = {Enrico Pontelli and V{\'{\i}}tor Santos Costa}, + title = {Programming Deep Concurrent Constraint Combinators}, + booktitle = {Practical Aspects of Declarative Languages, Second + International Workshop, {PADL} 2000, Boston, MA, USA, January + 2000, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 1753, + pages = {215--229}, + publisher = {Springer}, + year = 2000, + url = {https://doi.org/10.1007/3-540-46584-7_15}, + doi = {10.1007/3-540-46584-7_15}, + timestamp = {Tue, 14 May 2019 10:00:42 +0200}, + biburl = {https://dblp.org/rec/conf/padl/Schulte00.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{schulte-2005-views, + author = {Christian Schulte and Guido Tack}, + editor = {Peter van Beek}, + title = {Views and Iterators for Generic Constraint Implementations}, + booktitle = {Principles and Practice of Constraint Programming - {CP} + 2005, 11th International Conference, {CP} 2005, Sitges, Spain, + October 1-5, 2005, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 3709, + pages = {817--821}, + publisher = {Springer}, + year = 2005, + url = {https://doi.org/10.1007/11564751_71}, + doi = {10.1007/11564751_71}, + timestamp = {Tue, 14 May 2019 10:00:45 +0200}, + biburl = {https://dblp.org/rec/conf/cp/SchulteT05.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @article{schulte-2008-propagation, author = {Christian Schulte and Peter J. Stuckey}, title = {Efficient constraint propagation engines}, @@ -495,6 +670,26 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@inproceedings{schutt-2009-cumulative, + author = {Andreas Schutt and Thibaut Feydy and Peter J. Stuckey and + Mark Wallace}, + editor = {Ian P. Gent}, + title = {Why Cumulative Decomposition Is Not as Bad as It Sounds}, + booktitle = {Principles and Practice of Constraint Programming - {CP} + 2009, 15th International Conference, {CP} 2009, Lisbon, + Portugal, September 20-24, 2009, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 5732, + pages = {746--761}, + publisher = {Springer}, + year = 2009, + url = {https://doi.org/10.1007/978-3-642-04244-7_58}, + doi = {10.1007/978-3-642-04244-7_58}, + timestamp = {Tue, 14 May 2019 10:00:45 +0200}, + biburl = {https://dblp.org/rec/conf/cp/SchuttFSW09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{shaw-1998-local-search, author = {Paul Shaw}, editor = {Michael J. Maher and Jean{-}Francois Puget}, @@ -515,6 +710,17 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@phdthesis{rendl-2010-thesis, + author = {Andrea Rendl}, + title = {Effective compilation of constraint models}, + school = {University of St Andrews, {UK}}, + year = {2010}, + url = {http://hdl.handle.net/10023/973}, + timestamp = {Thu, 25 Aug 2016 17:20:59 +0200}, + biburl = {https://dblp.org/rec/phd/ethos/Rendl10.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @book{silvano-1990-knapsack, author = {Martello, Silvano and Toth, Paolo}, title = {Knapsack Problems: Algorithms and Computer Implementations}, @@ -575,6 +781,17 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@book{van-hentenryck-1999-opl, + title = {The OPL Optimization Programming Language}, + author = {Van Hentenryck, P. and Lustig, I. and Puget, J.F. and + Michel, L.}, + isbn = 9780262720304, + lccn = 98034698, + series = {Computing in Musicology; 11}, + year = 1999, + publisher = {MIT Press} +} + @book{wallis-2011-combinatorics, title = {Introduction to Combinatorics}, author = {Wallis, W.D. and George, J.}, @@ -601,3 +818,14 @@ year = 1988, publisher = {Wiley} } + +@techreport{gamrath-2020-scip, + author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros Gleixner and Leona Gottwald and Katrin Halbig and Gregor Hendel and Christopher Hojny and Thorsten Koch and Le Bodic, Pierre and Stephen J. Maher and Frederic Matter and Matthias Miltenberger and Erik M{\"u}hmer and Benjamin M{\"u}ller and Marc E. Pfetsch and Franziska Schl{\"o}sser and Felipe Serrano and Yuji Shinano and Christine Tawfik and Stefan Vigerske and Fabian Wegscheider and Dieter Weninger and Jakob Witzig}, + title = {{The SCIP Optimization Suite 7.0}}, + type = {ZIB-Report}, + institution = {Zuse Institute Berlin}, + number = {20-10}, + month = {March}, + year = {2020}, + url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023} +} diff --git a/assets/packages.tex b/assets/packages.tex index 70f9714..2a0e77e 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -67,7 +67,7 @@ style=apa, % Code formatting \usepackage[ -cachedir=build/listings, +cachedir=listings, outputdir=build, ]{minted} \usemintedstyle{borland} @@ -97,3 +97,62 @@ outputdir=build, % Proof Tree \usepackage[nounderscore]{syntax} \usepackage{bussproofs} + +% Half-reification math things + +% \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{\rep}{\mathit{rep}} +% \DeclareMathOperator{\cl}{\mathit{cl}} +% \DeclareMathOperator{\UP}{\mathit{UP}} +% \DeclareMathOperator{\up}{\mathit{up}} +% \DeclareMathOperator{\DOM}{\mathit{DOM}} +% \DeclareMathOperator{\false}{\mathit{false}} +% \DeclareMathOperator{\true}{\mathit{true}} +% \DeclareMathOperator{\lit}{\mathit{lit}} +% \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{\supp}{supp} +% \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}} + +% \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{\cross}{\times} +% \renewcommand{\cross}{\baucross} +% \renewcommand{\cross}{\ding{54}} +% \newcommand{\entails}{\models} +% \newcommand{\bigsqcap}{\mathop{\lower.1ex\hbox{\Large$\sqcap$}}} + +% \newcommand{\mdiv}{\texttt{div}} +% \newcommand{\element}{\texttt{element}} +% \newcommand{\alldiff}{\texttt{all\_different}} diff --git a/chapters/5_half_reif.tex b/chapters/5_half_reif.tex index a473bd4..40e6ffb 100644 --- a/chapters/5_half_reif.tex +++ b/chapters/5_half_reif.tex @@ -1,3 +1,2669 @@ %************************************************ \chapter{Mode Analysis and Half Reification}\label{ch:half_reif} %************************************************ + +Discrete optimisation solvers solve constraint optimisation problems of the form +$\min o \text{~subject to~} \wedge_{c \in C} c$, that is minimising an objective +$o$ subject to an (existentially quantified) conjunction of primitive +constraints $c$. But modelling languages such as OPL +\autocite{van-hentenryck-1999-opl}, Zinc/\minizinc\ +\autocite{marriott-2008-zinc, nethercote-2007-minizinc} and Essence +\cite{frisch-2007-essence} allow much more expressive problems to be formulated. +Modelling languages map the more expressive formulations to existentially +quantified conjunction through a combination of loop unrolling, and flattening +using reification. + +\begin{example}\label{ex:cons} + Consider the following ``complex constraint'' written in \minizinc\ syntax + + \begin{mzn} + constraint i <= 4 -> a[i] * x >= 6; + \end{mzn} + + which requires that if $i \leq 4$ then the value in the $i^{th}$ position of + array $a$ multiplied by $x$ must be at least 6. This becomes the following + existentially quantified conjunction through flattening and + reification:\footnote{Actually the result is in \flatzinc\ but we show an + equivalent \minizinc\ form for easy of readability.} + + \begin{mzn} + constraint b1 <-> i <= 4; % b1 holds iff i <= 4 + constraint element(i,a,t1); % t1 is the ith element of a + constraint mult(t1,x,t2); % t2 is t1 * x + constraint b2 <-> t2 >= 6; % b2 holds iff t2 >= 6 + constraint b1 -> b2 % b1 implies b2 + \end{mzn} + + The complex logic (implication) is encoded by ``reifying'' the arguments and + in effect naming their truth value using new Boolean variables $b1$ and $b2$. + The term structure is encoded by ``flattening'' the terms and converting the + functions to relations, introducing the new integer variables $t1$ and $t2$. + Note that the newly introduced variables are existentially quantified. +\end{example} + +The translation given in the above example is well understood, but potentially +flawed, for three reasons. The first is that the flattening may not give the +intuitive meaning when functions are partial. + +\begin{example} + Suppose the array $a$ has index set 1..5, but $i$ takes the value 7. The + constraint $\element(i,a,t1)$ will fail and no solution will be found. + Intuitively if $i = 7$ the constraint should be trivially true. +\end{example} + +The simple flattening used above treats partial functions in the following +manner. Application of a partial function to a value for which it is not defined +gives value $\bot$, and this $\bot$ function percolates up through every +expression to the top level conjunction, making the model unsatisfiable. For the +example $(t1\equiv)~ a[7] = \bot$, $(t2\equiv)~ \bot \times x = \bot$, +$(b2\equiv)~ \bot \geq 6 = \bot$, $(b1\equiv)~ 7 \leq 4 = \false$, +$\false \rightarrow \bot = \bot$. This is known as the \emph{strict} semantics +\autocite{frisch-2009-undefinedness} for modeling languages. + +The usual choice for modeling partial functions in modelling languages is the +\emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the +relational semantics the value $\bot$ percolates up through the term until it +reaches a Boolean subterm where it becomes $\false$. For the example +$(t1\equiv)~ a[7] = \bot$, $(t2\equiv)~ \bot \times x = \bot$, +$(b2\equiv)~ \bot \geq 6 = \false$, $(b1\equiv)~ 7 \leq 4 = \false$, +$\false \rightarrow \false = \true$. But in order to implement the relational +semantics, the translation of the original complex constraint needs to be far +more complex. + +\begin{example} + The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models + implementing the relational semantics. Assuming $i$ takes values in the set + 1..8, and $a$ has an index set 1..5, its translation of the constraint in + Example~\ref{ex:cons} is + + \begin{mzn} + constraint b1 <-> i <= 4; % b1 holds iff i <= 4 + constraint element(t3,a,t1);% t1 is the t3'th element of a + constraint mult(t1,x,t2); % t2 is t1 * x + constraint b2 <-> t2 >= 6; % b2 holds iff t2 >= 6 + constraint t3 in 1..5 % t3 in index set of a + constraint b3 <-> i = t3; % b3 holds iff i = t3 + constraint b3 <-> i <= 5; % b3 holds iff i in index set of a + constraint b4 <-> b2 /\ b3 % b4 holds iff b2 and b3 hold + constraint b1 -> b4 % b1 implies b4 + \end{mzn} + + The translation forces the partial function application $\element$ to be + ``safe'' since $t3$ is constrained to only take values in the index set of $a$. + The reified constraints defining $b3$ force $t3$ to equal $i$ iff $i$ takes a + value in the index set of $a$. + % Finally the Boolean + % $b4$ defines when the rhs condition holds $b2$ + % and the \element{} constraint was safe $b3$. +\end{example} + + +A second weakness of reification, independent of the problems with partial +functions, is that each reified version of a constraint requires further +implementation to create, and indeed most solvers do not provide any reified +versions of their global constraints. + +\begin{example}\label{ex:alldiff} + Consider the complex constraint + + \begin{mzn} + constraint i <= 4 -> all_different([i,x-i,x]); + \end{mzn} + + The usual flattened form would be + + \begin{mzn} + constraint b1 <-> i <= 4; % b1 holds iff i <= 4 + constraint minus(x,i,t1); % t1 = x - i + constraint b2 <-> all_different([i,t1,x]); + constraint b1 -> b2 % b1 implies b2 + \end{mzn} + + but no solver we are aware of implements the third primitive constraint. + \footnote{Although there are versions of soft \alldiff, they do not define + this form.} +\end{example} + +Reified global constraints are not implemented because a reified constraint +$b \full c$ must also implement a propagator for $\neg c$ (in the case that +$b = \false$). While for some global constraints, e.g. \alldiff{}, this may be +reasonable to implement, for most, such as \texttt{cumulative}, the task seems +to be very difficult. + +A third weakness of the full reification is that it may keep track of more +information than is required. In a typical finite domain solver, the first +reified constraint $b_1 \full i \leq 4$ will wake up whenever the upper bound of +$i$ changes in order to check whether it should set $b_1$ to $true$. But setting +$b_1$ to $true$ will \emph{never} cause any further propagation. There is no +reason to check this. + +This is particularly important when the target solver is a mixed integer +programming solver. In order to linearize a reified linear constraint we need to +create two linear constraints, but if we are only interested in half of the +behaviour we can manage this with one linear constraint. + +\begin{example} + Consider the constraint $b1 \full i \leq 4$, where $i$ can take values in the domain $0..10$ + then its linearization is + \begin{mzn} + constraint i <= 10 - 6*b1; % b1 -> i <= 4 + constraint i >= 5 - 5*b1; % not b1 -> i >= 5 + \end{mzn} + But in the system of constraints where this constraint occurs knowing that $b1$ is 0 + will never cause the system to fail, hence we do not need to keep track of it. + We can simply use the second constraint in the linearization, which always allows that + $b1$ takes the value 0. +\end{example} + +Flattening with half-reification is an approach to mapping complex constraints +to existentially quantified conjunctions that improves upon all these weaknesses +of flattening with full reification. + +\begin{itemize} + \item Flattening with half reification can naturally produce the relational + semantics when flattening partial functions in positive contexts. + \item Half reified constraints add no burden to the solver writer; if they + have a propagator for constraint $c$ then they can straightforwardly + construct a half reified propagator for $b \half c$. + \item Half reified constraints $b \half c$ can implement fully reified + constraints without any loss of propagation strength (assuming reified + constraints are negatable). + \item Flattening with half reification can produce more efficient propagation + when flattening complex constraints. + \item Flattening with half reification can produce smaller linear models when + used with a mixed integer programming solver. +\end{itemize} + +Our conclusion is that propagation solvers \emph{only} need to provide half +reified version of all constraints. This does not burden the solver writer at +all, yet it provides more efficient translation of models, and more +expressiveness in using global constraints. + +\jip{Add a variation of this: Adding support for half reification to the linear + library is more interesting and seems very worthwhile. Since the solvers using + the linear library only support linear constraints, full reification is + generally implemented using using the equivalence of two implications; for + example, the full reification \(b \full x \le y \) is implemented by the + linearisation of \((b \half x \le y) \land (\lnot b \half x > y)\). The half + reification of the same constraint consist only of the first half of the + conjunction.} + +\section{Propagation Based Constraint Solving} + +We consider a typed set of variables $\VV = \VV_I \cup \VV_B$ made up of +\emph{integer} variables, $\VV_I$, and \emph{Boolean} variables, $\VV_b$. We use +lower case letters such as $x$ and $y$ for integer variables and letters such as +$b$ for Booleans. +% +A \emph{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers +(for the variables in $\VV_I$) and to subsets of $\{\true,\false\}$ (for the +variables in $\VV_b$). +% +We can understand a domain $D$ as a formula $\wedge_{v \in \VV} (v \in D(v))$ +stating for each variable $v$ that its value is in its domain. A \emph{false + domain} $D$ is a domain where $\exists v \in \VV. D(v) = \emptyset$, and +corresponds to an unsatisfiable formula. + +Let $D_1$ and $D_2$ be domains and $V\subseteq\VV$. We say that $D_1$ is +\emph{stronger} than $D_2$, written $D_1 \sqsubseteq D_2$, if +$D_1(v) \subseteq D_2(v)$ for all $v \in \VV$. +%% and that $D_1$ and $D_2$ +%% are \emph{equivalent modulo $V$}, written $D_1 =_V D_2$, if $D_1(v) = +%% D_2(v)$ for all $v \in V$. \pjs{Equivelant modulo never used???} +%% +The \emph{intersection} of $D_1$ and $D_2$, denoted $D_1 \sqcap D_2$, is defined +by the domain $D_1(v) \cap D_2(v)$ for all $v\in\VV$. +% +%We use \emph{range} notation: +% +%For integers $l$ and $u$, $\range{l}{u}$ denotes the set of integers +%$\{ d ~|~ l \leq d \leq u\}$. +% +We assume an \emph{initial domain} $D_{init}$ such that all domains $D$ that +occur will be stronger i.e.~$D \sqsubseteq D_{init}$. + + +A \emph{valuation} $\theta$ is a mapping of integer and Boolean variables to +correspondingly typed values, written +$\{x_1 \mapsto d_1, \ldots, x_n \mapsto d_n, b_1 \mapsto u_1, \ldots, b_m \mapsto u_m\}$. +% PJS (not true unless \theta is in D) +% where $d_i \in D(x_i)$ and $A_j \in D(S_j)$. +We extend the valuation $\theta$ to map expressions or constraints involving the +variables in the natural way. Let $\vars$ be the function that returns the set +of variables appearing in an expression, constraint or valuation. + +In an abuse of notation, we define a valuation $\theta$ to be an element of a +domain $D$, written $\theta \in D$, if $\theta(v) \in D(v)$ for all +$v \in \vars(\theta)$. + + +%\paragraph{Constraints, Propagators and Propagation Solvers} + +A constraint is a restriction placed on the allowable values for a set of +variables. +%% We shall be interested in constraints +%PJS over integer, set and Boolean variables. +%% over integer and set variables. +We define the \emph{solutions} of a constraint $c$ to be the set of valuations +$\theta$ that make that constraint true, i.e. +$\solns(c) = \{ \theta \ |\ (\vars(\theta) = \vars(c))\ \wedge\ (\entails \theta(c))\}$ + +%%MC check this para that my changes are ok +We associate with every constraint $c$ a \emph{propagator} $f_c$. A propagator +$f_c$ is a monotonically decreasing function on domains that maintains solutions +of the constraint. That is, for all domains $D \sqsubseteq D_{init}$: + +$f_c(D) \sqsubseteq D$ (decreasing), and +$\{\theta\in D \,|\ \theta \in \solns(c)\} = \{\theta \in f_c(D)\,|\ \theta \in \solns(c)\}$ +(preserves solutions), and for domains +$D_1 \sqsubseteq D_2 \sqsubseteq D_{init}$: $f(D_1) \sqsubseteq f(D_2)$ +(monotonic). This is a weak restriction since, for example, the identity mapping +is a propagator for any constraint. + +A domain $D$ is \emph{domain consistent} for constraint $c$ if +$D(v) = \{ \theta(v) ~|~ \theta \in solns(c) ~\wedge~ \theta \in D \}$, for all +$v \in vars(c)$. + +A domain $D$ is \emph{bounds(Z) consistent} for constraint $c$ over variables +$v_1, \ldots v_n$ if for each $i \in \{1, \ldots, n\}$ there exists +$\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \min D(v_i)$ and +$\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$, and +similarly exists $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \max D(v_i)$ +and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$. For +Boolean variables $v$ we assume $\false < \true$. + +% A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ if the same +% conditions as for bounds(Z) consistency hold except $\theta \in solns(c')$ where +% $c'$ is the \emph{real relaxation} of $c$. + +A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ over integer +variables $x_1, \ldots x_n$ and Boolean variables $b_1, \ldots, b_m$ if $c'$ is +the real relaxation of $c$ (where $x_1, \ldots, x_n$ can take real values, +rather than just integer values) and for each $i \in \{1, \ldots, n\}$ there +exists $\theta \in solns(c') \cap D$ s.t. $\theta(x_i) = \min D(x_i)$ and +$\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n$ and +$\theta(b_j) \in D(b_j), 1 \leq j \leq m$, and similarly exists +$\theta \in solns(c') \cap D$ s.t. $\theta(x_i) = \max D(x_i)$ and +$\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n$ and +$\theta(b_j) \in D(b_j), 1 \leq j \leq m$. Also for each $i in \{1,\ldots, m\}$ +and $tf \in D(b_i)$ there exists $\theta \in solns(c') \cap D$ s.t. +$\theta(b_i) = tf$ and +$\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \leq n$ and +$\theta(b_j) \in D(b_j), 1 \leq j \neq i \leq m$. + +Note that we assume Booleans can only take Boolean values in the real +relaxation. + +Note that for the pure Boolean constraints domain, bounds(Z) and bounds(R) +consistency coincide. + +A propagator $f_c$ is $X$-consistent if $f(D)$ is always $X$ consistent for $c$, +where $X$ could be domain, bounds(Z) or bounds(R). + +A \emph{propagation solver} for a set of propagators $F$ and current domain $D$, +$\solv(F,D)$, repeatedly applies all the propagators in $F$ starting from domain +$D$ until there is no further change in the resulting domain. $\solv(F,D)$ is +the weakest domain $D' \sqsubseteq D$ which is a fixpoint (i.e.~$f(D') = D'$) +for all $f \in F$. In other words, $\solv(F,D)$ returns a new domain defined by +$ \solv(F,D) = \gfp(\lambda d.\iter(F,d))(D)$ where +$\iter(F,D) = \bigsqcap_{f \in F} f(D)$, where $\gfp$ denotes the greatest +fixpoint w.r.t $\sqsubseteq$ lifted to functions. +% (We use the greatest fixpoint because we are coming down from a full domain, +% not going up from an empty one.) + + +\subsection{A Language of Constraints} + +\newcommand{\nonterm}[1]{\textsc{#1}} + +\newcommand{\cons}{\nonterm{cons}} +\newcommand{\intc}{\nonterm{int}} +\newcommand{\bvar}{\nonterm{bvar}} +\newcommand{\ivar}{\nonterm{ivar}} +\newcommand{\term}{\nonterm{term}} +\newcommand{\cname}{\nonterm{pred}} +\newcommand{\relop}{\nonterm{relop}} +\newcommand{\aop}{\nonterm{arithop}} +\newcommand{\arrayc}{\nonterm{array}} +\newcommand{\arrow}{$\longrightarrow$} +\newcommand{\vb}{$|$} + +\label{sec:syntax} + +%\newcommand{\cons}{\textsf{cons}} +%\newcommand{\intc}{\textsf{int}} +%\newcommand{\bvar}{\textsf{bvar}} +%\newcommand{\ivar}{\textsf{ivar}} +\newcommand{\aivar}{\nonterm{aivar}} +\newcommand{\abvar}{\nonterm{abvar}} +\newcommand{\avar}{\nonterm{avar}} +%\newcommand{\term}{\textsf{term}} +%\newcommand{\cname}{\textsf{pred}} +\newcommand{\fname}{\nonterm{func}} +%\newcommand{\relop}{\textsf{relop}} +%\newcommand{\aop}{\textsf{arithop}} +\newcommand{\arrayi}{\nonterm{iarray}} +\newcommand{\arrayb}{\nonterm{barray}} +\newcommand{\decli}{\nonterm{idecl}} +\newcommand{\declb}{\nonterm{bdecl}} +\newcommand{\decls}{\nonterm{decls}} +\newcommand{\argo}{\nonterm{arg}} +\newcommand{\args}{\nonterm{args}} +\newcommand{\itm}{\nonterm{item}} +\newcommand{\itms}{\nonterm{items}} +\newcommand{\model}{\nonterm{model}} +\newcommand{\solve}{\nonterm{solve}} +\newcommand{\optcons}{\nonterm{ocons}} +%\newcommand{\arrow}{$\rightarrow$} +%\newcommand{\vb}{$|$} +\newcommand{\subs}[1]{[\![ #1 ]\!] } +\newcommand{\flatc}{\nonterm{flatc}} +\newcommand{\flatt}{\nonterm{flatt}} +\newcommand{\new}{\textbf{new}~} +\newcommand{\evalb}{\nonterm{evala}} +\newcommand{\evali}{\nonterm{evali}} + + +Below is a grammar for a subset of \minizinc\, with enough complexity to +illustrate all the main challenges in flattening. + +The \cons{} nonterminal defines constraints (Boolean terms), \term{} defines +integer terms, \arrayb{} defines Boolean arrays, and \arrayi{} defines integer +arrays: + +\vspace{2mm} +\noindent +\begin{tabular}{rcl} +\cons{} & \arrow & \texttt{true} \vb{} \texttt{false} \vb{} \bvar{} \vb{} \term{} \relop{} \term{} \\ + & \arrow & \texttt{not} \cons{} \vb{} \cons{} \verb+/\+ \cons{} \vb{} + \cons{} \verb+\/+ \cons{} \vb{} \cons{} \verb+->+ \cons{} \vb{} + \cons{} \verb+<->+ \cons{} \\ + & \arrow & \texttt{forall(} \arrayb{} \texttt{)} \vb{} + \texttt{exists(} \arrayb{} \texttt{)} + \vb{} \arrayb[\term{}] \\ + & \arrow & + \cname \texttt{(}\term{}, \ldots, \term{} \texttt{)} \vb{} \texttt{if} \cons{} \texttt{then} \cons{} \texttt{else} + \cons{} \texttt{endif} \\ + & \arrow & \texttt{let \{} \decls{} \optcons{} \texttt{\} in} \cons{} \\ +\term{} & \arrow & \intc{} \vb{} \ivar{} \vb{} \term{} \aop{} \term{} \vb{} +\arrayi[\term{}] \vb{} \texttt{sum(} \arrayi \texttt{)} +\\ +& \arrow & \texttt{if} \cons{} \texttt{then} \term{} \texttt{else} + \term{} \texttt{endif} \vb{} +\texttt{bool2int(} \cons{} \texttt{)} \\ + & \arrow & \texttt{let \{} \decls{} \optcons{} \texttt{\} in} \term{} \\ +\arrayb{} & \arrow & \verb+[+ \cons{}, \ldots, \cons{} +\verb+]+ \vb{} \verb+[+ \cons{} \verb+|+ \ivar{} \texttt{in} \term{} \texttt{..} +\term{} \verb+]+ \\ +\arrayi{} & \arrow & \verb+[+ \term{}, \ldots, \term{} \verb+]+ \vb{} + \verb+[+ \term{} \verb+|+ \ivar{} \texttt{in} \term{} \texttt{..} +\term{} \verb+]+ \\ +\end{tabular} + +\vspace{2mm} +The grammar uses the symbols +\bvar{} for Boolean variables, +\relop{} for relational operators +$\{$ \texttt{==}, \texttt{<=}, \texttt{<}, +\texttt{!=}, \texttt{>=}, \texttt{>} $\}$, +\cname{} for names of predicates, +\intc{} for integer constants, +\ivar{} for integer variables, and +\aop{} for arithmetic operators +$\{$ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{div} $\}$. + +In the \texttt{let} constructs we make use of the nonterminal +\decls{} for declarations. We define this below using +\decli{} for integer variable declarations, +\declb{} for Boolean variable declarations. +We use \optcons{} for optional constraint items appearing in let declarations. +We also define \args{} as a list of integer variable declarations, +an item \itm{} as either a predicate declaration, +a constraint or a function declaraions, +\itms{} as a list of items, +\solve{} as a solve directive either satisfaction or an objective, +and a model \model{} as +some declarations followed by items followed by a solve item. +Note that $\epsilon$ represents the empty string. + +\vspace{2mm} +\noindent +\begin{tabular}{rcl} +\decli{} & \arrow & \texttt{int:} \ivar{} +\vb{} \texttt{var int:} \ivar{} + \vb{} +% \term{} \texttt{..} \term{} \texttt{:} \ivar \vb{} +\texttt{var} \term{} \texttt{..} \term{} \texttt{:} \ivar{} \\ +\declb{} & \arrow & \texttt{bool:} \bvar{} \vb{} \texttt{var bool:} \bvar{} \\ +\decls{} & \arrow & $\epsilon$ \vb{} \decli{}\texttt{;} \decls{} \vb{} \decli{} +\texttt{=} \term{}\texttt{;} \decls{} \vb{} +\declb{}\texttt{;} \decls{} \vb{} \declb{} \texttt{=} \cons{}\texttt{;} +\decls{} \\ +\optcons{} & \arrow & $\epsilon$ \vb{} \texttt{constraint} \cons{} \texttt{;} +\optcons{} \\ +\args{} & \arrow & \texttt{var} \texttt{int:} \ivar{} \vb{} +\texttt{var} \texttt{int:} \ivar{} + \texttt{,} \args{} \vb{} \texttt{int:} \ivar{} \vb{} +\texttt{int:} \ivar{} + \texttt{,} \args{} \\ +\itm{} & \arrow & \texttt{predicate} \cname \texttt{(} \args \texttt{)} = +\cons{}\texttt{;} \vb{} \texttt{constraint} \cons{}\texttt{;} \vb{} \\ + & \arrow & \texttt{function} \texttt{var int :} \fname \texttt{(} \args{} \texttt{)} = +\term{} \texttt{;} \\ %\vb{} ~\\ +%\args{} & \arrow & \decli{} \vb{} \decli{} \texttt{,} \args{} \\ +\itms{} & \arrow & $\epsilon$ \vb{} \itm{} \itms{} \\ +\solve{} & \arrow & \texttt{satisfy} \texttt{;} \vb{} \texttt{minimize} +\term{} \texttt{;} \vb{} +\texttt{maximize} \term \texttt{;} \\ +\model{} & \arrow & \decls{} \itms{} \texttt{solve} \solve{} \\ +\end{tabular} +\vspace{2mm} + + +The main missing things are floats, long linear constraints, and set and array +variables. It misses many built-in operators and functions, but their treatment +is analogous to those we include. To simplify presentation, we assume all +predicate and function arguments are integers, but the translation can be +extended to arbitrary arguments in a straightforward way. + + +\subsection{Further Notation} + +Given an expression $e$ that contains the subexpression $x$, we denote by +$e\subs{x/y}$ the expression that results from replacing all occurrences of +subexpression $x$ by expression $y$. We will also use the notation for multiple +simultaneous replacements $\subs{\bar{x}/\bar{y}}$ where each $x_i \in \bar{x}$ +is replaced by the corresponding $y_i \in \bar{y}$. + +Given a \cons{} term defining the constraints of the model we can split its +\cons{} subterms as occurring in different kinds of places: root contexts, +positive contexts, negative contexts, and mixed contexts. A Boolean subterm $t$ +of constraint $c$ is in a \emph{root context} iff there is no solution of +$c\subs{t/\false}$, that is $c$ with subterm $t$ replaced by $\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/\true}$; and a \emph{negative context} iff for any solution +$\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\false}$. The +remaining Boolean subterms of $c$ are in \emph{mixed} contexts. While +determining contexts according to these definitions is hard, there are simple +syntactic rules which can determine the correct context for most terms, and the +rest can be treated as mixed. + +Consider the constraint expression + +\begin{mzn} + constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5); +\end{mzn} + +then $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. + + +We assume each integer variable $x$ is separately declared with a finite initial +set of possible values $D_{init}(x)$. We assume each array constant is +separately declared as a mapping $\{ i \mapsto d ~|~ i \in \dom(a) \}$ where its +index set $\dom(a)$ is a finite integer range. Given these initial declarations, +we can determine the set of possible values $poss(t)$ of any term $t$ in the +language as $poss(t) = \{ \theta(t) ~|~ \theta \in D_{init} \}$. Note also while +it may be prohibitive to determine the set of possible values for any term $t$, +we can efficiently determine a superset of these values by building a superset +for each subterm bottom up using approximation. + +% Given a \cons{} term defining the constraints of the model we can split its +% \cons{} subterms as occurring in kinds of places: positive contexts, negative +% contexts, and mixed contexts. A Boolean subterm $t$ of constraint $c$, written +% $c[t]$, is in a \emph{positive context} iff for any solution $\theta$ of $c$ +% then $\theta$ is also a solution of $c[\true]$, that is $c$ with subterm $t$ +% replaced by $\true$. Similarly, a subterm $t$ of constraint $c$ is in a +% \emph{negative context} iff for any solution $\theta$ of $c$ then $\theta$ is +% also a solution of $c[\false]$. The remaining Boolean subterms of $c$ are in +% mixed contexts. + +% \begin{example} +% Consider the constraint expression $c$ \negspace +% \begin{mzn} +% constraint i <= 4 -> x + bool2int(b) = 5; +% \end{mzn} +% then $i \leq 4$ is in a negative context, $x + \texttt{bool2int}(b) = 5$ is +% in a positive context, and $b$ is in a mixed context. If the last equality +% were $x + \texttt{bool2int}(b) \geq 5$ then $b$ would be in a positive +% context. \qed +% \end{example} + +% One can classify most contexts as positive or negative using a simple top-down +% analysis of the form of the expression. The remaining contexts can be +% considered mixed without compromising the correctness of the rest of the +% paper. + +Our small language contains two partial functions: \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)$. + +\section{Flattening with Full Reification} +\label{sec:translation} + +Constraint problems formulated in \minizinc\ are solved by translating them to a +simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc +consists only of a sequence of variables declarations and a conjunction of +constraints. This section shows how to translate our extended \minizinc\ to +\flatzinc. The usual method for flattening complex formula of constraints is +full reification. Given a constraint $c$ the \emph{full reified form} for $c$ is +$b \full c$, where $b \not\in vars(c)$ is a Boolean variable naming the +satisfied state of the constraint $c$. + +% The complexities in the translation arise from the need to simultaneously (a) +% unroll array comprehensions (and other loops), (b) replace predicate and +% function applications by their body, and (c) flatten expressions. + +% Once we take into account CSE, we cannot perform these separately. +% In order to have names for common subexpressions we need to flatten +% expressions. And in order to take advantage of functions +% for CSE we cannot replace predicate and function applications without +% flattening to generate these names. And without replacing predicate and +% function application by their body we are unable to see all the loops to +% unroll. + +\newcommand{\ctxt}{\ensuremath{\mathit{ctxt}}} +\newcommand{\rootc}{\textsl{root}} +\newcommand{\pos}{\textsl{pos}} +\newcommand{\negc}{\textsl{neg}} +\newcommand{\mix}{\textsl{mix}} +\newcommand{\cupp}{\ensuremath{\cup}\text{:=}~} +\newcommand{\posop}{\ensuremath{+}} +\newcommand{\negop}{\ensuremath{-}} +\newcommand{\fixed}{\textsf{fixed}} +\newcommand{\eval}{\textsf{eval}} + +The translation algorithm presented below generates a flat model equivalent to +the original model as a global set of constraints $S$. We ignore the collection +of variable declarations, which is also clearly important, but quite +straightforward. The translation uses full reification to create the model. + +Common subexpression elimination is implemented using a technique similar to +\emph{hash-consing} in Lisp \autocite{allen-1978-lisp}. For simplicity we only +show syntactic CSE, which eliminates expressions that are identical after +parameter replacement. The extension to semantic CSE, using commutativity and +other equivalences, is well understood (see \autocite{rendl-2010-thesis} for a +detailed discussion) but makes the pseudo-code much longer. + +The complex part of flattening arises in flattening the constraints, we shall +ignore the declarations part for flattening and assume that any objective +function term $e$ is replaced by a new variable $obj$ and a constraint item +$\texttt{constraint}~ obj = e$ which will then be flattened as part of the +model. + +\subsection{Flattening Constraints} + +Flattening a constraint $c$ in context $\ctxt$, $\flatc(c,\ctxt)$, returns a +Boolean literal $b$ representing the constraint and as a side effect adds a set +of constraints (the flattening) $S$ to the store such that +$S \models b \full c$. + +It uses the context ($\ctxt$) to decide how to translate, where possible +contexts are: \rootc, at the top level conjunction; \pos, positive context, +\negc, negative context, and \mix, mixed context. We use the context operations +$\posop$ and $\negop$ defined as: + +\centerline{ +\begin{tabular}{ccc} +$ +\begin{array}{lcl} +\posop \rootc & = &\pos \\ +\posop \pos & =& \pos \\ +\posop \negc & =& \negc, \\ +\posop \mix & =& \mix +\end{array} +$ +& ~~~ & +$ +\begin{array}{lcl} +\negop \rootc & = &\negc \\ +\negop \pos & =& \negc \\ +\negop \negc & =& \pos, \\ +\negop \mix & =& \mix +\end{array} +$ +\end{tabular} +} + +% \centerline{ +% \begin{tabular}{ccccccc} +% $ +% \begin{array}{lcl} +% \posop \rootc & = &\pos \\ +% \posop \pos & =& \pos +% \end{array} +% $ +% & ~~~ & +% $ +% \begin{array}{lcl} +% \posop \negc & =& \negc, \\ +% \posop \mix & =& \mix +% \end{array} +% $ +% & ~~~ & +% $ +% \begin{array}{lcl} +% \negop \rootc & = &\negc \\ +% \negop \pos & =& \negc +% \end{array} +% $ +% & ~~~ & +% $ +% \begin{array}{lcl} +% \negop \negc & =& \pos, \\ +% \negop \mix & =& \mix +% \end{array} +% $ +% \end{tabular} +% } + +% $\negop$ and $\posop$ as $\negop \rootc = \negc$, $\negop \pos = \negc$, +% $\negop \negc = \pos$, $\negop \mix = \mix$; and +% $\posop \rootc = \pos$, +% $\posop \pos = \pos$, +% $\posop \negc = \negc$, +% $\posop \mix = \mix$, + +Note that flattening in a $\mix$ context is the most restrictive case, and the +actual flattening rules only differentiate between $\rootc$ and other contexts. +The importance of the $\pos$ context is that \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 $\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. + + +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 +$\true$ in $S$, and modify the hash table to record the expression appears at +the root. If the expression appeared in a mixed context we simply reuse the old +result since this is the most constrained context. Similarly if the previous +context is the same as the current one we reuse the old result. In the remaining +cases we set the context to $\mix$ since the remaining cases require at least +both a $\pos$ and $\negc$ or a $\mix$ context. Note that if an expression +introduces a fresh variable and it appears first in a negative context and only +later in the root context, the translation aborts. This could be fixed in a +preprocessing step that sorts expressions according to their context. + + +The flattening proceeds by evaluating fixed Boolean expressions and returning +the value. We assume $\fixed$ checks if an expression is fixed (determined +during \minizinc's type analysis), and $\eval$ evaluates a fixed expression. For +simplicity of presentation, we assume that fixed expressions are never undefined +(such as \lstinline|3 div 0|). We can extend the algorithms to handle this case, +but it complicates the presentation. Our implementation aborts in this +case.\pjs{CHECK and FIX!} While this does not agree with the relational +semantics it likely indicates a modelling error since a fixed part of the model +must be undefined. The abort forces the user to redefine the model to avoid +this. + + +\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. +% 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.\short{\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 $\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} ($prev =\rootc$) \textbf{return} $h$ \\ +\>\> \textbf{if} ($ctxt = \rootc$) $S$ \cupp $\{ h \}$; hash[$c$] := +$\tuple{h,\rootc}$; \textbf{return} $h$ +\\ +\>\> \textbf{if} ($prev = \mix \vee prev = \ctxt$) +\textbf{return} $h$ \\ +\>\> $\ctxt$ := $\mix$ \\ +\> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\ +\> \textbf{else} \\ +\> \> \textbf{switch} $c$ \\ +%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ +%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ +\> \> \textbf{case} $b'$ (\bvar): $b$ := $b'$; \\ +\> \> \textbf{case} $t_1$ $r$ $t_2$ (\relop): \\ +\>\>\> $\tuple{v_1, b_1}$ := $\flatt(t_1,\ctxt)$; +$\tuple{v_2, b_2}$ := $\flatt(t_2,\ctxt)$; \\ +\> \> \> $S$ \cupp $\{ \new b \full (b_1 \wedge b_2 \wedge \new b'), b' \full v_1~r~v_2\}$ \\ +\> \> \textbf{case} \texttt{not} $c_1$: +$b$ := $\neg \flatc(c_1, \negop \ctxt)$ \\ +\> \> \textbf{case} $c_1$ \verb+/\+ $c_2$: $S$ \cupp $\{ \new b \full (\flatc(c_1, \ctxt) \wedge \flatc(c_2, \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+\/+ $c_2$: +$S$ \cupp $\{ \new b \full (\flatc(c_1,\posop \ctxt) \vee \flatc(c_2,\posop \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+->+ $c_2$: +$S$ \cupp $\{ \new b \full (\flatc(c_1,\negop \ctxt) \half \flatc(c_2,\posop \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+<->+ $c_2$: +$S$ \cupp $\{ \new b \full (\flatc(c_1,\mix) \full +\flatc(c_2,\mix))\}$ +\\ +\> \> \textbf{case} \texttt{forall(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\flatc(c_j, \ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \full \bigwedge_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} \texttt{exists(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\flatc(c_j, +\ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \full \bigvee_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} $[c_1, \ldots, c_n]$ \texttt{[} $t$ \texttt{]}: \\ +\>\>\> +\textbf{foreach}($j \in 1..n$) $b_j$ := $\flatc(c_j, \posop \ctxt)$; \\ +\>\>\> $\tuple{v, b_{n+1}}$ := $\flatt(t, \ctxt)$; \\ +%\>\>\> $S$ \cupp +%$\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), +%\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), +%b'' \full v \in \{1,..,n\} \} $ \\ +\>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\texttt{element}(v', [b_1, \ldots, b_n], +\true)\}$; $b$ := $\true$ \\ +\>\>\> \textbf{else} \\ +\>\>\>\> $S$ \cupp +$\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, +\ldots, n\},$ \\ +\>\>\>\>\>\>\> $\texttt{element}(v', [b_1, \ldots, b_n], b'), +b'' \full v = v', b'' \full v \in \{1,..,n\} \} $ +\\ +\callbyvalue{ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := $\flatt(t_j,\ctxt)$; \\ +\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \\ +\> \> \> \> \textbf{if} ($p\_reif$ does not exist) \textbf{abort} \\ +\> \> \> \> \textbf{else} $S$ \cupp $\{ p\_reif(v_1,\ldots,v_n,\new b'), +\new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}$ \\ +\> \> \> \textbf{else} \\ +\>\> \> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j +\}$ +\\ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): user-defined predicate \\ +\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := $\flatt(t_j,\ctxt)$; \\ +\>\> \> $\new b'$ := $\flatc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)$ +\\ +\> \>\> $S$ \cupp $\{ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n +b_j\}$ +\\ +} +\callbyunroll{ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\ +\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ +\>\> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ +\\ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): 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}: +% \\ \> \> \> +\textbf{if} ($\eval(c_0)$) $b$ := $\flatc(c_1,\ctxt)$ \textbf{else} $b$ := $\flatc(c_2,\ctxt)$ \\ +\>\> \textbf{case} \texttt{let \{} $d$ \texttt{\} in} $c_1$: \\ +\>\> \> \textbf{let} $\bar{v}'$ be a renaming of variables $\bar{v}$ defined +in $d$ \\ +\> \> \> $\tuple{c',\_}$ := $\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, +c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)$ \\ +\> \> \> $b$ := $\flatc(c',\ctxt)$; +\\ +\> \> \textbf{endswitch} \\ +\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{ b \}$; \\ +\> hash[$c$] := $\tuple{b,\ctxt}$ \\ +\> \textbf{return} $b$ +\end{tabbing} +} + +The function \evalb{} replaces an array comprehension by the resulting array. +Note that terms $\mathit{lt}$ and $\mathit{ut}$ must be fixed in a correct +\minizinc\ model. + +\begin{tabbing} +xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +\evalb($t$) \\ +\> \textbf{switch} $t$ \\ +\> \textbf{case} \verb+[+ $t_1, \ldots, t_n$ \verb+]+: + \textbf{return} \verb+[+ $t_1, \ldots, t_n$ \verb+]+ + \\ +\> \textbf{case} \verb+[+ $e$ \verb+|+ $v$ \texttt{in} $\mathit{lt}$ \texttt{..} $\mathit{ut}$ +\verb+]+: + \\ \> \> +\textbf{let} $l = \eval(\mathit{lt})$, $u = \eval(\mathit{ut})$ + \\ \> \> +\textbf{return} \verb+[+ $e\subs{v/l}$, $e\subs{v/l+1}$, +\ldots $e\subs{v/u}$ \verb+]+ +\end{tabbing} + +\subsection{Handling \texttt{let} Expressions} + +Much of the handling of a \texttt{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. + +{%\small +\begin{tabbing} +xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +\textsf{flatlet}($d$,$c$,$t$,$\ctxt$) \\ +\> \textbf{foreach} ($item \in d$) \\ +\> \> \textbf{switch} $item$ \\ +\> \> \textbf{case} \texttt{var bool :} $b = c'$ : \= \kill +\> \> \textbf{case} \texttt{bool :} $b = c'$ : \> $d$ := +$d\subs{b/\eval(c')}$; \= $c$ := $c\subs{b/\eval(c')}$; \= \kill +%\> \> \textbf{case} \texttt{$l$ .. $u$ :} $v = t'$ : \> $d$ := +%$d\subs{v/\eval(t')}$; \> $c$ := $c\subs{v/\eval(t')}$; \> $t$ := $t\subs{v/\eval(t')}$ \\ +\> \> \textbf{case} \texttt{int :} $v = t'$ : \> $d$ := $d\subs{v/\eval(t')}$; +\> $c$ := $c\subs{v/\eval(t')}$; \> $t$ := $t\subs{v/\eval(t')}$\\ +\> \> \textbf{case} \texttt{bool :} $b = c'$ : \> $d$ := +$d\subs{b/\eval(c')}$; \> $c$ := $c\subs{b/\eval(c')}$; \> $t$ := $t\subs{b/\eval(c')}$ +\\ +%\> \textbf{endfor} \\ +\> \textbf{foreach} ($item \in d$) \\ +\> \> \textbf{switch} $item$ \\ +%\> \> \textbf{case} \texttt{$l$ .. $u$ :} $v = t'$ : \> $c$ := $c$ \verb+/\+ $l$ +%\texttt{<=} $v$ \verb+/\+ $v$ \texttt{<=} $u$ \\ +\> \> \textbf{case} \texttt{var int :} $v$ : \> \textbf{if} ($\ctxt \in +\{\negc,\mix\}$) \textbf{abort} \\ +\> \> \textbf{case} \texttt{var int :} $v = t'$ : +\> $\tuple{v',b'}$ := $\flatt(t',\ctxt)$; +$S$ \cupp $\{v = v'\}$; $c$ := $c$ \verb+/\+ $b'$ +\\ +\> \> \textbf{case} \texttt{var} $l$ \texttt{..} $u$ \texttt{:} $v$ : \> +\textbf{if} ($\ctxt \in +\{\negc,\mix\}$) \textbf{abort} \textbf{else} $c$ := $c$ +\verb+/\+ $l$ \texttt{<=} $v$ \verb+/\+ $v$ \texttt{<=} $u$ + \\ +\> \> \textbf{case} \texttt{var} $l$ \texttt{..} $u$ \texttt{:} $v = t'$ : +\> $\tuple{v',b'}$ := $\flatt(t',\ctxt)$; +$S$ \cupp $\{v = v'\}$; \\ +\> \> \> $c$ := $c$ \verb+/\+ $b'$ +\verb+/\+ $l$ \texttt{<=} $v$ \verb+/\+ $v$ \texttt{<=} $u$; +\\ +\> \> \textbf{case} \texttt{var bool :} $b$ : \> \textbf{if} ($\ctxt \in +\{\negc,\mix\}$) \textbf{abort} \\ +\> \> \textbf{case} \texttt{var bool :} $b = c'$ : \> +$c$ := $c$ +\verb+/\+ ($b$ \verb+<->+ $c'$) \\ +\> \> \textbf{case} \texttt{constraint} $c'$ : \> $c$ := $c$ +\verb+/\+ $c'$ \\ +\> \> \textbf{endswitch} \\ +\> \textbf{return} $\tuple{c,t}$ +\end{tabbing} +} + +\subsection{Flattening Integer Expressions} + +$\flatt(t,\ctxt)$ flattens an integer term $t$ in context $\ctxt$. It returns a +tuple $\tuple{v,b}$ of an integer variable/value $v$ and a Boolean literal $b$, +and as a side effect adds constraints to $S$ so that +$S \models b \full (v = t)$. Note that again flattening in the root context +always returns a Boolean $b$ made equivalent to $\true$ by the constraints in +$S$. + +Flattening first checks if the same expression has been flattened previously and +if so returns the stored result. \flatt{} evaluates fixed integer expressions +and returns the result. +% For non-fixed integer expressions $t$, if $t$ +% is determined to be total, it changes the context to +% $\rootc$ since this is safe. +For non-fixed integer expressions $t$ each form is treated in turn. Simple +integer expressions are simply returned. Operators have their arguments +flattened and the new value calculated on the results. A safe form of division +is used, introducing a new variable $v'2$ as the divisor which can never be +zero, and a new Boolean $b'$ captures when the division is defined. Array lookup +flattens all the integer expressions involved and creates a $\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. + +\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} ($prev =\rootc$) +\textbf{return} $\tuple{h,b'}$ \\ +\>\> \textbf{if} ($ctxt = \rootc$) $S$ \cupp $\{ b' \}$; hash[$t$] := +$\tuple{h,b',\rootc}$; \textbf{return} $\tuple{h,b'}$ +\\ +\>\> \textbf{if} ($prev = \mix \vee prev = \ctxt$) +\textbf{return} $\tuple{h,b'}$ \\ +\>\> $\ctxt$ := $\mix$ \\ +\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\ +\> \textbf{else} %\\ +%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ +%\> \> +\textbf{switch} $t$ \\ +%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\ +\> \> \textbf{case} $v'$ (\ivar): $v$ := $v'$; $b$ := $\true$\\ +\> \> \textbf{case} $t_1$ $a$ $t_2$ (\aop): \\ +\> \> \> +$\tuple{v_1,b_1}$ := $\flatt(t_1,\ctxt)$; +$\tuple{v_2,b_2}$ := $\flatt(t_2,\ctxt)$; \\ +\> \> \> \textbf{if} ($a \not\equiv \texttt{div} \vee \ctxt = \rootc$) +$S$ \cupp $\{ \new b \full (b_1 \wedge b_2), a(v_1,v_2,\new v) \}$ \\ +%\> \> \> \textbf{else} $S$ \cupp $\{ \new b \full (b_1 \wedge b_2 \wedge +%\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}$ \\ +\> \> \> \textbf{else} $S$ \cupp $\{ \new b \full (b_1 \wedge b_2 \wedge +\new b'), \new v_2' \neq 0,$ \\ +\> \> \> \> \> \>\>\> $\texttt{div}(v_1,v_2',\new v), b' \full v_2 \neq 0, b' \full +v_2 = v_2' \}$ \\ +\> \> \textbf{case} $[t_1, \ldots, t_n]$ \texttt{[} $t_{0}$ \texttt{]}: \\ +\> \> \> +\textbf{foreach}($j \in 0..n$) $\tuple{v_j, b_j}$ := $\flatt(t_j,\ctxt)$; \\ +%\>\> \> $S$ := +%$\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), +%\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n], \new v), +%b' \full v_0 \in \{1,...,n\} \}$ +%\\ +\>\>\> \textbf{if} ($\ctxt \neq \rootc$) \\ +\>\>\>\> $S$ \cupp +$\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), \new v' \in \{1, +\ldots, n\},$ \\ +\>\>\>\>\>\>\> $\texttt{element}(v', [v_1, \ldots, v_n], \new v), +b' \full v_0 = v', b' \full v_0 \in \{1,..,n\} \} $ +\\ +\>\>\> \textbf{else} $S$ \cupp $\{\new b, \texttt{element}(v', [v_1, \ldots, v_n], +\new v) \}$ \\ +\> \> \textbf{case} \texttt{sum(} $\mathit{ia}$ \texttt{)}: \\ +\> \> \> \textbf{let} $[t_1, \ldots, t_n] = \evalb(ia)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := +$\flatt(t_j,\ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \full \bigwedge_{j=1}^n b_j, + \new v = \sum_{j=1}^n v_j \}$ \\ +%\> \> \> +%$\tuple{v,b}$ := \flatt( +%\textsf{foldl}($\evalb(ia)$, \texttt{0}, \texttt{+}), $\ctxt$) +%\\ +\> \> \textbf{case} \texttt{if} $c_0$ \texttt{then} $t_1$ \texttt{else} +$t_2$ \texttt{endif}: +% \\ \> \> \> +\textbf{if} ($eval(c_0)$) $\tuple{v,b}$ := $\flatt(t_1,\ctxt)$ \textbf{else} +$\tuple{v,b}$ := $\flatt(t_2,\ctxt)$ +\\ +\>\> \textbf{case} \texttt{bool2int(} $c_0$ \texttt{)}: + $b_0$ := $\flatc(c_0, \mix)$; + $S$ \cupp $\{ \texttt{bool2int}(b_0, \new v), \new b \}$ \\ +\callbyvalue{ +\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): function \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := $\flatt(t_j,\ctxt)$; \\ +\>\> \> \textbf{let} $f(x_1, \ldots, x_n) = t_0$ be defn of $f$ \\ +\> \> \> \textbf{if} ($f$ is declared total) $\ctxt' = \rootc$ \textbf{else} +$\ctxt' = \ctxt$ \\ +\>\> \> $\tuple{v,b'}$ := $\flatt(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt')$ \\ +\> \> \> $S$ \cupp $\{ \new b \full b' \wedge \bigwedge_{j=1}^n b_j \}$ +\\ +} +\callbyunroll{ +\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): 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$) (\fname): 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$; \\ +%\>\> \> \textbf{let} $f(x_1, \ldots, x_n) = t'$ be defn of $p$ \\ +%\>\> \> $\tuple{v,b}$ := $\flatt(t'\subs{x_1/w_1, \ldots, x_n/w_n},\rootc)$ +%\\ +%\>\> \> $S$ \cupp $\{ b \half (v_1=w_1 \wedge \ldots \wedge v_n=w_n)\}$\\ +\>\> \textbf{case} \texttt{let \{} $d$ \texttt{\} in} $t_1$: \\ +\>\> \> \textbf{let} $\bar{v}'$ be a renaming of variables $\bar{v}$ defined +in $d$ \\ +\> \> \> $\tuple{c',t'}$ := $\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true}, +t_1\subs{\bar{v}/\bar{v}'},\ctxt)$ \\ +\>\> \> $\tuple{v,b_1}$ := $\flatt(t',\ctxt)$; +$b_2$ := $\flatc(c',\ctxt)$; +$S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ +\\ +\> \> \textbf{endswitch} \\ +\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{ b \}$; \\ +\> hash[$t$] := $\tuple{v,b,\ctxt}$ \\ +\> \textbf{return} $\tuple{v,b}$ +\end{tabbing} + +\begin{example}\label{ex:flat} + Consider the flattening of the expression + $$ + a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee + (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b)) + $$ + The different terms and subterms of the expression are + illustrated and numbered in Figure~\ref{fig:tree}. + \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] \\ + && ~-^{(3)} \ar[dl]\ar[dr] && 4 && ~~\wedge^{(4)} \ar[dl]\ar[dr] &&& + ~~\rightarrow^{(5)} \ar[d]\ar[dr] &&& \\ + & ~+^{(6)} \ar[dr]\ar[dl] && bool2int^{(7)} \ar[d] && + \leq^{(8)}\ar[dr]\ar[d] && ~>^{(9)}\ar[dr]\ar[d] && ~>^{(10)}\ar[dr]\ar[d] & + b \\ + []^{(11)}\ar[dr]\ar[d] &&bool2int^{(12)}\ar[d] & ~>^{(13)}\ar[dr]\ar[d] && + []^{(14)} \ar[dr]\ar[d] & 2 &x &y &x &z &&&&& \\ + a &x & ~>^{(15)}\ar[dr]\ar[d]& x&z &a &x \\ + & & x & y && \\ + } + $$ + \caption{An expression to be flattened with non-leaf (sub-)terms + numbered.\label{fig: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. + + The result of flattening with full reification is: + + \begin{mzn} + constraint b0 <-> b1 \/ b2; + constraint b0; + constraint b1 <-> b2 /\ b1'; + constraint b1' <-> v3 >= 4; + constraint b2 <-> b4 /\ b5; + constraint b3 <-> b6 /\ b7; + constraint minus(v6, v7, v3); + constraint b4 <-> b8 /\ b9; + constraint b5 <-> (b10 -> b); + constraint b6 <-> b11 /\ b12; + constraint plus(v11, v12, v6); + constraint b7; + constraint bool2int(b10, v7); + constraint b8 <-> b11 /\ b8' + constraint b8' <-> v11 <= 2; + constraint b9 <-> x > y; + constraint b10 <-> x > z; + constraint b11 <-> b11'; + constraint v11' in 1..n; + constraint element(v11', a, v11); + constraint b11' <-> v11' = x; + constraint b11' <-> x in 1..n; + constraint b12; + constraint bool2int(b9, v12); + \end{mzn} + + % $b_0 \full b_1 \vee b_2$, $b_0$, + % $b_1 \full b_2 \wedge b_1'$, $b_1' \full v_3 \geq 4$, + % $b_2 \full b_4 \wedge b_5$, + % $b_3 \full b_6 \wedge b_7$, $minus(v_6,v_7,v_3)$, + % $b_4 \full b_8 \wedge b_9$, + % $b_5 \full (b_{10} \rightarrow b)$, + % $b_6 \full b_{11} \wedge b_{12}$, $plus(v_{11},v_{12},v_6)$, + % $b_7$, $bool2int(b_{10},v_7)$, + % $b_8 \full b_{11} \wedge b'_8$, $b'_8 \full v_{11} \leq 2$, + % $b_9 \full x > y$, + % $b_{10} \full x > z$, + % $b_{11} \full b'_{11}$, $v'_{11} \in \{1, \ldots, n\}$, + % $element(v'_{11}, a, v_{11})$, $b'_{11} \full + % v'_{11} = x$, $b'_{11} \full x \in \{1, \ldots, n\}$, + % $b_{12}$, $bool2int(b_{9}, v_{12})$ + where we use the position as underscore on the variable. Note that we use CSE + to reuse variables from position 11 for position 14, position 9 for position + 15, and position 10 for position 13. We dont expand the array $a$ for + simplicity, we assume it has $n$ entries. We can simplify the resulting + formulae by removing always true literals and replacing equivalent literals, + resulting in + + \begin{mzn} + constraint b1 \/ b2; + constraint b1 <-> b3 /\ b1'; + constraint b1' <-> v3 >= 4; + constraint b2 <-> b4 /\ b5; + constraint minus(v6, v7, v3); + constraint b4 <-> b8 /\ b9; + constraint b5 <-> (b10 -> b); + constraint plus(v11, v12, v6); + constraint bool2int(b10, v7); + constraint b8 <-> b3 /\ b8' + constraint b8' <-> v11 <= 2; + constraint b9 <-> x > y; + constraint b10 <-> x > z; + constraint v11' in 1..n; + constraint element(v11', a, v11); + constraint b3 <-> v11' = x; + constraint b3 <-> x in 1..n; + constraint bool2int(b9, v12); + \end{mzn} + + % $b_1 \vee b_2$, + % $b_1 \full b_3 \wedge b_1'$, $b_1' \full v_3 \geq 4$, + % $b_2 \full b_4 \wedge b_5$, + % $minus(v_6,v_7,v_3)$, + % $b_4 \full b_8 \wedge b_9$, + % $b_5 \full (b_{10} \rightarrow b)$, + % $plus(v_{11},v_{12},v_6)$, + % $bool2int(b_{10},v_7)$, + % $b_8 \full b_{3} \wedge b'_8$, $b'_8 \full v_{11} \leq 2$, + % $b_9 \full x > y$, + % $b_{10} \full x > z$, + % $v'_{11} \in \{1, \ldots, n\}$, $element(v'_{11}, a, v_{11})$, $b_{3} \full + % v'_{11} = x$, $b_{3} \full x \in \{1, \ldots, n\}$, + % $bool2int(b_{9}, v_{12})$; + a total of 18 primitive constraints and 14 intermediate variables introduced. +\end{example} +\jip{Maybe make this fit better} + +% Since the constraint solver only deals with a flat conjunction of constraints, +% modelling languages that support more complex constraint forms need to +% \emph{flatten} them into a form acceptable to the solver. The usual method for +% flattening complex formula of constraints is full reification. Given a +% constraint $c$ the \emph{full reified form} for $c$ is $b \full c$, where +% $b \not\in vars(c)$ is a Boolean variable naming the satisfied state of the +% constraint $c$. + +% %\newcommand{\new}{\textbf{new}~} +% %\newcommand{\flatc}{\textsf{flatc}} +% %\newcommand{\flatt}{\textsf{flatt}} +% \newcommand{\safen}{\textsf{safen}} + +% The pseudo-code for \flatc($b$,$c$) flattens a constraint expression $c$ to be +% equal to $b$, returning a set of constraints implementing $b \full c$. We +% flatten a whole model $c$ using $\flatc(\true, c)$. In the pseudo-code the +% expressions $\new b$ and $\new v$ create a new Boolean and integer variable +% respectively. + +% The code assumes there are reified versions of the basic relational +% constraints $r$ available, as well as reified versions of the Boolean +% connectives. Flattening of arbitrary constraint predicates aborts if not at +% the top level of conjunction. The code handles unsafe terms by capturing them +% when they first arrive at a Boolean context using \safen. + +% {\small +% \begin{tabbing} +% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +% \flatc($b$,$c$) \\ +% \> \textbf{switch} $c$ \\ +% \> \textbf{case} \texttt{true}: \textbf{return} $\{ b \}$ \\ +% \> \textbf{case} \texttt{false}: \textbf{return} $\{ \neg b \}$ \\ +% \> \textbf{case} $b'$ (\bvar): \textbf{return} $\{ b \full b' \}$ \\ +% \> \textbf{case} $t_1$ $r$ $t_2$ (\relop): \textbf{return} $\safen(b, \flatt(\new i_1, t_1) \cup \flatt(\new i_2, t_2)) \cup \{ b \full i_1~r~i_2 \}$ \\ +% \> \textbf{case} \texttt{not} $c_1$: +% \textbf{return} $\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}$ \\ +% \> \textbf{case} $c_1$ \verb+/\+ $c_2$: \= +% \textbf{if} ($b \equiv \true$) \textbf{return} $\flatc(\true, c_1) \cup +% \flatc(\true, c_2)$ \\ +% \> \> \textbf{else} \textbf{return} $\flatc(\new b_1, c_1) \cup +% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}$ \\ +% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +% \> \textbf{case} $c_1$ \verb+\/+ $c_2$: \textbf{return} $\flatc(\new b_1, c_1) \cup +% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \vee +% b_2)\}$ \\ +% \> \textbf{case} $c_1$ \verb+->+ $c_2$: \textbf{return} $\flatc(\new b_1, c_1) \cup +% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \half +% b_2)\}$ \\ +% \> \textbf{case} $c_1$ \verb+<->+ $c_2$: \textbf{return} $\flatc(\new b_1, c_1) \cup +% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full +% b_2)\}$ \\ +% \> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): \\ +% \> \> \textbf{if} ($b \equiv \true$) \textbf{return} $\safen(b, +% \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}$ \\ +% \> \> \textbf{else} \textbf{abort} +% \end{tabbing} +% } + +% The code $\flatt(v,t)$ flattens an integer term $t$, creating constraints +% that equate the term with variable $v$. It creates new variables to store +% the values of subterms, replaces integer operations by their relational +% versions, and array lookups by \element. + +% \begin{tabbing} +% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +% \flatt($v$,$t$) \\ +% \> \textbf{switch} $t$ \\ +% \> \textbf{case} $i$ (\intc): \textbf{return} $\{v = i\}$ \\ +% \> \textbf{case} $v'$ (\ivar): \textbf{return} $\{ v = v' \}$ \\ +% \> \textbf{case} $t_1$ $a$ $t_2$ (\aop): +% \textbf{return} $\flatt(\new v_1, t_1) \cup \flatt(\new v_2, t_2) \cup \{ a(v_1, v_2, v) \}$ \\ +% \> \textbf{case} $a$ \texttt{[} $t_1$ \texttt{]}: +% \textbf{return} $\flatt(\new v_1, t_1) \cup \{ \texttt{element}(v_1, a, v) \}$ \\ +% \> \textbf{case} \texttt{bool2int(} $c_1$ \texttt{)}: +% \textbf{return} $\flatc(\new b_1, c_1) \cup \{ \texttt{bool2int}(b_1,v) \})$ +% \end{tabbing} + +The procedure \safen($b, C$) enforces the relational semantics for unsafe +expressions, by ensuring that the unsafe relational versions of partial +functions are made safe. Note that to implement the \emph{strict semantics} as +opposed to the relational semantics we just need to define $\safen(b,C) = C$. If +$b \equiv \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 $\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 = \false$ since it is the conjunction of +the new variables $b'$. The \%HALF\% comments will be explained later. + +\begin{tabbing} +xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +\safen($b$,$C$) \\ +\> \textbf{if} ($b \equiv \true$) \textbf{return} $C$ \\ +\> \textbf{if} ($C$ is a set of safe constraints) \textbf{return} $C$ \\ +\> $B$ := $\emptyset$; $S$ := $\emptyset$ \\ +\> \textbf{foreach} $c \in C$ \\ +\> \> \textbf{if} ($c \equiv div(x,y,z)$ and $y$ can take value 0) \\ +\> \> \> $B$ := $B \cup \{ \new b' \}$ \\ +\> \> \> $S$ := $S \cup \{ \new y' \neq 0, b' \full y \neq 0, b' \full y += y', div(x,y',z) \}$ \\ +\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full y \neq 0, b' \half +div(x,y,z)\}$ \\ +\> \> \textbf{else if} $c \equiv \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', +\element(v',a,x)\}$ \\ +\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half +\element(v,a,x)\}$ \\ +\> \> \textbf{else} $S$ := $S \cup \{c\}$ \\ +\> \> \textbf{return} $S \cup \{b \full \wedge_{b' \in B} b' +\})$ +\end{tabbing} + +The flattening algorithms above can produce suboptimal results in special cases, +such as input with common subexpressions. Our implementation avoids generating +renamed-apart copies of already-generated constraints, but for simplicity of +presentation, we omit the algorithms we use to do this. + +\section{Half Reification} +\label{sec: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. + +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) & = & \{ \false \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\ +f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\ +f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \false \in D(b) \\ +f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c) +\text{~and~} \false \not\in D(b) +\end{array} +$$ + +% In reality most propagator implementations for $c$ can be thought of as +% a sequence of two propagators $f_c = f_{prop(c)} \cdot f_{check(c)}$ +% where +% $$ +% \begin{array}{rcll} +% f_{check(c)}(D)(v) & = & \emptyset & f_c(D) \text{~is a false domain} \\ +% f_{check(c)}(D)(v) & = & D(v) & \text{otherwise} \\ +% f_{prop(c)}(D)(v) & = & D & $D$ \text{~is a false domain} \\ +% f_{prop(c)}(D)(v) & = & f_c(D)(v) & \text{otherwise} \\ +% \end{array} +% $$ +% that is first we check whether constraint is satisfiable $check(c)$ +% and if so we propagate changes in variable domains $prop(c)$. + +% \begin{example} +% Most propagators check consistency before propagating: e.g. +% $\sum_i a_i x_i \leq a_0$ determines $L = \sum_i min_D(a_i x_i) - a_0$ +% and fails if $L > 0$ before propagating~\autocite{harveyschimpf}; +% Regin's domain propagator~\autocite{reginalldifferent} for \alldiff$([x_1, \ldots, x_n])$ +% determines a maximum matching between variables and values first, +% if this is not of size $n$ it fails before propagating; +% and the timetable \texttt{cumulative} constraint~\autocite{cumulative} +% determines a profile of +% necessary resource usage, and fails if this breaks the resource limit, +% before considering propagation. \qed +% \end{example} + +% Given this separation we can improve the definition of $f_{b \half c}$ above by +% replacing the check ``$f_c(D)$ is a false domain'' by ``$f_{check(c)}(D)$ is a +% false domain''. In practice it means that the half-reified propagator can be +% implemented to only perform the checking part until $D(b) = \{\true\}$, when it +% needs to perform both. + +In practice most propagator implementations for $c$ first check whether $c$ is +satisfiable, before continuing to propagate. For example, +$\sum_i a_i x_i \leq a_0$ determines $L = \sum_i min_D(a_i x_i) - a_0$ and fails +if $L > 0$ before propagating; Regin's domain propagator for +\alldiff$([x_1, \ldots, x_n]$) determines a maximum matching between variables +and values first, if this is not of size $n$ it fails before propagating; 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_{b \half c}$ by only +performing the checking part until $D(b) = \{\true\}$. + +Half reification naturally encodes the relational semantics for partial function +applications in positive contexts. We associate a Boolean variable $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:cons}. First we will convert + it to an equivalent expression with only positive contexts + + \begin{mzn} + i > 4 \/ a[i] * x >= 6 + \end{mzn} + + There are three Boolean terms: the entire constraint, $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 + + \begin{mzn} + constraint b1 -> i > 4; + constraint b2 -> element(i,a,t1); + constraint mult(t1,x,t2); + constraint b2 -> t2 >= 6; + constraint b1 \/ b2; + \end{mzn} + + The unsafe $\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 = \false$. Given this, the final constraint requires $b1 = \true$, which + in turn requires $i > 4$. Since this holds, the whole constraint is $\true$ + with no restrictions on $x$. +\end{example} + +Half reification can handle more constraint terms than full reification if we +assume that each global constraint predicate $p$ is available in half-reified +form. Recall that this places no new burden on the solver implementer. + +\begin{example} + Consider the constraint of \cref{ex:alldiff}. Half reification results in + + \begin{mzn} + constraint b1 -> i > 4; + constraint minus(i,x,t1); % t1 = i - x + constraint b2 -> all_different([i,t1,x]); + constraint b1 \/ b2 % b1 or b2 + \end{mzn} + + We can easily modify any existing propagator for \alldiff to support the + half-reified form, hence this model is executable by our constraint solver. +\end{example} + +Half reification can lead to more efficient constraint solving, since it does +not propagate unnecessarily. + +\begin{example}\label{ex:cumul} + Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\ + \autocite{schutt-2009-cumulative}) which includes constraints of the form + + \begin{mzn} + constraint sum(i in Tasks where i != j) + (bool2int(s[i] <= s[j] /\ s[i]+d[i] > s[j]) * r[i]) <= L-r[j]; + \end{mzn} + + which requires that at the start time $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: + + \begin{mzn} + constraint b1[i] <-> s[i] <= s[j]; + constraint plus(s[i],d[i],e[i]); % e[i] = s[i] + d[i] + constraint b2[i] <-> e[i] > s[j]; + constraint b3[i] <-> b1[i] /\ b2[i]; + constraint bool2int(b3[i], a[i]); % a[i] = bool2int(b3[i]) + constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j]; + \end{mzn} + + Whenever the start time of task $i$ is constrained so that it does not overlap + time $s[j]$, then $b3[i]$ is fixed to $\false$ and $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 + + \begin{mzn} + constraint b1[i] -> s[i] > s[j]; + constraint plus(s[i],d[i],e[i]); % e[i] = s[i] + d[i] + constraint b2[i] -> e[i] <= s[j]; + constraint b3[i] -> b1[i] \/ b2[i]; + constraint b4[i] <-> not b3[i]; + constraint bool2int(b4[i], a[i]); % a[i] = bool2int(b4[i]) + constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j]; + \end{mzn} + + which may seem to be more expensive since there are additional variables (the + $b4[i]$), but since both $b4[i]$ and $a[i]$ are implemented by + views~\autocite{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]$. +\end{example} + +\pjs{Add linearization example here!} + +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. We can reduce this disadvantage by fully +reifying Boolean connectives (which have low overhead) where possible in the +half reification. \pjs{Do we do this?} + +\subsection{Flattening with Half Reification} + +\newcommand{\halfc}{\textsf{halfc}} +\newcommand{\halft}{\textsf{halft}} +\newcommand{\halfnc}{\textsf{halfnc}} + +We describe flattening using half reification in a manner analogous to +flattening using full reification. We concentrate once more on flattening +constraint items, although we shall treat objectives differently than the simple +rewriting used with full reification. + + +The procedure $\halfc(b,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(\true, c)$. 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 +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. + +\newcommand{\bnds}{\mathit{bnds}} +\newcommand{\sign}{\textsf{sign}} +\newcommand{\iabove}{\textsf{ub}} +\newcommand{\ibelow}{\textsf{lb}} +\newcommand{\iboth}{\textsf{both}} +\newcommand{\negaterel}{\textsf{negaterel}} + +Halfreifying a constraint $c$ in context $\ctxt$, $\halfc(c,\ctxt)$, returns a +Boolean literal $b$ representing the constraint and as a side effect adds a set +of constraints (the flattening) $S$ to the store such that +$S \models b \half c$. The half reification function is only called with +$\ctxt = \rootc$ or $\ctxt = \pos$ if negative or mixed contexts arise we use +$\flatc$ instead. The procedure $\halfc$ is very similar to $\flatc$. The main +difference is that we use implication $(\half)$ to connect the Boolean literal +$b$ of a constraint to its component parts, and use half reified versions of the +primitive constraints. We also can simplify most translations. + +The treatment of common subexpressions is simpler. We use a separate hash table. +If the previous context was the $\rootc$, or the same we simply reuse the old +value. The remaining case is when the new context is $\rootc$ and the previous +was $\pos$. Then we force the variable to hold and update the hash table for +both half and full reification. When we store the result we construct for half +reification we also add an entry to the full reification hash table if the +context is $\rootc$, in case we meet the same term in a negative or mxed context +later. + +The translation of relational operators is similar to $\flatc$ except we use a +half reification specialized version of flattening terms $\halft$. This takes as +an extra argument the \emph{bounds} of the term we are interested in, these +could be: $\iabove$ we are only interested in the upper bound, $\ibelow$ we are +only interested in the lower bound, or $\iboth$ we are interested in both bounds +and interior values. For example for the constraint $b \half x \leq y$ we are +only interested in the lower bound of $x$ and the upper bound of $y$ since these +are the only bounds that can cause failure. + +Half reifying constaints of the form $\texttt{not}~c$ is handled by the +procedure $\halfnc$, which pushes the negation through operations where this is +safe to do so. We discuss it in detail later. Half reification of the Boolean +connectives is very similar to full reification, it treats $c_1 ~\verb+->+~ c_2$ +and $\texttt{not}~c_1 \vee c_2$ and full reification for $c_1 ~\verb+<->+~ c_2$. +\texttt{forall} and \texttt{exists} are treated analogously to \verb+/\+ and +\verb+\/+. + +Array lookup had to flatten the index term in a manner that is interested in +everything about its value ($\iboth)$. The translation use a half reified +\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 +created using the propagator for $p$, this is a fair assumption. + +User defined predicates, if-then-else-endif and let are treated analogously to +full reification. + +\begin{tabbing} +xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +\halfc($c$,$\ctxt$) \\ +\> $\tuple{h,prev}$ := hhash[$c$]; \\ +\> \textbf{if} ($h \neq \bot$) \\ +\>\> \textbf{if} ($prev =\rootc \vee prev = \ctxt$) \textbf{return} $h$ \\ +\>\> $S$ \cupp $\{ h \}$; hhash[$c$] := +$\tuple{h,\rootc}$; hash[$c$] := +$\tuple{h,\rootc}$; \textbf{return} $h$ +\\ +\> \textbf{if} ($\fixed(c)$) $b$ := $\eval(c)$ \\ +\> \textbf{else} \\ +\> \> \textbf{switch} $c$ \\ +%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ +%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ +\> \> \textbf{case} $b'$ (\bvar): $b$ := $b'$; \\ +\> \> \textbf{case} $t_1$ $r$ $t_2$ (\relop): \\ +\> \> \> \textbf{switch} $r$ \\ +\> \> \> \textbf{case} $\leq$, $<$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\iabove)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\ibelow)$; \\ +\> \> \> \textbf{case} $\geq$, $>$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\ibelow)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\iabove)$; \\ +\> \> \> \textbf{case} $=$, $\neq$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\iboth)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\iboth)$; \\ +\> \> \> \textbf{endswitch} \\ +\> \> \> $S$ \cupp $\{ \new b \half (b_1 \wedge b_2 \wedge \new b'), + b' \half v_1 ~r~ v_2\}$ \\ +\> \> \textbf{case} \texttt{not} $c_1$: +$b$ := $\halfnc(c_1, \ctxt)$ \\ +\> \> \textbf{case} $c_1$ \verb+/\+ $c_2$: $S$ \cupp $\{ \new b \half (\halfc(c_1, \ctxt) \wedge \halfc(c_2, \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+\/+ $c_2$: +$S$ \cupp $\{ \new b \half (\halfc(c_1,\posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+->+ $c_2$: +$S$ \cupp $\{ \new b \half (\halfnc(c_1, \posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+<->+ $c_2$: +$S$ \cupp $\{ \new b \half (\flatc(c_1,\mix) \full +\flatc(c_2,\mix))\}$ +\\ +\> \> \textbf{case} \texttt{forall(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfc(c_j, \ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \half \bigwedge_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} \texttt{exists(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfc(c_j, \posop\ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \half \bigvee_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} $[c_1, \ldots, c_n]$ \texttt{[} $t$ \texttt{]}: \\ +\>\>\> +\textbf{foreach}($j \in 1..n$) $b_j$ := $\halfc(c_j, \posop \ctxt)$; \\ +\>\>\> $\tuple{v, b_{n+1}}$ := $\halft(t, \ctxt, \iboth)$; \\ +%\>\>\> $S$ \cupp +%$\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), +%\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), +%b'' \full v \in \{1,..,n\} \} $ \\ +\>\>\> \textbf{if} ($\ctxt = \rootc$) +$S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \true), \new b\}$ \\ +\>\>\> \textbf{else} +$S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half +\texttt{element}(v, [b_1, \ldots, b_n], b') \}$ \\ +%\>\>\> \textbf{else} \\ +%\>\>\>\> $S$ \cupp $\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, +%\ldots, n\},$ \\ +%\>\>\>\>\>\>\> $\texttt{element}(v', [b_1, \ldots, b_n], b'), +%b'' \full v = v', b'' \full v \in \{1,..,n\} \} $ +%\\ +\callbyvalue{ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := +$\halft(t_j,\ctxt,\iboth)$; \\ +\> \> \> \textbf{if} ($\ctxt = \rootc$) +$b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j +\}$ +\\ +\>\>\> \textbf{else} %($\ctxt = \pos$) \\ \> \> \> \> +$S$ \cupp $\{ p\_half(v_1,\ldots,v_n,\new b'), +\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}$ \\ +%\> \>\> \textbf{else} \\ +%\> \> \> \> \textbf{if} ($p\_reif$ does not exist) \textbf{abort} \\ +%\> \> \> \> \textbf{else} $S$ \cupp $\{ p\_reif(v_1,\ldots,v_n,\new b'), +%\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}$ \\ +%\\ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): user-defined predicate \\ +\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := +$\halft(t_j,\ctxt, \iboth)$; \\ +\>\> \> $\new b'$ := $\halfc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)$ +\\ +\> \>\> $S$ \cupp $\{ \new b \half b' \wedge \bigwedge_{j=1}^n +b_j\}$ +\\ +} +\callbyunroll{ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\ +\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ +\>\> \> $b$ := $\true$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ +\\ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): 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}: +% \\ \> \> \> +\textbf{if} ($\eval(c_0)$) $b$ := $\halfc(c_1,\ctxt)$ \textbf{else} $b$ := $\halfc(c_2,\ctxt)$ \\ +\>\> \textbf{case} \texttt{let \{} $d$ \texttt{\} in} $c_1$: \\ +\>\> \> \textbf{let} $\bar{v}'$ be a renaming of variables $\bar{v}$ defined +in $d$ \\ +\> \> \> $\tuple{c',\_}$ := $\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, +c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)$ \\ +\> \> \> $b$ := $\halfc(c',\ctxt)$; +\\ +\> \> \textbf{endswitch} \\ +\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{ b \}$; \\ +\> hhash[$c$] := $\tuple{b,\ctxt}$; \textbf{if} ($\ctxt = +\rootc$) hash[$c$] := $\tuple{b,\ctxt}$; \\ +\> \textbf{return} $b$ +\end{tabbing} + +Since half reification has advantages rather than give up on using it when we +encounter a negation we instead try to effectively transform the term under the +negation as much as possible by pushing negations down. The procedure +$\halfnc(c,\ctxt)$, returns a Boolean literal $b$ representing the constraint +and as a side effect adds a set of constraints (the flattening) $S$ to the store +such that $S \models b \half \neg c$. The $\ctxt$ argument stores the context +for the term $\neg c$ and again is only ever $\rootc$ or $\pos$. + +The procedure $\halfnc$ use the same hash table but stores and looks up on the +key $\texttt{not}~c$. When negating a basic relation we first check that the +subterms are safe, that is cannot involve partial functions, if this is the case +we can negate the relational operation and continue using half reification on +the terms. If not we use full reification. + +A term of the form $\texttt{not}~c$ simply half riefies $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 +defined predicates use full reification on the terms (since they occur in a +negative or mixed context) and negated half reification on the body. +If-then-else-endif and let are handled straightforwardly although note that the +context passed to $\textsf{flatlet}$ is either $\negc$ or $\mix$. + +\begin{tabbing} +xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill +\halfnc($c$,$\ctxt$) \\ +\> $\tuple{h,prev}$ := hhash[$\texttt{not}~c$];\\ +\> \textbf{if} ($h \neq \bot$) \\ +\>\> \textbf{if} ($prev =\rootc \vee prev = \ctxt$) \textbf{return} $h$ \\ +\>\> $S$ \cupp $\{ h \}$; hhash[$\texttt{not}~c$] := +$\tuple{h,\rootc}$; hash[$\texttt{not}~c$] := +$\tuple{h,\rootc}$; \textbf{return} $h$\\ +\> \textbf{if} ($\fixed(c)$) $b$ := $\neg \eval(c)$ \\ +\> \textbf{else} \\ +\> \> \textbf{switch} $c$ \\ +%\> \> \textbf{case} \texttt{true}: $b$ := $\true$;\\ +%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\ +\> \> \textbf{case} $b'$ (\bvar): $S$ \cupp $\{\new b \half \neg b'\}$; \\ +\> \> \textbf{case} $t_1$ $r$ $t_2$ (\relop): \\ +\> \> \> \textbf{if} ($t_1$ and $t_2$ are safe) \\ +\> \> \> \> $r'$ := $\negaterel(r)$ \\ +\> \> \> \> \textbf{switch} $r'$ \\ +\> \> \> \> \textbf{case} $\leq$, $<$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\iabove)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\ibelow)$; \\ +\> \> \> \> \textbf{case} $\geq$, $>$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\ibelow)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\iabove)$; \\ +\> \> \> \> \textbf{case} $=$, $\neq$: $\tuple{v_1, b_1}$ := $\halft(t_1,\ctxt,\iboth)$; +$\tuple{v_2, b_2}$ := $\halft(t_2,\ctxt,\iboth)$; \\ +\> \> \> \> \textbf{endswitch} \\ +\> \> \> \> $S$ \cupp $\{ \new b \half (b_1 \wedge b_2 \wedge \new b'), + b' \half v_1 r' v_2\}$ \\ +\> \> \> \textbf{else} \\ +\> \> \> \> $\new b$ := $\flatc(\texttt{not} (t_1~r~t_2), \negop \ctxt)$ \\ +\> \> \textbf{case} \texttt{not} $c_1$: +$b$ := $\halfc(c_1, \ctxt)$ \\ +\> \> \textbf{case} $c_1$ \verb+/\+ $c_2$: $S$ \cupp $\{ \new b \half (\halfnc(c_1, \posop\ctxt) \vee \halfnc(c_2, \posop\ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+\/+ $c_2$: +$S$ \cupp $\{ \new b \half (\halfnc(c_1, \ctxt) \wedge \halfnc(c_2, \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+->+ $c_2$: +$S$ \cupp $\{ \new b \half (\halfc(c_1, \posop\ctxt) \vee \halfnc(c_2,\posop \ctxt))\}$ +\\ +\>\> \textbf{case} $c_1$ \verb+<->+ $c_2$: +$b$ := $\flatc(\texttt{not}~ c_1~ \verb+<->+ ~c_2, \ctxt)$ +\\ +\> \> \textbf{case} \texttt{forall(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfnc(c_j, \posop \ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \half \bigvee_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} \texttt{exists(} $ba$ \texttt{)}: \\ +\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfnc(c_j, \ctxt)$; \\ +\>\>\> $S$ \cupp $\{ \new b \half \bigwedge_{j=1}^n b_j \}$ \\ +\>\> \textbf{case} $[c_1, \ldots, c_n]$ \texttt{[} $t$ \texttt{]}: \\ +\>\>\> $b$ := $\flatc(\texttt{not}~[c_1, \ldots, c_n]~\texttt{[} ~t~ +\texttt{]}, \ctxt)$ \\ +\callbyvalue{ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\ +\> \> \> $b$ := $\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)$ \\ +\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): user-defined predicate \\ +\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := +$\flatt(t_j,\negop \ctxt)$; \\ +\>\> \> $\new b'$ := $\halfnc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)$ +\\ +\> \>\> $S$ \cupp $\{ \new b \half b' \wedge \bigwedge_{j=1}^n +b_j\}$ +\\ +} +\> \> \textbf{case} \texttt{if} $c_0$ \texttt{then} $c_1$ \texttt{else} +$c_2$ \texttt{endif}: +% \\ \> \> \> +\textbf{if} ($\eval(c_0)$) $b$ := $\halfnc(c_1,\ctxt)$ \textbf{else} $b$ := $\halfnc(c_2,\ctxt)$ \\ +\>\> \textbf{case} \texttt{let \{} $d$ \texttt{\} in} $c_1$: \\ +\>\> \> \textbf{let} $\bar{v}'$ be a renaming of variables $\bar{v}$ defined +in $d$ \\ +\> \> \> $\tuple{c',\_}$ := $\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'}, +c_1\subs{\bar{v}/\bar{v}'},0,\negop \ctxt)$ \\ +\> \> \> $b$ := $\halfnc(c',\ctxt)$; +\\ +\> \> \textbf{endswitch} \\ +\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{ b \}$; \\ +\> hhash[$\texttt{not}~c$] := $\tuple{b,\ctxt}$; \textbf{if} +($\ctxt = \rootc$) hash[$\texttt{not}~c$] := $\tuple{b,\ctxt}$ \\ +\> \textbf{return} $b$ +\end{tabbing} + +\subsection{Flattening Integer Expressions with Half Reification} + +We use a specialized procedure to flatten terms for half reification. The +procedure $\halft(t, \ctxt, \bnds)$ flattens term $t$ in context $\ctxt$ (which +again can only be $\rootc$ or $\pos$) when we are interested in $\bnds$ of term +$t$. It returns a pair $\tuple{v,b}$ and adds constraints to $S$ that enforce +that $b \half v = t$. The third argument is there to create accurate context +information when we meet terms of the form $\texttt{bool2int(} $c$ \texttt{)}$. +It acts independently of the context. + +We flatten objective functions $e$ using this procedure also. The item +\texttt{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 +$\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 $\true$ in $S$, and then reuse the result if the +bounds are the same, or set $\bnds$ to $\iboth$ and reflatten. We store the +result found at the end of flattening, note that we only need one entry: context +can move from $\pos$ to $\rootc$ and bounds can move from one of $\iabove$ or +$\ibelow$ to $\iboth$. + + +The case of arithmetic operators is interesting since we need to propagate the +interest in bounds. Addition leaves us interested in the same bounds of both +subterms, subtraction reverses the bound we are interested in for the second +argument. Multiplication is the most complex case. If one argument has a known +sign we can accurately determine the bounds of interest in the other argument, +otherwise we lose all information ($\iboth$). We assume $\sign(t)$ returns one +of the context operators $\posop$ if $\forall d \in poss(t). d \geq 0$ and +$\negop$ if $\forall d \in poss(t). d \leq 0$, and returns $\pm$ otherwise. We +extend the context operators to work on bounds information as follows: + +\centerline{ +\begin{tabular}{ccc} +$ +\begin{array}{lcl} +\posop \iabove & = &\iabove \\ +\posop \ibelow & =& \ibelow \\ +\posop \iboth & =& \iboth, \\ +\end{array} +$ +& ~~~ & +$ +\begin{array}{lcl} +\negop \iabove & = &\ibelow \\ +\negop \ibelow & =& \iabove \\ +\negop \iboth & =& \iboth, \\ +\end{array} +$ +\end{tabular} +} + +For simplicity division simply loses all information. The half reification is +simpler for the partial function \texttt{div} requiring only the half reified +constraint. + +Array lookup is again simpler in half reification where we use half reified +\texttt{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$. + + +\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} ($prev =\rootc \vee prev = \ctxt$) \\ +\>\> \> \textbf{if} ($pbnds = \bnds$) \textbf{return} $\tuple{h,b'}$ \\ +\>\> \> \textbf{else} $\bnds$ := $\iboth$ \\ +\>\> \textbf{else} \\ +\> \> \> $S$ \cupp $\{ b' \}$ \\ +\> \> \> \textbf{if} ($pbnds = \bnds$) hhash[$t$] := $\tuple{h,b',\rootc,\bnds}$; \textbf{return} $\tuple{h,b'}$ +\\ +\> \> \> \textbf{else} $\bnds$ := $\iboth$ \\ +\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\true$ \\ +\> \textbf{else} %\\ +%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ +%\> \> +\textbf{switch} $t$ \\ +%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\ +\> \> \textbf{case} $v'$ (\ivar): $v$ := $v'$; $b$ := $\true$\\ +\> \> \textbf{case} $t_1$ $a$ $t_2$ (\aop): \\ +\> \> \> \textbf{switch} $a$ \\ +\> \> \> \textbf{case} $+$: +$\tuple{v_1,b_1}$ := $\halft(t_1,\ctxt,\bnds)$; +$\tuple{v_2,b_2}$ := $\halft(t_2,\ctxt,\bnds)$; \\ +\> \> \> \textbf{case} $-$: +$\tuple{v_1,b_1}$ := $\halft(t_1,\ctxt,\bnds)$; +$\tuple{v_2,b_2}$ := $\halft(t_2,\ctxt,\negop \bnds)$; \\ +\> \> \> \textbf{case} $\times$: \\ +\> \> \> \> \textbf{if} ($\sign(t_2) \in \{\posop,\negop\}$) +$\tuple{v_1,b_1}$ := $\halft(t_1,\ctxt,\sign(t_2)~ \bnds)$; \\ +\> \> \> \> \textbf{else} +$\tuple{v_1,b_1}$ := $\halft(t_1,\ctxt,\iboth)$; \\ +\> \> \> \> \textbf{if} ($\sign(t_1) \in \{\posop,\negop\}$) +$\tuple{v_2,b_2}$ := $\halft(t_2,\ctxt,\sign(t_1)~ \bnds)$; \\ +\> \> \> \> \textbf{else} +$\tuple{v_2,b_2}$ := $\halft(t_2,\ctxt,\iboth)$; \\ +\> \> \> \textbf{case} $\texttt{div}$: +$\tuple{v_1,b_1}$ := $\halft(t_1,\ctxt,\iboth)$; +$\tuple{v_2,b_2}$ := $\halft(t_2,\ctxt,\iboth)$; \\ +\> \> \> \textbf{endswitch} \\ +\> \> \> \textbf{if} ($a \not\equiv \texttt{div} \vee \ctxt = \rootc$) +$S$ \cupp $\{ \new b \half (b_1 \wedge b_2), a(v_1,v_2,\new v) \}$ \\ +%\> \> \> \textbf{else} $S$ \cupp $\{ \new b \full (b_1 \wedge b_2 \wedge +%\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}$ \\ +\> \> \> \textbf{else} +$S$ \cupp $\{ \new b \half (b_1 \wedge b_2 \wedge +\new b'), b' \half \texttt{div}(v_1,v_2,\new v), \}$ \\ +\> \> \textbf{case} $[t_1, \ldots, t_n]$ \texttt{[} $t_{0}$ \texttt{]}: \\ +\> \> \> +\textbf{foreach}($j \in 0..n$) $\tuple{v_j, b_j}$ := $\halft(t_j,\ctxt,\iboth)$; \\ +%\>\> \> $S$ := +%$\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), +%\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n], \new v), +%b' \full v_0 \in \{1,...,n\} \}$ +%\\ +\>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\new b, \texttt{element}(v', [v_1, \ldots, v_n], +\new v) \}$ \\ +\>\>\> \textbf{else} \\ +\>\>\>\> $S$ \cupp +$\{ \new b \half (\new b' \wedge \bigwedge_{j=0}^n b_j), +b' \half \texttt{element}(v_0, [v_1, \ldots, v_n], \new v), \} $ +\\ +\> \> \textbf{case} \texttt{sum(} $\mathit{ia}$ \texttt{)}: \\ +\> \> \> \textbf{let} $[t_1, \ldots, t_n] = \evalb(ia)$; \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := +$\halft(t_j,\ctxt,\bnds)$; \\ +\>\>\> $S$ \cupp $\{ \new b \half \bigwedge_{j=1}^n b_j, + \new v = \sum_{j=1}^n v_j \}$ \\ +%\> \> \> +%$\tuple{v,b}$ := \flatt( +%\textsf{foldl}($\evalb(ia)$, \texttt{0}, \texttt{+}), $\ctxt$) +%\\ +\> \> \textbf{case} \texttt{if} $c_0$ \texttt{then} $t_1$ \texttt{else} +$t_2$ \texttt{endif}: +\\ \> \> \> +\textbf{if} ($eval(c_0)$) $\tuple{v,b}$ := $\halft(t_1,\ctxt,\bnds)$ \textbf{else} +$\tuple{v,b}$ := $\halft(t_2,\ctxt,\bnds)$ +\\ +\>\> \textbf{case} \texttt{bool2int(} $c_0$ \texttt{)}: \\ +\> \> \> \textbf{if} $(\bnds = \ibelow$) $b_0$ := $\halfc(c_0, \pos)$; \\ +\> \> \> \textbf{elseif} $(\bnds = \iabove$) $b'_0$ := $\halfnc(c_0, +\pos)$; $S$ \cupp $\{\new b_0 \full \neg b'_0\}$ \\ +\> \> \> \textbf{else} $b_0$ := $\flatc(c_0, \mix)$; \\ +\> \> \> $S$ \cupp $\{ \texttt{bool2int}(b_0, \new v), \new b \}$ \\ +\callbyvalue{ +\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): function \\ +\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := $\halft(t_j,\ctxt,\iboth)$; \\ +\>\> \> \textbf{let} $f(x_1, \ldots, x_n) = t_0$ be defn of $f$ \\ +\> \> \> \textbf{if} ($f$ is declared total) $\ctxt' = \rootc$ \textbf{else} +$\ctxt' = \ctxt$ \\ +\>\> \> $\tuple{v,b'}$ := $\halft(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt',\bnds)$ \\ +\> \> \> $S$ \cupp $\{ \new b \half b' \wedge \bigwedge_{j=1}^n b_j \}$ +\\ +} +\>\> \textbf{case} \texttt{let \{} $d$ \texttt{\} in} $t_1$: \\ +\>\> \> \textbf{let} $\bar{v}'$ be a renaming of variables $\bar{v}$ defined +in $d$ \\ +\> \> \> $\tuple{c',t'}$ := $\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true}, +t_1\subs{\bar{v}/\bar{v}'},\ctxt)$ \\ +\>\> \> $\tuple{v,b_1}$ := $\halft(t',\ctxt,\bnds)$; +$b_2$ := $\halfc(c',\ctxt)$; +$S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$ +\\ +\> \> \textbf{endswitch} \\ +\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{ b \}$; \\ +\> hhash[$t$] := $\tuple{v,b,\ctxt, \bnds}$ \\ +\> \textbf{return} $\tuple{v,b}$ +\end{tabbing} + + +% Half reification of terms returns a set of constraints that enforce $v = t$ if +% the term $t$ is safe, and $b \half v = t$ otherwise. The most complex case is +% \texttt{bool2int}$(c_1)$, which half-reifies $c_1$ if it is in a positive +% context, negates $c_1$ and half-reifies the result if $c_1$ is safe and in a +% negative context, and uses full flattening otherwise. + +\begin{example}\label{ex:half} + Now lets consider half reifying the expression of \cref{ex:flat}. + + The result of flattening with half reification is: + + \begin{mzn} + constraint b0 -> b1 \/ b2; + constraint b0; + constraint b1 -> b2 /\ b1'; + constraint b1' -> v3 >= 4; + constraint b2 -> b4 /\ b5; + constraint b4 -> b8 /\ b9; + constraint b3 -> b6 /\ b7; + constraint minus(v6, v7, v3); + constraint b4 -> b8 /\ b9; + constraint b5 -> (b10 \/ b); + constraint b6 -> b11 /\ b12; + constraint plus(v11, v12, v6); + constraint b7; + constraint bool2int(b13, v7); + constraint b13 <-> not b10; + constraint b8 -> b11 /\ b8'; + constraint b8' -> v11 <= 2; + constraint b9 -> x > y; + constraint b10 -> x <= z; + constraint b11 -> b11'; + constraint b11' -> element(x, a, v11); + constraint b12; + constraint bool2int(b9, v12); + \end{mzn} + + Note that again we use CSE to reuse variables from position 11 for position + 14, position 9 for position 15, and position 10 for position 13. + + Half reification is significantly different from full reification in the + treatment of the partial function array access, as well as the treatment of + the negated context at 10 and 13. The bounds analysis finds the positions 1, + 3, 6, 11 are only interested in upper bounds, while positions 7 and 14 are + only interested in lower bounds. This means that the positions 13 and 15 are + reified using \halfnc{} and \halfc{} respectively even though they occur under + a $bool2int$. \pjs{explain more!} + + We can simplify the resulting formulae by removing always true literals and + replacing literals $b'$, which only occur in chains $b'' \half b'$, + $b' \half e_1$, $b' \half e_2$ etc, by $b''$ resulting in + + \begin{mzn} + constraint b1 \/ b2; + constraint b1 -> v3 >= 4; + constraint minus(v6, v7, v3); + constraint b2 -> b9; + constraint b2 -> (b10 \/ b); + constraint b1 -> b11; + constraint plus(v11, v12, v6); + constraint bool2int(b13, v7); + constraint b13 <-> not b10; + constraint b2 -> b11 /\ b8'; + constraint b8' -> v11 <= 2; + constraint b9 -> x > y; + constraint b10 -> x <= z; + constraint b11 -> element(x, a, v11); + constraint bool2int(b9, v12); + \end{mzn} + + with 15 primitive constraints and 12 intermediate variables. This reduces the + number of constraints by 3 and the number of intermediate variables by 2. +\end{example} + +\pjs{Extend and add section in implementation} As presented the half reification +transformation will construct many implications of the form $b \half b'$, note +that the constraint $b \half b_1 \wedge \cdots \wedge b_n$ is equivalent to +$b \half b_1, b \half b_2, \ldots, b \half b_n$. Just as in +Example~\ref{ex: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. + +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 ( \{ \false \} \cup f_{b \full c}(D)(b)) \\ +f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~ v \in vars(c),~\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}~ \{ \false \} \in f_{b \full c}(D)(b) \\ +f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \false\} & \text{otherwise}\\ +f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~ v \in vars(c),~\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 \{ \false, \true\}$. That is if the propagator ever +reduces the domain of some variable, then it must also fix the Boolean variable +$b$. This is sensible since if $b$ is not fixed then every possible value of $v$ +is consistent with constraint $b \full c$ regardless of the domain $D$. This is +a very weak assumption, every implementation of reified constraints we are aware +of satisfies this property, and indeed only a deliberately inaccurate propagator +would not. + +For the sake of simplicity of proving the following theorem we also assume +$f_{b \full c}$ is an \emph{idempotent} propagator, that is forall +$D \sqsubseteq D_{init}$: $f_{b \full c}(D) = f_{b \full c}(f_{b \full c}(D))$. +We assume the propagator $f_{b' \full \neg b}$ is domain consistent, which is +the usual case for such a trivial propagator. + +% Define +% $f_{b \half c}(D) =_{vars(b \full c)} \solv(\{f_{b'' \full c}, f_{b \half b''} \}, D)$, +% that is the half-reified version propagates on all variables only in the +% forward direction of the implication, by introducing the hidden variable +% $b''$ which prevents propagation in the other direction. We assume a domain +% consistent propagator for $b \half b''$. Similarly define +% $f_{b' \half \neg c}(D) =_{vars(b' \full c)} \solv(\{f_{b''' \full c}, f_{b' \half \neg b'''} \}, D)$ + +\begin{theorem} + $\forall D. \solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D) = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$. +\end{theorem} +\begin{proof} + Let $V = vars(c)$. First w.l.o.g. we only consider domains $D$ at a fixpoint + of the propagators $f_{b' \full \neg b}$, i.e. + $D(b') = \{ \neg d ~|~ d \in D(b)\}$, since both $\solv$ expressions include + $f_{b' \full \neg b}$. Let + $D' = \solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D)$, now since + $f_{b \full c}$ and $f_{b' \full \neg b}$ are idempotent and $D$ is a fixpoint + of $f_{b' \full \neg b}$, then $D' = f_{b' \full \neg b}(f_{b \full c}(D))$. + Let + $D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$. + The proof is by cases of $D$. + + \textbf{(a)} Suppose $D(b) = \{\true,\false\}$. \textbf{(a-i)} Suppose + $f_{b \full c}(D) = D$. Then clearly $f_{b \half c}(D) = D$ by definition, and + similarly $f_{b' \half \neg c}(D) = D$. Hence $D_1 = D_2 = D$. Note that since + $f_{b \full c}$ is reified consistent, then $f_{b \full c}(D) \neq D$ implies + that $f_{b \full c}(D)(b) \neq \{ \false, \true \}$. \textbf{(a-ii)} Suppose + $f_{b \full c}(D)(b) = \{ \true \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then + $D_1(b') = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$. + Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \true \}$ and + $D_2(v) = D(v), v \not\in \{b,b'\}$. Then + $D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)$ by definition, and by + idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and + $b'$ this is a fixpoint of $f_{b \full c}$ and + $D_3(v) = f_{b \full c}(D)(v), v \not \equiv b'$. $D_3$ is also a fixpoint of + $f_{b \half c}$, $f_{b' \full \neg b}$ and $f_{b' \half \neg c}$ and hence + $D'' = D_3$. But also $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since + $D_3$ and $f_{b \full c}(D)$ only differ on $b'$. \textbf{(a-iii)} Suppose + $f_{b \full c}(D)(b) = \{ \false \}$. Let $D_1 = f_{b \half c}(D)$, then + $D_1(b) = \{ \false \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let + $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \true \}$ and + $D_2(v) = D(v), v \not\in \{b,b'\}$. Then + $D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)$ by definition, and by + idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and + $b'$ this is a fixpoint for $f_{b \half c}$, $f_{b' \full \neg b}$ and + $f_{b' \half \neg c}$ and hence $D'' = D_3$. But also + $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since $D_3$ and + $f_{b \full c}(D)$ only differ on $b'$. + + \textbf{(b)} If $D(b) = \{\true\}$ then clearly $f_{b \full c}$ and + $f_{b \half c}$ act identically on variables in $vars(c)$. + + \textbf{(c)} If $D(b) = \{\false\}$ then $D(b') = \{\true\}$ and clearly + $f_{b \full c}$ and $f_{b' \half \neg c}$ act identically on variables in + $vars(c)$. \qed +\end{proof} + +The reason for the generality of the above theorem which defines the +half-reified propagation strength in terms of the full reified propagator is +that we can now show that for the usual notions of consistency, replacing a +fully reified propagator leads to the same propagation. + +Note that the additional variable $b'$ can be implemented as a view +\autocite{schulte-2005-views} in the solver and hence adds no overhead. + +\begin{corollary} + A domain (resp. bounds(Z), bounds(R)) consistent propagator for $b \full c$ + propagates identically to domain (resp. bounds(Z), bounds(R)) consistent + propagators for $b \half c$, $b \full \neg b'$, $b' \half \neg c$. \qed +\end{corollary} + + +\section{Propagation and Half Reification} + +\pjs{What happens to this section?} A propagation engine gains certain +advantages from half-reification, but also may suffer certain penalties. Half +reification can cause propagators to wake up less frequently, since variables +that are fixed to true by full reification will never be fixed by half +reification. This is advantageous, but a corresponding disadvantage is that +variables that are fixed can allow the simplification of the propagator, and +hence make its propagation faster. + +When full reification is applicable (where we are not using half reified +predicates) an alternative to half reification is to implement full reification +$b \full c$ by two half reified propagators +$b \half c, b' \half \neg c, b' \full \neg b$. This does not lose propagation +strength. For Booleans appearing in a positive context we can make the the +propagator $b' \half \neg c$ run at the lowest priority, since it will never +cause failure. Similarly in negative contexts we can make the propagator +$b \half c$ run at the lowest priority. This means that Boolean variables are +still fixed at the same time, but there is less overhead. + + +\section{Implementation in the \minizinc{} Distribution} + +Implementing half-reification within the \minizinc\ distribution consists of two +parts: the \minizinc\ compiler needs to be extended with an implementation of +the half-reification flattening algorithm as described in \cref{sec:halfreif} +and for any target solver that supports half-reification its library needs to be +appended with definitions for the predicates that are half-reified. Because the +\minizinc\ language allows for the definition of new predicates, we allow any +predicate to have an implemented half-reification, not just the predicates +defined as \flatzinc\ builtins. + +The implementation of half-reification in \minizinc\ requires little change to +the translator. As the translator was already aware of the context of +expressions, we can track the context of each expression using annotations to +the expressions, which are native to the \minizinc\ language. Through the use of +common subexpression elimination, we use the same generated \flatzinc\ for the +same expression and are able to update the context annotation if it should be +required. In the translator, reifications are delayed until the full model is +flattened because further processing might reveal that a constraint might not +need to be reified. Because of this delay, we know that if a reification still +has a positive context annotation, then we can use a half-reified version of +that constraint if it is available without having both a fully reified version +and a half-reified version of the same constraint. Note that this might not be +true if the flattening of the reifications requires the addition of a full +reification of which a half-reified version was already used. Because this +situation is so uncommon, no solution for this situation is implemented. Our +implementation currently does not implement the transformations shown in +\halfnc\, which push down negations to avoid negative context. Although this +would likely improve number of possible half-reifications, we believe that the +positive effects of half-reifications will already be noticeable without this +optimisation. + +Our implementation currently targets various linear solvers, including Gurobi +\autocite{gurobi-2021-gurobi} and Cbc (Coin-or branch and cut) +\autocite{lougee-heimer-2003-coin}, and Gecode \autocite{gecode-2021-gecode}. +Adding support for half-reification to the solver's \minizinc\ library can be +done in multiple ways: half-reified predicates can be be declared as solver +builtins, a redefinition using the \minizinc\ language can be provided for the +half-reified constraint, or a combination of the two can be used. Because Gecode +has propagators for half-reified constraints we have declared the corresponding +predicates as solver builtins. Gecode provides half-reified propagators for +almost all \flatzinc\ builtins. The other targeted solvers use the linear +library. The linear library \jip{,as seen before + reference ???,} already has +redefinition for their fully reified predicates, \(b \full c\). These generally +consist of two parts which are equivalent to the implications +\(b \half c \land \lnot b \half \lnot c \). Because of this, the implementations +of the half-reified version of the same predicates usually consist of using only +one of these two parts, which will eliminate the need of many constraints. We +added half-reified versions for all predicates for which a full reification was +provided. + +\subsection{Implication Chain Compression} + +As shown in Example \ref{ex:half}, flattening with half reification will in many +cases result in implication chains: \((b \half b') \land (b' \half c)\), where +\(b'\) has no other occurrences. In this case the conjunction can be replaced by +\(b \half c\) and \(b'\) can be removed from the model. The case shown in the +example can be generalized to +\((b \half b') \land \left(\forall_{i \in N} b' \half c_i \right)\), which, if +\(b'\) has no other usage in the instance, can be resolved to +\(\forall_{i \in N} b \half c_i\) after which \(b'\) can be removed from the +model. + +An algorithm to remove these chains of implications is best visualised through +the use of an implication graph. An implication graph \(\tuple{V,E}\) is a +directed graph where the vertices \(V\) represent the variables in the instance +and an edge \(\tuple{x,y} \in E\) represents the presence of an implication +\(x \half y\) in the instance. Additionally, for the benefit of the algorithm, a +vertex is marked when it is used in other constraints in the constraint model. +The goal of the algorithm is now to identify and remove vertices that are not +marked and have only one incoming edge. The following pseudo code provides a +formal specification for this algorithm. + +\newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~} +\begin{tabbing} + xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill + \textsf{compress}($V$, $E$) \\ + \> \textbf{foreach} ($x \in V$) \\ + \> \> \textbf{if} $|\{\tuple{a,x}| \tuple{a,x} \in E\}| = 1$ $\land$ $\lnot$ marked($x$) \\ + \> \> \> \textbf{foreach} ($\tuple{x, b} \in E$) \\ + \> \> \> \> $E$ \cupp $\{ \tuple{a,b} \}$ \\ + \> \> \> \> $E$ \setminusp $\{ \tuple{x,b} \}$ \\ + \> \> \> $E$ \setminusp $\{\tuple{a,x}\}$ \\ + \> \> \> $V$ \setminusp $\{x\}$ \\ +\end{tabbing} + +\jip{Here we could actually show an example using a drawn graph} + +The algorithm can be further improved by considering implied conjunctions. These +can be split up into multiple implications: \(b' \half \forall_{i \in N} b_i\) +is equivalent to \(\forall_{i \in N} (b' \half b_i)\). This transformation both +simplifies a complicated constraint and possibly allows for the further +compression of implication chains. It should however be noted that although this +transformation can result in an increase in the number of constraints, it +generally increases the propagation efficiency. + +To adjust the algorithm to simplify implied conjunctions more introspection from +the \minizinc\ compiler is required. The compiler must be able to tell if a +variable is (only) a control variable of a reified conjunction and what the +elements of that conjunction are. In the case where a variable has one incoming +edge, but it is marked as used in other constraint, we can now check if it is +only a control variable for a reified conjuction and perform the transformation +in this case. + +\section{Experiments} + +We ran our experiments on a server cluster using an Intel Xeon 8260. Each run +had exclusive access to 1 core of the CPU and 4 GB of RAM. The experiments are +available \jip{Insert new link} has our experimental \minizinc\ instances and +the infrastructure that performs the benchmarks. + +The first experiment considers ``QCP-max'' problems which are defined as +quasi-group completion problems where the \alldiff constraints are soft, and the +aim is to satisfy as many of them as possible. + +\begin{mzn} +int: n; % size +array[1..n,1..n] of 0..n: s; % 0 = unfixed 1..n = fixed + +array[1..n,1..n] of var 1..n: q; % qcp array; + +constraint forall(i,j in 1..n where s[i,j] > 0)(q[i,j] = s[i,j]); + +solve maximize + sum(i in 1..n)(bool2int(all_different([q[i,j] | j in 1..n]))) + + sum(j in 1..n)(bool2int(all_different([q[i,j] | i in 1..n]))); + +predicate all_different(array[int] of var int: x) = + forall(i,j in index_set(x) where i < j)(x[i] != x[j]); +\end{mzn} + +Note that this is not the same as requiring the maximum number of +disequality constraints to be satisfied. The \alldiff constraints, while +apparently in a mixed context, are actually in a positive context, since the +maximization in fact is implemented by inequalities forcing at least some number +to be true. + +In Table~\ref{tab:qcp} we compare three different resulting programs on QCP-max +problems: full reification of the model above, using the \alldiff decomposition +defined by the predicate shown (\textsf{full}), half reification of the model +using the \alldiff decomposition (\textsf{half}), and half reification using a +half-reified global \alldiff (\textsf{half-g}) implementing arc consistency +(thus having the same propagation strength as the decomposition). \jip{is this + still correct??} We use standard QCP examples from the literature, and group +them by size. +% and whether they are satisfiable or unsatisfiable as QCP problems. +We compare both a standard finite domain solver (FD) and a learning lazy clause +generation solver (FD + Explanations). We use the same fixed search strategy of +labeling the matrix in order left-to-right from highest to lowest value for all +approaches to minimize differences in search. + +\begin{table} [tb] \begin{center} +\caption{\label{tab:qcp} QCP-max problems: +Average time (in seconds), number of solved instances (300s timeout).} +\begin{tabular}{|l||rr|rr|rr|} +\hline +Instances & \multicolumn{2}{c|}{\textsf{half-g}} & \multicolumn{2}{c|}{\textsf{half}} & \multicolumn{2}{c|}{\textsf{full}} \\ +\hline +\texttt{qcp-10} (x15) & 17.12 & 15 & 21.17 & 14 & 21.09 & 14 \\ +\hline +\texttt{qcp-15} (x15) & 40.35 & 13 & 40.52 & 13 & 40.55 & 13 \\ +\hline +\texttt{qcp-20} (x15) & 27.50 & 14 & 64.05 & 14 & 65.55 & 14 \\ +\hline +\texttt{qcp-25} (x15) & 195.85 & 6 & 223.44 & 6 & 225.22 & 6 \\ +\hline +\end{tabular} +\end{center} +\end{table} + +\jip{adjust text to match new table}Half reification of the decomposition is +more efficient, principally because it introduces fewer Boolean variables, and +the direct implementation of the half reified constraint is more efficient +still. Note that learning can be drastically changed by the differences in the +model and \textsf{full} solves one more instance in \texttt{qcp-20}, thus +winning in that case. Apart from this instance, the half reified versions give +an almost uniform improvement. + +The second experiment shows how half reification can reduce the overhead of +handling partial functions correctly. Consider the following model for +determining a prize collecting path, a simplified form of prize collecting +travelling salesman problem +\autocite{balas-1989-pctsp}, %shown in Figure~\ref{fig:pct} +where the aim is define an acyclic path from node 1 along weighted edges to +collect the most weight. Not every node needs to be visited ($pos[i] = 0$). + +\begin{mzn} +int: n; % size +array[1..n,0..n] of int: p; % prize for edge (i,j), p[i,0] = 0 + +array[1..n] of var 0..n: next; % next posn in tour +array[1..n] of var 0..n: pos; % posn on node i in path, 0=notin +array[1..n] of var int: prize = [p[i,next[i]] | i in 1..n]; + % prize for outgoing edge + +constraint forall(i in 1..n)( + (pos[i] = 0 <-> next[i] = 0) /\ + (next[i] > 1 -> pos[next[i]] = pos[i] + 1)); + +include "alldifferent_except_0.mzn"; +constraint alldifferent_except_0(next) /\ pos[1] = 1; + +solve minimize sum(i in 1..n)(prize[i]); +\end{mzn} + +It uses the global constraint \texttt{alldifferent\_except\_0} which constrains +each element in the $next$ array to be different or equal 0. The model has one +unsafe array lookup $pos[next[i]]$. We compare using full reification +(\textsf{full}) and half reification (\textsf{half}) to model this problem. Note +that if we extend the $pos$ array to have domain $0..n$ then the model becomes +safe, by replacing its definition with the following two lines + +\begin{mzn} + array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin + constraint pos[0] = 0; +\end{mzn} + +We also compare against this model (\textsf{extended}). + +We use graphs with both positive and negative weights for the tests. The search +strategy fixes the $next$ variables in order of their maximum value. First we +note that \textsf{extended} is slightly better than \textsf{full} because of the +simpler translation, while \textsf{half} is substantially better than +\textsf{extended} since most of the half reified \texttt{element} constraints +become redundant. Learning increases the advantage because the half reified +formulation focusses on propagation which leads to failure which creates more +reusable nogoods. + +\begin{table} [tb] \begin{center} +\caption{\label{tab:pctsp} Prize collecting paths: +Average time (in seconds) and number of solved +instances with a 300s timeout for various number of nodes.} +\begin{tabular}{|l||rr|rr|rr||rr|rr|rr|} +\hline + & \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\ +Nodes & + \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} & + \multicolumn{2}{|c|}{\textsf{extended}}& \multicolumn{2}{|c|}{\textsf{full}} & + \multicolumn{2}{|c|}{\textsf{half}} & \multicolumn{2}{|c|}{\textsf{extended}} + \\ +\hline +15-3-5 (x 10) & 0.31&10& 0.25&10& 0.26&10 & 0.21&10 & 0.17&10 & 0.17&10 \\ +\hline +18-3-6 (x 10) & 1.79&10& 1.37&10& 1.52&10 & 0.70&10 & 0.51&10 & 0.58&10 \\ +\hline +20-4-5 (x 10) & 5.30&10& 4.04&10& 4.51&10 & 1.28&10 & 0.97&10 & 1.17&10 \\ +\hline +24-4-6 (x 10) & 46.03&10& 34.00&10& 40.06&10 & 7.28&10 & 4.91&10 & 6.37&10 \\ +\hline +25-5-5 (x 10) & 66.41&10& 50.70&10& 57.51&10 & 9.75&10 & 6.58&10 & 8.28&10 \\ +\hline +28-4-7 (x 10) & 255.06&5& 214.24&8& 241.10&6 & 38.54&10 & 23.27&10 & 34.83&10 \\ +\hline +30-5-6 (x 10) & 286.48&1& 281.00&2& 284.34&1 & 100.54&10 & 60.65&10 & 92.19&10\\ +\hline +32-4-8 (x 10) & 300.00&0& 297.12&1& 300.00&0 & 229.86&5 & 163.73&10 & 215.16&8\\ +\hline + +%15-3-5 (x 10) & 0.31&10& 0.31&10& 0.26&10 & 0.21&10 & 0.19&10 & 0.17&10 \\ +%\hline +%18-3-6 (x 10) & 1.79&10& 1.77&10& 1.52&10 & 0.70&10 & 0.57&10 & 0.58&10 \\ +%\hline +%20-4-5 (x 10) & 5.30&10& 5.31&10& 4.51&10 & 1.28&10 & 1.13&10 & 1.17&10 \\ +%\hline +%24-4-6 (x 10) & 46.03&10& 47.43&10& 40.06&10 & 7.28&10 & 6.00&10 & 6.37&10 \\ +%\hline +%25-5-5 (x 10) & 66.41&10& 70.03&10& 57.51&10 & 9.75&10 & 8.57&10 & 8.28&10 \\ +%\hline +%28-4-7 (x 10) & 255.06&5& 260.79&5& 241.10&6 & 38.54&10 & 28.05&10 & 34.83&10 \\ +%\hline +%30-5-6 (x 10) & 286.48 &0& 287.33 &0& 284.34 &0 & 100.54&10 & 83.50&10 & 92.19&10 \\ +%\hline +%32-4-8 (x 10) & 300.00 &0& 300.00 &0& 300.00 &0 & 229.86&5 & 187.40&9 & 215.16&8 \\ +%\hline +\end{tabular} +\end{center} +\end{table} + +In the final experiment we compare resource constrained project scheduling +problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task +decomposition as in Example~\ref{ex:cumul} above, using both full reification +and half-reification. We use standard benchmark examples from +PSPlib~\autocite{psplib}. Table~\ref{tab:rcpsp} compares RCPSP instances using +\textsf{full} reification and \textsf{half} reification. We compare using J30 +instances (\textsf{J30} ) and instances due to Baptiste and Le Pape +(\textsf{BL}). Each line in the table shows the average run time and number of +solved instances. The search strategy tries to schedule the task with the +earliest possible start time. We find a small and uniform speedup for +\textsf{half} over \textsf{full} across the suites, which improves with +learning, again because learning is not confused by propagations that do not +lead to failure. + +\begin{table} [tb] \caption{\label{tab:rcpsp} RCPSP: +Average time (in seconds) and number of solved instances with a 300s timeout.} +\begin{center} +\begin{tabular}{|l||rr|rr||rr|rr|} +\hline + & \multicolumn{4}{|c||}{FD} & \multicolumn{4}{|c|}{FD + Explanations} \\ + Instances & + \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} + & \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}}\\ +\hline +BL (x 40) & 277.2 & 5 & 269.3 & 5 & 17.1 & 39 & 15.4 & 39\\ +\hline +J30 (x 480) & 116.1 & 300 & 114.3 & 304 & 16.9 & 463 & 12.9 & 468\\ +\hline +\end{tabular} +\end{center} +\tableend +\end{table} + +\subsection{MiniZinc Challenge} + +To verify the effectiveness of the half reification implementation within the +\minizinc{} distribution we compare the results of the current version of the +\minizinc{} translator (rev. \jip{add revision}) against the equivalent version +for which we have implemented half reification. We use the model instances used +by the \minizinc{} challenges\autocite{challenge} from 2012 until 2017. Note +that the instances that the instances without any reifications have been +excluded from the experiment as they would not experience any change. The +performance of the generated \flatzinc{} models will be tested using Gecode, +flattened with its own library, and Gurobi and CBC, flattened with the linear +library. + +\begin{table} [tb] + \caption{\label{tab:flat_results} Flattening results: Average changes in the + generated the \flatzinc{} models} + \begin{center} + \begin{tabular}{|l|r||r|r|r||r|} + \hline + Library & Nr. Instances & Full Reifications + & Constraints & Variables & Chains Compressed\\ + \hline + Gecode & 274 & -38.19\% & -6.29\% & -8.66\% & 21.35\% \\ + \hline + Linear & 346 &- 33.11\% & -13.77\% & -3.70\% & 11.63\% \\ + \hline + \end{tabular} + \end{center} + \tableend +\end{table} +\jip{Better headers for table \ref{tab:flat_results} and update with current +results} + +Table \ref{tab:flat_results} shows the average change on the number of full +reification, constraints, and variables between the \flatzinc{} models generated +by the different versions of the translator using the different libraries. We +find that the number full reifications is reduced by a significant amount. +Together with the chain compressions this has a positive effect on the number of +constraints and the number of variables. + +\jip{Add something regarding the chain compression. Is this the right +statistic? (Compressions in terms of reifications)} + +We ran our experiments on a computer with a 3.40GHz Intel i7-3770 CPU and 16Gb +of memory running the Ubuntu 16.04.3 LTS operating system. + +\jip{Scatter plot of the runtimes + discussion!} + +%=============================================================================% +\section{Related Work and Conclusion} +\label{conclusion} +%=============================================================================% + +Half reification on purely Boolean constraints is well understood, this is the +same as detecting the \emph{polarity} of a gate, and removing half of the +clausal representation of the circuit (see e.g.~\autocite{polarity}). The +flattening of functions (partial or total) and the calculation of polarity for +Booleans terms inside \texttt{bool2int} do not arise in pure Boolean +constraints. + +Half reified constraints have been used in constraint modeling but are typically +not visible as primitive constraints to users, or produced through flattening. +Indexicals~\autocite{indexicals} can be used to implement reified constraints by +specifying how to propagate a constraint $c$, %($prop(c)$), +propagate its negation, +%$prop(\neg c)$, +check disentailment, % $check(c)$, +and check entailment, %$check(\neg c)$, +and this is implemented in SICstus Prolog~\autocite{sicstus}. A half reified +propagator simply omits entailment and propagating the negation. +%$prop(\neg c)$ and $check(\neg c)$. +%Half reification was briefly discussed in our earlier work~\autocite{cp2009d}, +%in terms of its ability to reduce propagation. +Half reified constraints appear in some constraint systems, for example SCIP +\autocite{gamrath-2020-scip} supports half-reified real linear constraints of +the form $b \half \sum_i a_i x_i \leq a_0$ exactly because the negation of the +linear constraint $\sum_i a_i x_i > a_0$ is not representable in an LP solver so +full reification is not possible. + +While flattening is the standard approach to handle complex formula involving +constraints, there are a number of other approaches which propagate more +strongly. Schulte proposes a generic implementation of $b \full c$ propagating +(the flattened form of) $c$ in a separate constraint space which does not affect +the original variables \autocite*{schulte-2000-deep}; entailment and +disentailment of $c$ fix the $b$ variable appropriately, although when $b$ is +made $\false$ the implementation does not propagate $\neg c$. This can also be +implemented using propagator groups~\autocite{groups}. Brand and Yap define an +approach to propagating complex constraint formulae called controlled +propagation which ensures that propagators that cannot affect the satisfiability +are not propagated \autocite*{brand-2006-propagation}. They note that for a +formula without negation, they could omit half their control rules, +corresponding to the case for half reification of a positive context. Jefferson +et al. similarly define an approach to propagating positive constraint formulae +by using watch literal technology to only wake propagators for reified +constraints within the formula when they can affect the final result +\autocite*{jefferson-2010-connectives}. They use half reified propagators, which +they call the ``reifyimplied'' form of a constraint, in some of their constraint +models, though they do not compare half reified models against full reified +models. We can straightforwardly fit these stronger propagation approaches to +parts of a constraint formula into the flattening approach by treating the whole +formula as a predicate, and the implementation of the stronger propagation as +its propagator. + +A passing contribution of this paper is a much simpler approach to enforcing the +relational semantics, by combining the ``safening'' of expressions with +flattening. The original approach of \autocite{frisch-2009-undefinedness} is a +source to source transformation without flattening and substantially more +complex. + +We suggest that all finite domain constraint solvers should move to supporting +half-reified versions of all constraints. This imposes no further burden on +solver implementors, it allows more models to be solved, it can be used to +implement full reification, and it can allow translation to more efficient +models. diff --git a/dekker_thesis.tex b/dekker_thesis.tex index fa8ecc0..6f42627 100644 --- a/dekker_thesis.tex +++ b/dekker_thesis.tex @@ -43,7 +43,7 @@ following publication: \include{chapters/2_background} \include{chapters/3_paradigms} \include{chapters/4_rewriting} -\include{chapters/5_half_reif} +% \include{chapters/5_half_reif} \include{chapters/6_incremental} \backmatter{}