Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Minor glossary fixes

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-28 16:17:44 +10:00
parent affa257ac0
commit b510c3edea
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
5 changed files with 33 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
assets/acronyms.tex
View File

@ -1,22 +1,22 @@
\newacronym[see={[Glossary:]{gls-api}}]{api}{API\glsadd{gls-api}}{Application Programming Interface} \newacronym[see={[Glossary:]{gls-api}}]{api}{API\glsadd{gls-api}}{\emph{Application Programming Interface}}
\newacronym[see={[Glossary:]{gls-ampl}}]{ampl}{AMPL\glsadd{gls-ampl}}{A Mathematical Programming Language} \newacronym[see={[Glossary:]{gls-ampl}}]{ampl}{AMPL\glsadd{gls-ampl}}{\emph{A Mathematical Programming Language}}
\newacronym[see={[Glossary:]{gls-ast}}]{ast}{AST\glsadd{gls-ast}}{Abstract Syntax Tree} \newacronym[see={[Glossary:]{gls-ast}}]{ast}{AST\glsadd{gls-ast}}{\emph{Abstract Syntax Tree}}
\newacronym[see={[Glossary:]{gls-cbc}}]{cbc}{CBC\glsadd{gls-cbc}}{COIN-OR Branch-and-Cut} \newacronym[see={[Glossary:]{gls-cbc}}]{cbc}{CBC\glsadd{gls-cbc}}{\emph{COIN-OR Branch-and-Cut}}
\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based Local Search} \newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{\emph{Constraint-Based Local Search}}
\newacronym[see={[Glossary:]{gls-chr}}]{chr}{CHR\glsadd{gls-chr}}{Constraint Handling Rules} \newacronym[see={[Glossary:]{gls-chr}}]{chr}{CHR\glsadd{gls-chr}}{\emph{Constraint Handling Rules}}
\newacronym[see={[Glossary:]{gls-clp}}]{clp}{CLP\glsadd{gls-clp}}{Constraint Logic Programming} \newacronym[see={[Glossary:]{gls-clp}}]{clp}{CLP\glsadd{gls-clp}}{\emph{Constraint Logic Programming}}
\newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP\glsadd{gls-cp}}{Constraint Programming} \newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP\glsadd{gls-cp}}{\emph{Constraint Programming}}
\newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common Sub-expression Elimination} \newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common Sub-expression Elimination}
\newacronym{cnf}{CNF}{Conjunctive Normal Form} \newacronym{cnf}{CNF\glsadd{cnf}}{\emph{Conjunctive Normal Form}}
\newacronym{cpu}{CPU}{Central Processing Unit} \newacronym{cpu}{CPU}{Central Processing Unit}
@ -24,23 +24,23 @@
\newacronym{gbac}{GBAC}{Generalized Balanced Academic Curriculum} \newacronym{gbac}{GBAC}{Generalized Balanced Academic Curriculum}
\newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{Lazy Clause Generation} \newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{\emph{Lazy Clause Generation}}
\newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large Neighbourhood Search} \newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{\emph{Large Neighbourhood Search}}
\newacronym{lp}{LP}{Linear Programming} \newacronym{lp}{LP}{Linear Programming}
\newacronym{maxsat}{MaxSAT}{Maximum Satisfiability} \newacronym{maxsat}{MaxSAT\glsadd{gls-maxsat}}{\emph{Maximum Satisfiability}}
\newacronym{mix}{\textit{mix}}{mixed context} \newacronym{mix}{\textit{mix}}{mixed context}
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer Programming} \newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{\emph{Mixed Integer Programming}}
\newacronym{neg}{\textit{neg}}{negative context} \newacronym{neg}{\textit{neg}}{negative context}
\newacronym{np}{NP}{Nondeterministic Polynomial-time} \newacronym{np}{NP}{Nondeterministic Polynomial-time}
\newacronym{or}{OR}{Operational Research} \newacronym{or}{OR}{Operations Research}
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The Optimization Programming Language} \newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The Optimization Programming Language}
@ -52,7 +52,7 @@
\newacronym{root}{\textit{root}}{root context} \newacronym{root}{\textit{root}}{root context}
\newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability} \newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{\emph{Boolean Satisfiability}}
\newacronym{tsp}{TSP}{Travelling Salesperson Problem} \newacronym{tsp}{TSP}{Travelling Salesperson Problem}

12
assets/glossary.tex
View File

@ -126,6 +126,11 @@
description={A type of expression that makes a choice between two or more expressions. In \minizinc{} these expressions take the form \mzninline{if @\(B\)@ then @\(X\)@ else @\(Y\)@endif}.}, description={A type of expression that makes a choice between two or more expressions. In \minizinc{} these expressions take the form \mzninline{if @\(B\)@ then @\(X\)@ else @\(Y\)@endif}.},
} }
\newglossaryentry{gls-cnf}{
name={conjunctive normal form},
description={The formulation of a Boolean formula as a conjunction of disjunctions of Boolean literals. This a standardized format for \gls{gls-sat} problems.},
}
\newglossaryentry{constraint}{ \newglossaryentry{constraint}{
name={constraint}, name={constraint},
description={A formalized rule of a problem. Constraints are generally expressed in terms of Boolean logic.}, description={A formalized rule of a problem. Constraints are generally expressed in terms of Boolean logic.},
@ -396,6 +401,11 @@
description={A \gls{trs} has reached its normal form when none of the rewriting rules can be applied.}, description={A \gls{trs} has reached its normal form when none of the rewriting rules can be applied.},
} }
\newglossaryentry{gls-maxsat}{
name={Maximum Satisfiability},
description={An extension of the \gls{gls-sat} problem class into an \gls{opt-prb}. A \gls{gls-sat} problem in \gls{gls-cnf} is extended with weights for each clause. An \gls{opt-sol} of a problem \instance{} maximizes the weights of the \gls{satisfied} clauses.},
}
\newglossaryentry{gls-mip}{ \newglossaryentry{gls-mip}{
name={mixed integer programming}, name={mixed integer programming},
description={ description={
@ -483,7 +493,7 @@
} }
\newglossaryentry{gls-sat}{ \newglossaryentry{gls-sat}{
name={boolean satisfiability}, name={Boolean satisfiability},
description={ description={
A problem class that tries to find a valid \gls{assignment} for a set of Boolean \glspl{variable} subject to a logical formula. A problem class that tries to find a valid \gls{assignment} for a set of Boolean \glspl{variable} subject to a logical formula.
Boolean satisfiability is extensively studied and there are many \glspl{solver} dedicated to solving this problem class. Boolean satisfiability is extensively studied and there are many \glspl{solver} dedicated to solving this problem class.

8
chapters/2_background.tex
View File

@ -676,10 +676,10 @@ Instead, it is sometimes better to use a \gls{propagator} with a lower level of
Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency. Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency.
This is, for example, the case for integer linear \constraints{} \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer \parameters{} and \(x_{i}\) are integer \variable{}. This is, for example, the case for integer linear \constraints{} \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer \parameters{} and \(x_{i}\) are integer \variable{}.
For these \constraints{}, a realistic \gls{domain-con} \gls{propagator} cannot exist because the problem is \gls{np}-hard \autocite{choi-2006-fin-cons}. For these \constraints{}, a realistic \gls{domain-con} \gls{propagator} cannot exist because the problem is \glsxtrshort{np}-hard \autocite{choi-2006-fin-cons}.
A more feasible problem is to find the minimal and maximal values, or \gls{bounds}, for the \variables{} had they been rational numbers. A more feasible problem is to find the minimal and maximal values, or \gls{bounds}, for the \variables{} had they been rational numbers.
A \gls{boundsr-con} \gls{propagator} then ensures that the values in the \domain{} of the integer \variables{} are between their rational \gls{bounds}. A \gls{boundsr-con} \gls{propagator} then ensures that the values in the \domain{} of the integer \variables{} are between their rational \gls{bounds}.
Note that this is a relaxation of calculating the integer \gls{bounds}, to create a \gls{boundsz-con} \gls{propagator}, which is still \gls{np}-hard. Note that this is a relaxation of calculating the integer \gls{bounds}, to create a \gls{boundsz-con} \gls{propagator}, which is still \glsxtrshort{np}-hard.
We will see the same relaxation in mathematical programming, discussed in the next section. We will see the same relaxation in mathematical programming, discussed in the next section.
Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}. Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}.
@ -723,7 +723,7 @@ It was questioned whether the same problem could be solved in worst-case polynom
Methods for solving linear programs provide the foundation for a harder problem. Methods for solving linear programs provide the foundation for a harder problem.
In \gls{lp} our \variables{} must be continuous. In \gls{lp} our \variables{} must be continuous.
If we require that one or more take an integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \gls{np} hard. If we require that one or more take an integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \glsxtrshort{np}-hard.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take an integer value). The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take an integer value).
Unlike \gls{lp}, there is not an algorithm that solves a mixed integer program in polynomial time. Unlike \gls{lp}, there is not an algorithm that solves a mixed integer program in polynomial time.
@ -784,7 +784,7 @@ An indicator variable \(y_{i}\) is a \gls{avar} that for a \variable{} \(x\) tak
\glsreset{maxsat} \glsreset{maxsat}
The study of the \gls{sat} problem is one of the oldest in computer science. The study of the \gls{sat} problem is one of the oldest in computer science.
The DPLL algorithm that is still the basis for modern \gls{sat} solving stems from the 1960s \autocite{davis-1960-dpll, davis-1962-dpll}, and \gls{sat} was the first problem to be proven to be \gls{np}-complete \autocite{cook-1971-sat}. The DPLL algorithm that is still the basis for modern \gls{sat} solving stems from the 1960s \autocite{davis-1960-dpll, davis-1962-dpll}, and \gls{sat} was the first problem to be proven to be \glsxtrshort{np}-complete \autocite{cook-1971-sat}.
The problem asks if there is an \gls{assignment} for the \variables{} of a given Boolean formula, such that the formula is \gls{satisfied}. The problem asks if there is an \gls{assignment} for the \variables{} of a given Boolean formula, such that the formula is \gls{satisfied}.
This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type and all \constraints{} are simple Boolean formulas. This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type and all \constraints{} are simple Boolean formulas.

2
chapters/5_incremental.tex
View File

@ -23,7 +23,7 @@ The following algorithms are examples of \gls{meta-optimization}.
Instead, it can be achieved using a \gls{meta-optimization} approach: find a \gls{sol} to a (single-objective) problem, then add more \constraints{} to the original problem and repeat. Instead, it can be achieved using a \gls{meta-optimization} approach: find a \gls{sol} to a (single-objective) problem, then add more \constraints{} to the original problem and repeat.
\item[\gls{lns}] \autocite{shaw-1998-local-search} \item[\gls{lns}] \autocite{shaw-1998-local-search}
This is a very successful \gls{meta-optimization} algorithm to quickly improve \gls{sol} quality. This \gls{meta-optimization} algorithm was first introduced as a heuristic to vehicle routing problem, but has proven to be a very successful method to quickly improve \gls{sol} quality for many types of problem.
After finding a (sub-optimal) \gls{sol} to a problem, \constraints{} are added to restrict the search in the \gls{neighbourhood} of that \gls{sol}. After finding a (sub-optimal) \gls{sol} to a problem, \constraints{} are added to restrict the search in the \gls{neighbourhood} of that \gls{sol}.
When a new \gls{sol} is found, the \constraints{} are removed, and \constraints{} for a new \gls{neighbourhood} are added. When a new \gls{sol} is found, the \constraints{} are removed, and \constraints{} for a new \gls{neighbourhood} are added.

4
chapters/A2_benchmark.tex
View File

@ -4,8 +4,8 @@
%************************************************ %************************************************
\noindent{}All experiments included in this thesis were conducted on a dedicated node in a computational cluster. \noindent{}All experiments included in this thesis were conducted on a dedicated node in a computational cluster.
The machine operates using an \textbf{Intel Xeon 8260} \gls{cpu}, which has 24 non-hyperthreaded cores, and has access to \textbf{268.55 GB} of \gls{ram}. The machine operates using an \textbf{Intel Xeon 8260} \glsxtrshort{cpu}, which has 24 non-hyperthreaded cores, and has access to \textbf{268.55 GB} of \gls{ram}.
Each experimental test was given exclusive access to a single \gls{cpu} core and access to sufficient \gls{ram}. Each experimental test was given exclusive access to a single \glsxtrshort{cpu} core and access to sufficient \glsxtrshort{ram}.
\section{Experimental Design}% \section{Experimental Design}%
\label{sec:bench-env} \label{sec:bench-env}