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

Add background on MIP and SAT

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-17 19:59:51 +10:00
parent 2fad33d550
commit 771c450ea2
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
5 changed files with 297 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
assets/acronyms.tex
View File

@ -22,6 +22,8 @@
\newacronym[see={[Glossary:]{gls-csp}}]{csp}{CSP\glsadd{gls-csp}}{Constraint
Satisfaction Problem}
\newacronym{cnf}{CNF}{Conjunctive Normal Form}
\newacronym[see={[Glossary:]{gls-cop}}]{cop}{COP\glsadd{gls-cop}}{Constraint
Optimisation Problem}
@ -36,9 +38,15 @@
\newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large
Neighbourhood Search}
\newacronym{lp}{LP}{Linear Programming}
\newacronym{maxsat}{MAX-SAT}{Maximum Satisfiability}
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer
Programming}
\newacronym{np-comp}{NP-complete}{Nondeterministic Polynomial-time complete}
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The
Optimisation Programming Language}

137
assets/bibliography/references.bib
View File

@ -107,6 +107,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{biere-2021-sat,
title = {Handbook of Satisfiability},
author = {Biere, A. and Heule, M. and Van Maaren, H. and Walsh, T.},
isbn = 9781643681610,
series = {Frontiers in artificial intelligence and applications},
url = {https://books.google.com.au/books?id=YVSM3sxhBhcC},
year = 2021,
publisher = {IOS Press},
edition = 2,
}
@article{bjordal-2015-fzn2oscarcbls,
author = {Gustav Bj{\"{o}}rdal and Jean{-}No{\"{e}}l Monette and
Pierre Flener and Justin Pearson},
@ -196,6 +207,23 @@
numpages = 5
}
@inproceedings{cook-1971-sat,
author = {Stephen A. Cook},
editor = {Michael A. Harrison and Ranan B. Banerji and Jeffrey D.
Ullman},
title = {The Complexity of Theorem-Proving Procedures},
booktitle = {Proceedings of the 3rd Annual {ACM} Symposium on Theory of
Computing, May 3-5, 1971, Shaker Heights, Ohio, {USA}},
pages = {151--158},
publisher = {{ACM}},
year = 1971,
url = {https://doi.org/10.1145/800157.805047},
doi = {10.1145/800157.805047},
timestamp = {Mon, 26 Nov 2018 15:05:57 +0100},
biburl = {https://dblp.org/rec/conf/stoc/Cook71.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{davis-1962-dpll,
author = {Davis, Martin and Logemann, George and Loveland, Donald},
title = {A Machine Program for Theorem-Proving},
@ -268,6 +296,29 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@software{gecode-2021-gecode,
author = {{Gecode Team}},
title = {Gecode: A Generic Constraint Development Environment},
year = 2021,
url = {http://www.gecode.org},
version = {6.3.0},
}
@software{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual},
year = 2021,
url = {http://www.gurobi.com},
}
@software{minizinc-2021-minizinc,
author = {{MiniZinc Team}},
title = {MiniZinc: a free and open-source constraint modeling language},
year = 2021,
url = {http://www.minizinc.org},
version = {2.5.5},
}
@book{fourer-2003-ampl,
title = {AMPL: A Modeling Language for Mathematical Programming},
author = {Fourer, R. and Gay, D.M. and Kernighan, B.W.},
@ -293,29 +344,6 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@software{gecode-2021-gecode,
author = {{Gecode Team}},
title = {Gecode: A Generic Constraint Development Environment},
year = 2021,
url = {http://www.gecode.org},
version = {6.3.0},
}
@software{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual},
year = 2021,
url = {http://www.gurobi.com},
}
@software{minizinc-2021-minizinc,
author = {{MiniZinc Team}},
title = {MiniZinc: a free and open-source constraint modeling language},
year = 2021,
url = {http://www.minizinc.org},
version = {2.5.5},
}
@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},
@ -569,6 +597,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{mears-2014-option,
author = {Christopher Mears and Andreas Schutt and Peter J. Stuckey
and Guido Tack and Kim Marriott and Mark Wallace},
@ -608,17 +647,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}
}
@inproceedings{nethercote-2007-minizinc,
author = {Nicholas Nethercote and Peter J. Stuckey and Ralph Becket
and Sebastian Brand and Gregory J. Duck and Guido Tack},
@ -724,6 +752,15 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{rossi-2006-cp,
title = {Handbook of Constraint Programming},
author = {Rossi, F. and van Beek, P. and Walsh, T.},
isbn = 9780080463803,
series = {ISSN},
year = 2006,
publisher = {Elsevier Science}
}
@article{schiendorfer-2018-minibrass,
author = {Alexander Schiendorfer and Alexander Knapp and Gerrit
Anders and Wolfgang Reif},
@ -741,6 +778,16 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{schrijver-1998-mip,
title = {Theory of Linear and Integer Programming},
author = {Schrijver, A.},
isbn = 9780471982326,
lccn = {lc85012314},
series = {Wiley Series in Discrete Mathematics \& Optimization},
year = 1998,
publisher = {Wiley}
}
@article{schrijvers-2013-combinators,
author = {Tom Schrijvers and Guido Tack and Pieter Wuille and Horst
Samulowitz and Peter J. Stuckey},
@ -777,6 +824,17 @@
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}
}
@inproceedings{schulte-2005-views,
author = {Christian Schulte and Guido Tack},
editor = {Peter van Beek},
@ -851,17 +909,6 @@
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}
}
@book{silvano-1990-knapsack,
author = {Martello, Silvano and Toth, Paolo},
title = {Knapsack Problems: Algorithms and Computer Implementations},

5
assets/glossary.tex
View File

@ -150,6 +150,11 @@
description={},
}
\newglossaryentry{indicator-var}{
name={indicator variable},
description={},
}
\newglossaryentry{interval}{
name={interval},
description={},

1
assets/packages.tex
View File

@ -63,6 +63,7 @@ style=apa,
\usepackage[acronym,toc]{glossaries}
\usepackage[stylemods=bookindex]{glossaries-extra}
\usepackage{titlecaps}
\setabbreviationstyle[acronym]{long-short}
\defglsentryfmt[main]{\ifglsused{\glslabel}{\glsgenentryfmt}{\textit{\glsgenentryfmt}}}
\makeglossaries{}

198
chapters/2_background.tex
View File

@ -22,8 +22,10 @@ solution, we give a concise description of the problem. We describe what we
already know, the \glspl{parameter}, what we wish to know, the \glspl{variable},
and the relationships that should exist between them, the \glspl{constraint}.
This type of combinatorial problem is typically called a \gls{csp}. Many \cmls\
also support the modelling of \gls{cop}, where a \gls{csp} is augmented with a
This type of combinatorial problem is typically called a \gls{csp}. The goal of
a \gls{csp} is to find values for the \glspl{variable} that satisfy the
\glspl{constraint} or prove that no such assignment exists. Many \cmls\ also
support the modelling of \gls{cop}, where a \gls{csp} is augmented with a
\gls{objective} \(z\). In this case the goal is to find a solution that
satisfies all \glspl{constraint} while minimising (or maximising) \(z\).
@ -617,24 +619,206 @@ this section will discuss the other dominant technologies used used by
\label{subsec:back-cp}
\glsreset{cp}
\gls{cp}
When given a \gls{csp}, one might wonder what the best way is to find a solution
to the problem. The simplest solution would be to apply ``brute force'': try
every value in the \gls{domain} all \glspl{variable}. It will not surprise the
reader that this is an inefficient approach. Given, for example, the constraint
\begin{mzn}
constraint a + b = 5;
\end{mzn}
It is clear that when the value \mzninline{a} is known, then the value of
\mzninline{b} can be deduced. \gls{cp} is the idea solving \glspl{csp} by
performing an intelligent search by inferring which which values are still
feasible for each \gls{variable} \autocite{rossi-2006-cp}.
\begin{example}%
\label{ex:back-nqueens}
\begin{mzn}
int: n;
array [1..n] of var 1..n: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in 1..n]);
constraint all_different([q[i] - i | i in 1..n]);
\end{mzn}
\end{example}
\paragraph{Constraint Propagation}
\subsection{Mathematical Programming}%
\label{subsec:back-mip}
\glsreset{lp}
\glsreset{mip}
\gls{mip}
One of the oldest techniques to solve optimisation problems is the use of
\gls{lp} \autocite{schrijver-1998-mip}. A linear program describes a problem
using a set of linear equations over continuous variables. In general, a linear
program can be expressed in the form:
\begin{align*}
\text{maximise } & \sum_{j=1}^{V} c_{j} x_{j} & \\
\text{subject to } & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{i=1}^{C} \\
& x_{i} \in \mathbb{R} & \forall_{i=1}^{V}
\end{align*}
where \(V\) and \(C\) represent the number of variables and number of
constraints respectively. The vector \(c\) holds the coefficients of the
objective function and the matrix \(a\) holds the coefficients for the
constraints. The vectors \(l\) and \(u\) respectively contain the lower and
upper bounds of the constraints. Finally, the \glspl{variable} of the linear
program held in the \(x\) vector.
For problems that are in the form of a linear program, there are proven methods
to find the optimal solution. The most prominent method, the simplex method, can
find the optimal solution of a linear program in polynomial time.
The same method provides the foundation for a harder problem. In \gls{lp} our
variables must be continuous. If we require that one or more take a discrete
value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all}
\glspl{variable} must take a discrete value).
Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in
polynomial time. The general method to solve a mixed integer program is to treat
it as an linear program and find an optimal solution using the simplex method.
If the \glspl{variable} in the problem that are required to be discrete already
have discrete values, then we have found our optimal solution. Otherwise, we
pick one of the \glspl{variable}. For this \gls{variable} we create a version
of the linear program where it is less or equal to the value in the solution
rounded down to the nearest discrete value and a version where it is greater or
equal to the value in the solution rounded up. Both versions are solved to find
the best solution. The process is repeated recursively until a discrete solution
is found.
Much of the power of this solving method comes from bounds that can be inferred
during the process. The solution that the simplex provides an upper bound for
the solution in the current step of the solving process. Similarly, any discrete
solution found in an earlier branches of the search process provide a lower
bound. When the upper bound given by the simplex method is lower that the lower
bound from an earlier solution, then we know that any discrete solutions
following from the linear program will be strictly worse than the incumbent.
Over the years \gls{lp} and \gls{mip} \glspl{solver} have developed immensely.
\Glspl{solver}, such as CBC \autocite{}, CPLEX \autocite{}, Gurobi \autocite{},
and SCIP \autocite{}, can solve many complex problems. It is therefore often
worthwhile to encode problem as an mixed integer program to find a solution.
\glspl{csp} can be often be encoded as mixed integer programs. This does,
however, come with its challenges. Most \glspl{constraint} in a \minizinc\ model
are not linear equations. The translation of a single \gls{constraint} can
introduce many linear \glspl{constraint} and even new \glspl{variable}. For
example, when a \gls{constraint} reasons about the value that a variable will
take, to encode it we will need to introduce \glspl{indicator-var}. The
\glspl{indicator-var} \(y_{i}\) for a \gls{variable} \(x\) take the value 1 if
\(x = i\) and 0 otherwise. \Glspl{constraint} reasoning about the value of \(x\)
can then be rewritten as linear \glspl{constraint} using the \glspl{variable}
\(y_{i}\).
\begin{example}
Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. The
following model shows a integer program of this problem.
\begin{align}
\text{maximise } & 0 & \\
\text{subject to } & q_{i} \in \{1,\ldots{},n\} & \forall_{i=1}^{n} \\
& y_{ij} \in \{0,1\} & \forall_{i=1}^{n} \forall_{j=1}^{n} \\
\label{line:back-mip-channel} & x_{i} = \sum_{j=1}^{n} j * y_{ij} & \forall_{i=1}^{n} \\
\label{line:back-mip-row} & \sum_{i=1}^{n} y_{ij} \leq 1 & \forall_{j=1}^{n}
\end{align}
% & \sum_{j=1} y_{ij} \leq 1 & \forall_{i=1}^{n}\\
The encoding of this variable uses only integers. Like the \gls{cp} model,
integer \glspl{variable} \(q\) are used to represent where the queen is
located in each column. To encode the \mzninline{all_different} constraints,
the \glspl{indicator-var} \(y\) are inserted to reason about the value of
\(q\). The \cref{line:mip-channel} is used to connect the \(q\) and \(y\)
\glspl{variable} and make sure that their values correspond.
\Cref{line:back-mip-row} ensures that only one queen is placed in the same
row.
\jip{TODO: Fix diagonals}
\end{example}
\subsection{Boolean Satisfiability}%
\label{subsec:back-sat}
\glsreset{sat}
\glsreset{maxsat}
\gls{sat}
\gls{sat} was the first problem to be proven to be \gls{np-comp}
\autocite{cook-1971-sat}. The problem asks if there is an assignment for the
variables of a given Boolean formula, such that the formula is satisfied. This
problem can be seen as a restriction of the general \gls{csp} where
\glspl{variable} can only be of a Boolean type.
\subsection{Hybrid Technologies}%
\label{subsec:back-hybrid}
There is a field of research dedicated to solving \gls{sat} problems. In this
field a \gls{sat} problem is generally standardised to be in \gls{cnf}. A
\gls{cnf} is formulated in terms of Boolean literals. These are variables \(x\)
or their negations \(\neg x\). These literals are then used in a conjunction of
disjunctive clauses: a Boolean formula in the form
\(\forall_{i \in P} \exists_{b \in C_{i}} b\). To solve the \gls{sat} problem,
the \gls{solver} has to find an assignment for the \glspl{variable} where at
least one literal is true in every clause.
Even though the problem is proven to be hard to solve, a lot of progress has
been made towards solving even the biggest the most complex \gls{sat} problems
\autocite{biere-2021-sat}. Modern day \gls{sat} solvers can solve instances of
the problem with thousands of \glspl{variable} and clauses.
Many real world problems modelled in \cmls\ directly correspond to \gls{sat}.
However, even problems that contain \glspl{variable} with types other than
Boolean can often be encoded as a \gls{sat} problem. Depending of the problem,
using a \gls{sat} \glspl{solver} to solve the encoded problem can still be the
most efficient way to solve the problem.
\begin{example}
Consider the N-Queens problem presented in \cref{ex:back-nqueens}. A possible
\gls{sat} encoding for this problem is the following.
\begin{align}
\text{given } & n & \\
\text{find } & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i=1}^{n}\forall_{j=1}^{n} \\
\label{line:back-sat-at-least}\text{subject to } & \exists_{j=1}^{n} q_{ij} & \forall_{i=1}^{n} \\
\label{line:back-sat-row}& \neg q_{ij} \lor \neg q_{ik} & \forall_{i=1}^{n} \forall_{j=1}^{n} \forall_{k=j}^{n}\\
\label{line:back-sat-col}& \neg q_{ij} \lor \neg q_{kj} & \forall_{i=1}^{n} \forall_{j=1}^{n} \forall_{k=i}^{n}\\
\label{line:back-sat-diag1}& \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i=1}^{n} \forall_{j=1}^{n} \forall_{k=1}^{min(n-i, n-j)}\\
\label{line:back-sat-diag2}& \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i=1}^{n} \forall_{j=1}^{n} \forall_{k=1}^{min(n-i, j)}
\end{align}
The encoding of the problem uses a Boolean \gls{variable} for every position
of the chess board. Each \gls{variable} represents if a queen will be located
on this position or not. \Cref{line:back-sat-at-least} forces that a queen is
placed on every column of the chess board.
\Cref{line:back-sat-row,line:back-sat-col} ensure that only one queens is
place in each row and column respectively.
\Cref{line:back-sat-diag1,line:back-sat-diag2} similarly constrain each
diagonal to contain only one queen.
\end{example}
A variation on \gls{sat} is the \gls{maxsat} problem. Where in a \gls{sat}
problem all clauses need to be satisfied, this is not the case in a \gls{maxsat}
problem. Instead clauses are given individual weights. The higher the weight,
the more important the clause is for the overall problem. The goal in the
\gls{maxsat} problem is then to find a assignment for Boolean \glspl{variable}
that maximises the cumulative weights of the satisfied clauses.
The \gls{maxsat} problem is analogous to a \gls{cop}. Like a \gls{cop}, the aim
of \gls{maxsat} is to find the optimal solution to the problem. The difference
is that the weights are given to the \glspl{constraint} instead of the
\glspl{variable} or a function over them. It is, again, often possible to encode
a \gls{cop} as a \gls{maxsat} problem. A naive approach approach to encode an
integer objective is, for example, to encode each value in the domain as a
Boolean variable and assign that same value to a clause containing just that
Boolean variable.
For many problems the use of \gls{maxsat} \glspl{solver} can offer a very
successful method to find the optimal solution to a problem.
\section{Other Constraint Modelling Languages}%
\label{sec:back-other-languages}