From 645ae1fa3a7291e9a0350f74633d1a6e24dce378 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 4 Mar 2021 13:35:14 +1100 Subject: [PATCH] Fix final references --- assets/bibliography/references.bib | 122 +++++++++++++--- assets/glossary.tex | 2 +- assets/mzn/6_round_robin.mzn | 2 +- assets/mzn/6_status.mzn | 2 +- assets/packages.tex | 6 + assets/shorthands.tex | 2 + chapters/4_rewriting.tex | 15 +- chapters/5_half_reif.tex | 221 +++++++++++++++-------------- chapters/6_incremental.tex | 2 +- dekker_thesis.tex | 2 +- 10 files changed, 232 insertions(+), 144 deletions(-) diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 7e92265..836ddf5 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -132,6 +132,26 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@inproceedings{carlsson-1997-sicstus, + author = {Mats Carlsson and Greger Ottosson and Bj{\"{o}}rn Carlson}, + editor = {Hugh Glaser and Pieter H. Hartel and Herbert Kuchen}, + title = {An Open-Ended Finite Domain Constraint Solver}, + booktitle = {Programming Languages: Implementations, Logics, and + Programs, 9th International Symposium, PLILP'97, Including a + Special Trach on Declarative Programming Languages in + Education, Southampton, UK, September 3-5, 1997, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = 1292, + pages = {191--206}, + publisher = {Springer}, + year = 1997, + url = {https://doi.org/10.1007/BFb0033845}, + doi = {10.1007/BFb0033845}, + timestamp = {Tue, 14 May 2019 10:00:36 +0200}, + biburl = {https://dblp.org/rec/conf/plilp/CarlssonOC97.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}, @@ -369,6 +389,42 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{kolisch-1997-psplib, + title = {PSPLIB - A project scheduling problem library: OR Software + - ORSEP Operations Research Software Exchange Program}, + journal = {European Journal of Operational Research}, + volume = 96, + number = 1, + pages = {205-216}, + year = 1997, + issn = {0377-2217}, + doi = {https://doi.org/10.1016/S0377-2217(96)00170-1}, + url = + {https://www.sciencedirect.com/science/article/pii/S0377221796001701}, + author = {Rainer Kolisch and Arno Sprecher}, + keywords = {Project scheduling, Resource constraints, Benchmark + instances}, +} + +@inproceedings{lagerkvist-2009-groups, + author = {Mikael Z. Lagerkvist and Christian Schulte}, + editor = {Ian P. Gent}, + title = {Propagator Groups}, + 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 = {524--538}, + publisher = {Springer}, + year = 2009, + url = {https://doi.org/10.1007/978-3-642-04244-7\_42}, + doi = {10.1007/978-3-642-04244-7\_42}, + timestamp = {Tue, 14 May 2019 10:00:45 +0200}, + biburl = {https://dblp.org/rec/conf/cp/LagerkvistS09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{leo-2015-multipass, author = {Kevin Leo and Guido Tack}, editor = {Qiang Yang and Michael J. Wooldridge}, @@ -528,6 +584,21 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{plaisted-1986-polarity, + author = {David A. Plaisted and Steven Greenbaum}, + title = {A Structure-Preserving Clause Form Translation}, + journal = {J. Symb. Comput.}, + volume = 2, + number = 3, + pages = {293--304}, + year = 1986, + url = {https://doi.org/10.1016/S0747-7171(86)80028-1}, + doi = {10.1016/S0747-7171(86)80028-1}, + timestamp = {Wed, 17 Feb 2021 08:57:26 +0100}, + biburl = {https://dblp.org/rec/journals/jsc/PlaistedG86.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @inproceedings{rendl-2009-enhanced-tailoring, author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher Jefferson}, @@ -636,6 +707,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} +} + @inproceedings{schulte-2005-views, author = {Christian Schulte and Guido Tack}, editor = {Peter van Beek}, @@ -710,17 +792,6 @@ 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}, @@ -781,6 +852,24 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@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 = {3}, + year = {2020}, + url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023} +} + +@unpublished{van-hentenryck-1992-indexicals, + title = {Constraint processing in cc(FD)}, + author = {Van Hentenryck, P. and Saraswat, V. and Deville, Y.}, + year = 1992, + note = {Manuscript}, +} + @book{van-hentenryck-1999-opl, title = {The OPL Optimization Programming Language}, author = {Van Hentenryck, P. and Lustig, I. and Puget, J.F. and @@ -818,14 +907,3 @@ 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/glossary.tex b/assets/glossary.tex index 9d11d22..da6c77a 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -37,7 +37,7 @@ which the user creates a problem description, in this thesis referred to as name={common subexpression elimination}, description={Common Subexpression Elimination (CSE) is a technique used in the evaluation of programming languages to avoid redoing the same work. A -description of how CSE works in \cmls\ can be found in \cref{sec:3-cse}}, +description of how CSE works in \cmls\ can be found in \cref{sec:4-cse}}, } \newglossaryentry{gls-csp}{ diff --git a/assets/mzn/6_round_robin.mzn b/assets/mzn/6_round_robin.mzn index f7c626b..647d166 100644 --- a/assets/mzn/6_round_robin.mzn +++ b/assets/mzn/6_round_robin.mzn @@ -8,5 +8,5 @@ predicate round_robin(array[int] of var bool: nbhs) = select = (last_val(select) + 1) mod N endif /\ forall(i in 1..N) ( - select = i-1 -> nbhs[i] @\Vlabel{line:6:roundrobin:post}@ + select = i-1 -> nbhs[i] % <-- Post Neighbourhood@\Vlabel{line:6:roundrobin:post}@ ); diff --git a/assets/mzn/6_status.mzn b/assets/mzn/6_status.mzn index bd4ace5..368d11a 100644 --- a/assets/mzn/6_status.mzn +++ b/assets/mzn/6_status.mzn @@ -1,4 +1,4 @@ -predicate status(var int: stat); @\Vlabel{line:6:status}@ +predicate status(var int: stat); % <-- @\Vlabel{line:6:status}@ function var STATUS: status() = let { var STATUS: stat; diff --git a/assets/packages.tex b/assets/packages.tex index 0ed9a65..dc95f1d 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -98,3 +98,9 @@ outputdir=build, % Proof Tree \usepackage[nounderscore]{syntax} \usepackage{bussproofs} + +% Half Reif packages (maybe we should get rid of these) +\usepackage[all]{xy} +% Comments +\newcommand{\pjs}[1]{\textcolor{blue}{\Big[\textbf{Peter}: #1\Big]}} +\newcommand{\jip}[1]{\textcolor{red}{\Big[\textbf{Jip}: #1\Big]}} diff --git a/assets/shorthands.tex b/assets/shorthands.tex index 7706213..d2cdca7 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -71,3 +71,5 @@ \DeclareMathOperator{\ran}{\mathit{ran}} \DeclareMathOperator{\ite}{\mathit{ite}} \DeclareMathOperator{\VAR}{\mathit{VAR}} + +\DeclareMathOperator{\dom}{\mathit{idx}} diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 1b8d609..766d51a 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -222,7 +222,7 @@ type. A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list of calls, where the result of each call is bound to either an identifier or the constant true. The \syntax{$\sep$ *} will be used to track dependent -constraints (this will be explained in detail in \cref{sec:6-nanozinc}, for +constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now you can assume it is empty). \begin{figure} @@ -407,15 +407,16 @@ rewritten into \mzninline{int_gt(t,y)} and bound to fresh identifier \subsection{Rewriting Rules} The core of the proposed \minizinc\ architecture is an abstract machine that -performs the rewriting of \nanozinc\ items using the corresponding \microzinc +performs the rewriting of \nanozinc\ items using the corresponding \microzinc\ function definitions. We can now formally define the rewriting rules for this abstract machine. -The full set of rules appears in \cref{fig:4-rewrite-to-nzn}. To simplify -presentation, we assume that all rules that introduce new identifiers into the -\nanozinc\ program do so in a way that ensures those identifiers are fresh -(i.e., not used in the rest of the \nanozinc\ program), by suitable alpha -renaming. +The full set of rules appears in +\cref{fig:4-rewrite-to-nzn-calls,fig:4-rewrite-to-nzn-let,fig:4-rewrite-to-nzn-other}. +To simplify presentation, we assume that all rules that introduce new +identifiers into the \nanozinc\ program do so in a way that ensures those +identifiers are fresh (\ie\ not used in the rest of the \nanozinc\ program), by +suitable alpha renaming. \begin{figure*} \centering diff --git a/chapters/5_half_reif.tex b/chapters/5_half_reif.tex index 40e6ffb..bc90852 100644 --- a/chapters/5_half_reif.tex +++ b/chapters/5_half_reif.tex @@ -8,10 +8,10 @@ $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. +\autocite{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 @@ -708,7 +708,7 @@ 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, +(such as \mzninline{3 div 0}). We can extend the algorithms to handle this case, but it complicates the presentation. Our implementation aborts in this 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 @@ -734,21 +734,21 @@ 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$. +context.\footnote{Using half reification this can be relaxed to also allow + positive contexts.} They flatten their arguments and add an appropriate +built-in constraint. \callbyvalue{ User defined predicate applications flatten + their arguments and then flatten a renamed copy of the body.} \callbyunroll{ + User defined predicate applications are replaced by a renamed and flattened + copy of the body.} \emph{if-then-else} evaluates the condition (which must be +fixed) and flattens the \emph{then} or \emph{else} branch appropriately. +\pjs{USe the same resdtriction, but explain its not all required} The handling +of \texttt{let} is the most complicated. The expression is renamed with new +copies of the let variables. We extract the constraints from the \texttt{let} +expression using function \textsf{flatlet} which returns the extracted +constraint and a rewritten term (not used in this case, but used in \flatt{}). +The constraints returned by function \textsf{flatlet} are then flattened. +Finally if we are in the root context, we ensure that the Boolean $b$ returned +must be $\true$ by adding $b$ to $S$. { \begin{tabbing} @@ -1229,10 +1229,10 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ % $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}} +%\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 @@ -1376,16 +1376,15 @@ $$ % 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 +% 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 @@ -1499,8 +1498,8 @@ not propagate unnecessarily. \end{mzn} which may seem to be more expensive since there are additional variables (the - $b4[i]$), but since both $b4[i]$ and $a[i]$ are implemented by - views~\autocite{views}, there is no additional runtime overhead. This + $b4[i]$), but since both $b4[i]$ and $a[i]$ are implemented by views + \autocite{schulte-2005-views}, there is no additional runtime overhead. This decomposition will only wake the linear constraint when some task $i$ is guaranteed to overlap time $s[j]$. \end{example} @@ -2156,55 +2155,56 @@ the usual case for such a trivial propagator. % 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$. +\jip{There is a proof here, but I don't have a proof environment yet} +% \begin{theorem} +% $\forall D. \solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D) = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)$. +% \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{(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{(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} +% \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 @@ -2214,11 +2214,12 @@ 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} +\jip{The corollary environment is also missing} +% \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} @@ -2522,9 +2523,9 @@ Nodes & 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 +decomposition as in \cref{ex:cumul} above, using both full reification and +half-reification. We use standard benchmark examples from PSPlib +\autocite{kolisch-1997-psplib}. \Cref{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 @@ -2550,7 +2551,6 @@ 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} @@ -2559,8 +2559,9 @@ 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 +by the \minizinc{} challenges +\autocite{stuckey-2010-challenge,stuckey-2014-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 @@ -2581,7 +2582,6 @@ library. \hline \end{tabular} \end{center} - \tableend \end{table} \jip{Better headers for table \ref{tab:flat_results} and update with current results} @@ -2608,24 +2608,25 @@ of memory running the Ubuntu 16.04.3 LTS operating system. 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. +clausal representation of the circuit (see \eg\ +\autocite{plaisted-1986-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)$), +Indexicals \autocite{van-hentenryck-1992-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. +and this is implemented in SICstus Prolog \autocite{carlsson-1997-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 @@ -2639,11 +2640,11 @@ strongly. Schulte proposes a generic implementation of $b \full c$ propagating 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, +implemented using propagator groups \autocite{lagerkvist-2009-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 diff --git a/chapters/6_incremental.tex b/chapters/6_incremental.tex index e440f69..9217e05 100644 --- a/chapters/6_incremental.tex +++ b/chapters/6_incremental.tex @@ -671,7 +671,7 @@ model was flattened, then this flattening can be performed without any trailing. \begin{example}\label{ex:6-trail} - Let us look again at the resulting \nanozinc\ code from \Cref{ex:absreif}: + Let us look again at the resulting \nanozinc\ code from \cref{ex:4-absreif}: % \mznfile{assets/mzn/6_abs_reif_result.mzn} diff --git a/dekker_thesis.tex b/dekker_thesis.tex index 6f42627..fa8ecc0 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{}