A lot of work on the background section
This commit is contained in:
parent
e9c7b6ffca
commit
595ca2246a
@ -34,18 +34,27 @@
|
||||
|
||||
\newacronym{maxsat}{MaxSAT}{Maximum Satisfiability}
|
||||
|
||||
\newacronym{mix}{\textit{mix}}{mixed context}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer Programming}
|
||||
|
||||
\newacronym{neg}{\textit{neg}}{negative context}
|
||||
|
||||
\newacronym{np}{NP}{Nondeterministic Polynomial-time}
|
||||
|
||||
\newacronym{or}{OR}{Operational Research}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The Optimisation Programming Language}
|
||||
|
||||
\newacronym{pos}{\textit{pos}}{positive context}
|
||||
|
||||
\newacronym{ram}{RAM}{Random Access Memory}
|
||||
|
||||
\newacronym{root}{\textit{root}}{root context}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System}
|
||||
|
||||
\newacronym{tsp}{TSP\glsadd{gls-trs}}{Travelling Salesperson Problem}
|
||||
|
||||
|
||||
@ -265,6 +265,24 @@
|
||||
year = 2020,
|
||||
}
|
||||
|
||||
@article{davis-1960-dpll,
|
||||
author = {Davis, Martin and Putnam, Hilary},
|
||||
title = {A Computing Procedure for Quantification Theory},
|
||||
year = {1960},
|
||||
issue_date = {July 1960},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
volume = {7},
|
||||
number = {3},
|
||||
issn = {0004-5411},
|
||||
url = {https://doi.org/10.1145/321033.321034},
|
||||
doi = {10.1145/321033.321034},
|
||||
journal = {J. ACM},
|
||||
month = jul,
|
||||
pages = {201–215},
|
||||
numpages = {15},
|
||||
}
|
||||
|
||||
@article{davis-1962-dpll,
|
||||
author = {Davis, Martin and Logemann, George and Loveland, Donald},
|
||||
title = {A Machine Program for Theorem-Proving},
|
||||
@ -283,6 +301,25 @@
|
||||
numpages = 4,
|
||||
}
|
||||
|
||||
@inproceedings{een-2003-minisat,
|
||||
author = {Niklas E{\'{e}}n and Niklas S{\"{o}}rensson},
|
||||
editor = {Enrico Giunchiglia and Armando Tacchella},
|
||||
title = {An Extensible SAT-solver},
|
||||
booktitle = {Theory and Applications of Satisfiability Testing, 6th
|
||||
International Conference, {SAT} 2003. Santa Margherita Ligure,
|
||||
Italy, May 5-8, 2003 Selected Revised Papers},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
volume = {2919},
|
||||
pages = {502--518},
|
||||
publisher = {Springer},
|
||||
year = {2003},
|
||||
url = {https://doi.org/10.1007/978-3-540-24605-3\_37},
|
||||
doi = {10.1007/978-3-540-24605-3\_37},
|
||||
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
|
||||
biburl = {https://dblp.org/rec/conf/sat/EenS03.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org},
|
||||
}
|
||||
|
||||
@inproceedings{ek-2020-online,
|
||||
author = {Alexander Ek and Maria Garcia de la Banda and Andreas Schutt and
|
||||
Peter J. Stuckey and Guido Tack},
|
||||
|
||||
@ -45,12 +45,12 @@
|
||||
|
||||
\newglossaryentry{backtrack}{
|
||||
name={backtrack},
|
||||
description={},
|
||||
description={A \gls{solver} is said to backtrack when it revisits a search decision (\eg{} an value assumed during search). Notably the action of backtracking generally involves invalidating all effects of the revisited and subsequent search decisions},
|
||||
}
|
||||
|
||||
\newglossaryentry{bnb}{
|
||||
name={branch and bound},
|
||||
description={},
|
||||
description={A search method to find an \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is proven that no such \gls{sol} exists, then the final incumbent \gls{sol} is an \gls{opt-sol}},
|
||||
}
|
||||
|
||||
\newglossaryentry{byte-code}{
|
||||
@ -60,7 +60,7 @@
|
||||
|
||||
\newglossaryentry{bounds-con}{
|
||||
name={bounds consistent},
|
||||
description={},
|
||||
description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-cbls}{
|
||||
@ -98,11 +98,6 @@
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{constraint-store}{
|
||||
name={constraint store},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{cplex}{
|
||||
name={CPLEX},
|
||||
description={},
|
||||
@ -130,7 +125,7 @@
|
||||
|
||||
\newglossaryentry{confluence}{
|
||||
name={confluence},
|
||||
description={},
|
||||
description={A property of a \gls{trs}. The system is said to be confluent if it always arrives at the same \gls{normal-form}},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-csp}{
|
||||
@ -191,7 +186,7 @@
|
||||
|
||||
\newglossaryentry{domain-con}{
|
||||
name={domain consistent},
|
||||
description={},
|
||||
description={A \gls{propagator} is domain consistent if it is able to remove all values from \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied},
|
||||
}
|
||||
|
||||
\newglossaryentry{essence}{
|
||||
@ -260,9 +255,9 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{indicator-var}{
|
||||
name={indicator variable},
|
||||
description={},
|
||||
\newglossaryentry{half-reified}{
|
||||
name={half reified},
|
||||
description={See \gls{half-reif}},
|
||||
}
|
||||
|
||||
\newglossaryentry{ivar}{
|
||||
@ -290,11 +285,24 @@
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{kleene-sem}{
|
||||
name={Kleene semantic},
|
||||
description={
|
||||
A semantic model for treating undefined behaviour in \glspl{cml}.
|
||||
Under Kleene semantics an occurrence of undefined behaviour will only cause its surrounding expression to be undefined when its value is required to compute its result
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{knapsack}{
|
||||
name={knapsack problem},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{linearisation}{
|
||||
name={linearisation},
|
||||
description={The process of \gls{rewriting} a \gls{model} to a mixed integer program},
|
||||
}
|
||||
|
||||
\newglossaryentry{let}{
|
||||
name={let expression},
|
||||
description={},
|
||||
@ -397,7 +405,7 @@
|
||||
|
||||
\newglossaryentry{optional}{
|
||||
name={optional},
|
||||
description={},
|
||||
description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} model, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.},
|
||||
}
|
||||
|
||||
\newglossaryentry{opt-sol}{
|
||||
@ -434,6 +442,14 @@
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{strict-sem}{
|
||||
name={strict semantic},
|
||||
description={
|
||||
A semantic model for treating undefined behaviour in \glspl{cml}.
|
||||
Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{parameter}{
|
||||
name={problem parameter},
|
||||
description={
|
||||
@ -473,6 +489,19 @@
|
||||
description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} being enforced in the \glspl{sol}, it enforces that a \gls{cvar} represents whether the \gls{constraint} holds or not},
|
||||
}
|
||||
|
||||
\newglossaryentry{reified}{
|
||||
name={reified},
|
||||
description={See \gls{reification}},
|
||||
}
|
||||
|
||||
\newglossaryentry{rel-sem}{
|
||||
name={relational semantic},
|
||||
description={
|
||||
A semantic model for treating undefined behaviour in \glspl{cml}.
|
||||
Under relational semantics an occurrence of undefined behaviour will cause its closest surrounding Boolean expression to be \mzninline{false}
|
||||
},
|
||||
}
|
||||
|
||||
\newglossaryentry{rewriting}{
|
||||
name={rewriting},
|
||||
description={
|
||||
@ -504,27 +533,22 @@
|
||||
|
||||
\newglossaryentry{term}{
|
||||
name={term},
|
||||
description={},
|
||||
description={An expression in a \gls{trs}. A term can have nested sub-expressions},
|
||||
}
|
||||
|
||||
\newglossaryentry{termination}{
|
||||
name={termination},
|
||||
description={},
|
||||
description={A property of a \gls{trs}. A system is terminating if it is guaranteed to eventually arrive at a \gls{normal-form}},
|
||||
}
|
||||
|
||||
\newglossaryentry{trail}{
|
||||
name={trail},
|
||||
description={},
|
||||
description={A chronological account of changes to data structures with as goal to possibly reverse these changes. The usage of a trail is a common way for \gls{solver} to revisit search decisions (\ie{} \gls{backtrack})},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-trs}{
|
||||
name={term rewriting system},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{unification}{
|
||||
name={unification},
|
||||
description={},
|
||||
description={A computational model that expresses computation through the application of rewriting rules. A rewriting rule replaces the \glspl{term} on its left hand side with the \glspl{term} on its right hand side},
|
||||
}
|
||||
|
||||
\newglossaryentry{unsat}{
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
predicate basic_LNS() =
|
||||
(status() != START) -> nbh(X);
|
||||
(status() != START) -> nbh(X);
|
||||
|
||||
@ -28,6 +28,8 @@
|
||||
\newcommand*{\nanozinc}{\gls{nanozinc}\xspace{}}
|
||||
\newcommand*{\parameters}{\glspl{parameter}\xspace{}}
|
||||
\newcommand*{\parameter}{\gls{parameter}\xspace{}}
|
||||
\newcommand*{\reified}{\gls{reified}\xspace{}}
|
||||
\newcommand*{\halfreified}{\gls{half-reified}\xspace{}}
|
||||
\newcommand*{\solvers}{\glspl{solver}\xspace{}}
|
||||
\newcommand*{\solver}{\gls{solver}\xspace{}}
|
||||
\newcommand*{\variable}{\gls{variable}\xspace{}}
|
||||
@ -46,10 +48,10 @@
|
||||
\newcommand*{\Cbind}{\ensuremath{\wedge}}
|
||||
|
||||
% Context syntax (half-reification)
|
||||
\newcommand*{\rootc}{\textit{root}}
|
||||
\newcommand*{\posc}{\textit{pos}}
|
||||
\newcommand*{\negc}{\textit{neg}}
|
||||
\newcommand*{\mixc}{\textit{mix}}
|
||||
\newcommand*{\rootc}{\gls{root}}
|
||||
\newcommand*{\posc}{\gls{pos}}
|
||||
\newcommand*{\negc}{\gls{neg}}
|
||||
\newcommand*{\mixc}{\gls{mix}}
|
||||
\newcommand*{\mayberootc}{\textit{root?}}
|
||||
\newcommand*{\changepos}{\ensuremath{+}}
|
||||
\newcommand*{\changeneg}{\ensuremath{-}}
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@ -15,7 +15,7 @@ Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc
|
||||
The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.
|
||||
|
||||
In the remainder of this chapter we will first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose.
|
||||
\Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading constraint modelling language used within this thesis.
|
||||
\Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading \cml{} used within this thesis.
|
||||
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} can be used to solve a \gls{slv-mod}.
|
||||
\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
|
||||
Then, \cref{sec:back-term} survey the closely related technologies in the field of \glspl{trs}.
|
||||
|
||||
@ -644,7 +644,7 @@ The resulting \nanozinc{} looks like this:
|
||||
constraint g_rel(b, x);
|
||||
\end{nzn}
|
||||
|
||||
The process of equality propagation is similar to \gls{unification} in logic programming \autocite{warren-1983-wam}.
|
||||
The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
|
||||
However, since equations in \minizinc\ always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}.
|
||||
|
||||
\paragraph{Implementation}
|
||||
|
||||
@ -535,7 +535,7 @@ The declaration item of a \variable{} does not further the context, and does not
|
||||
It merely triggers the creation of a new \variable{}.
|
||||
The (Item0) rule is triggered when there are no more inner items in the let-expression.
|
||||
|
||||
\subsection{Potentially \rootc{}}%
|
||||
\subsection{Potentially Root}%
|
||||
\label{subsec:half-?root}
|
||||
|
||||
In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
|
||||
|
||||
Reference in New Issue
Block a user