From b510c3edea22108319992d26f7f9e711dc31290d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 28 Jul 2021 16:17:44 +1000 Subject: [PATCH] Minor glossary fixes --- assets/acronyms.tex | 30 +++++++++++++++--------------- assets/glossary.tex | 12 +++++++++++- chapters/2_background.tex | 8 ++++---- chapters/5_incremental.tex | 2 +- chapters/A2_benchmark.tex | 4 ++-- 5 files changed, 33 insertions(+), 23 deletions(-) diff --git a/assets/acronyms.tex b/assets/acronyms.tex index e6f100f..19e133e 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -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{cnf}{CNF}{Conjunctive Normal Form} +\newacronym{cnf}{CNF\glsadd{cnf}}{\emph{Conjunctive Normal Form}} \newacronym{cpu}{CPU}{Central Processing Unit} @@ -24,23 +24,23 @@ \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{maxsat}{MaxSAT}{Maximum Satisfiability} +\newacronym{maxsat}{MaxSAT\glsadd{gls-maxsat}}{\emph{Maximum Satisfiability}} \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{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} @@ -52,7 +52,7 @@ \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} diff --git a/assets/glossary.tex b/assets/glossary.tex index 92e5f69..0d2addc 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -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}.}, } +\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}{ name={constraint}, 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.}, } +\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}{ name={mixed integer programming}, description={ @@ -483,7 +493,7 @@ } \newglossaryentry{gls-sat}{ - name={boolean satisfiability}, + name={Boolean satisfiability}, description={ 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. diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 6467903..2d756a8 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -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. 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 \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. 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. 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). 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} 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}. 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. diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index dcab270..fa6c72b 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -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. \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}. When a new \gls{sol} is found, the \constraints{} are removed, and \constraints{} for a new \gls{neighbourhood} are added. diff --git a/chapters/A2_benchmark.tex b/chapters/A2_benchmark.tex index 55a3cc4..692802b 100644 --- a/chapters/A2_benchmark.tex +++ b/chapters/A2_benchmark.tex @@ -4,8 +4,8 @@ %************************************************ \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}. -Each experimental test was given exclusive access to a single \gls{cpu} core and access to sufficient \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 \glsxtrshort{cpu} core and access to sufficient \glsxtrshort{ram}. \section{Experimental Design}% \label{sec:bench-env}