From 369e21134e0933c78d2bef79debd0e3cd523f271 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 18 May 2021 16:07:47 +1000 Subject: [PATCH] Small adjustments --- assets/bibliography/references.bib | 127 ++++++++++++++++++++--------- chapters/2_background.tex | 25 +++++- 2 files changed, 109 insertions(+), 43 deletions(-) diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index ef228c8..03fca83 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -287,6 +287,14 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@software{chuffed-2021-chuffed, + author = {Geoffrey Chu and Peter J. Stuckey and Andreas Schutt and Thorsten Ehlers and Graeme Gange and Kathryn Francis}, + title = {Chuffed, a lazy clause generation solver}, + year = 2021, + url = {https://github.com/chuffed/chuffed}, + version = {0.10.3}, +} + @software{gecode-2021-gecode, author = {{Gecode Team}}, title = {Gecode: A Generic Constraint Development Environment}, @@ -396,6 +404,21 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{gebser-2012-clasp, + author = {Martin Gebser and Benjamin Kaufmann and Torsten Schaub}, + title = {Conflict-driven answer set solving: From theory to + practice}, + journal = {Artif. Intell.}, + volume = 187, + pages = {52--89}, + year = 2012, + url = {https://doi.org/10.1016/j.artint.2012.04.001}, + doi = {10.1016/j.artint.2012.04.001}, + timestamp = {Fri, 09 Apr 2021 18:34:15 +0200}, + biburl = {https://dblp.org/rec/journals/ai/GebserKS12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @manual{gurobi-2021-gurobi, author = {{Gurobi Optimization, LLC}}, title = {Gurobi Optimizer Reference Manual}, @@ -573,6 +596,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} +} + @book{marriott-1998-clp, location = {Cambridge, Mass}, title = {Programming with constraints: an introduction}, @@ -586,17 +620,6 @@ programming}, } -@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} -} - @article{marriott-2008-zinc, author = {Kim Marriott and Nicholas Nethercote and Reza Rafeh and Peter J. Stuckey and Maria Garcia de la Banda and Mark @@ -704,6 +727,16 @@ bibsource = {dblp computer science bibliography, https://dblp.org} } +@manual{prudhomme-2016-choco, + author = {Charles Prud'homme and Jean-Guillaume Fages and Xavier + Lorca}, + title = {Choco Solver Documentation}, + year = 2016, + organization = {TASC, INRIA Rennes, LINA CNRS UMR 6241, COSLING S.A.S.}, + timestamp = {Tue, 9 Feb 2016}, + url = {http://www.choco-solver.org }, +} + @inproceedings{rendl-2009-enhanced-tailoring, author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher Jefferson}, @@ -785,6 +818,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} +} + @book{schrijver-1998-mip, title = {Theory of Linear and Integer Programming}, author = {Schrijver, A.}, @@ -812,17 +856,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} -} - @inproceedings{schulte-2000-deep, author = {Christian Schulte}, editor = {Enrico Pontelli and V{\'{\i}}tor Santos Costa}, @@ -1015,23 +1048,6 @@ combinatorial optimization} } -@book{wallis-2011-combinatorics, - title = {Introduction to Combinatorics}, - author = {Wallis, W.D. and George, J.}, - isbn = 9781439806234, - series = {Discrete Mathematics and Its Applications}, - year = 2011, - publisher = {Taylor \& Francis} -} - -@article{warren-1983-wam, - title = {An abstract Prolog instruction set}, - author = {Warren, David HD}, - journal = {Technical note 309}, - year = 1983, - publisher = {SRI International} -} - @software{forrest-2020-cbc, author = {Forrest, J. and Stefan Vigerske and @@ -1055,6 +1071,39 @@ url = {https://doi.org/10.5281/zenodo.3700700} } +@book{wallis-2011-combinatorics, + title = {Introduction to Combinatorics}, + author = {Wallis, W.D. and George, J.}, + isbn = 9781439806234, + series = {Discrete Mathematics and Its Applications}, + year = 2011, + publisher = {Taylor \& Francis} +} + +@software{perron-2021-ortools, + title = {OR-Tools}, + version = {9.0}, + author = {Laurent Perron and Vincent Furnon}, + organization = {Google}, + url = {https://developers.google.com/optimization/}, + date = {2021-04-30} +} + +@article{warren-1983-wam, + title = {An abstract Prolog instruction set}, + author = {Warren, David HD}, + journal = {Technical note 309}, + year = 1983, + publisher = {SRI International} +} + +@software{biere-2021-kissat, + title = {Kissat}, + version = {2021}, + author = {Armin Biere}, + url = {http://fmv.jku.at/kissat/}, +} + @book{wolsey-1988-mip, title = {Integer and Combinatorial Optimization}, author = {Wolsey, L.A. and Nemhauser, G.L.}, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index feb5d7d..8ba30dd 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -677,12 +677,23 @@ was made, it is guaranteed that these \gls{domain} changes do not depend on the search decision. Furthermore, because propagation is performed to a \gls{fixpoint}, it is guaranteed that no duplicate propagation is required. +The solving method used by \gls{cp} \glspl{solver} is very flexible. A +\gls{solver} can support many different types of \glspl{variable}: they can +range from Boolean, floating point numbers, and integers, to intervals, sets, +and functions. Similarly, \glspl{solver} do not all have access to the same +propagators. Therefore, a \gls{csp} modelled for one \gls{solver} might look +very different to an equivalent \gls{csp} modelled for a different solver. +Instead, \cmls{}, like \minizinc{}, can serve as a standardised form of input +for these \glspl{solver}. They allow modellers to use high-level constraints +that are used directly by the solver when supported or they are automatically +translated to a collection of equivalent supported constraints otherwise. + \begin{example}% \label{ex:back-nqueens} Consider as an example the N-Queens problem. Given a chess board of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another. Meaning only one queen per row, one queen per column, and -one queen per diagonal. The problem can be modelled as a \gls{csp} as follows. +one queen per diagonal. The problem can be modelled in \minizinc\ as follows. \begin{mzn} int: n; @@ -699,7 +710,7 @@ The \glspl{constraint} in the model model the remaining rules of the problem: no two queen can be placed in the same row, no two queen can be place in the same upward diagonal, and no two queens can be place in the same downward diagonal. This model can be directly used in most \gls{cp} \glspl{solver}, since integer -\glspl{variable} and a \gls{propagator} are common. +\glspl{variable} and an \mzninline{all_different} \gls{propagator} are common. When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \glspl{variable}. The first propagation will happen when @@ -750,6 +761,11 @@ another solution, then the incumbent solution is updated and the search process continues. If the search process does not find any other solutions, then it is proven that there are no better solutions than the current incumbent solution. +\gls{cp} solvers like Chuffed \autocite{chuffed-2021-chuffed}, Choco +\autocite{prudhomme-2016-choco}, Gecode \autocite{gecode-2021-gecode}, and +OR-Tools \autocite{perron-2021-ortools} have long been one of the leading method +to solve \minizinc\ instances. + \subsection{Mathematical Programming}% \label{subsec:back-mip} \glsreset{lp} @@ -870,8 +886,9 @@ 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. +\autocite{biere-2021-sat}. Modern day \gls{sat} solvers, like Kissat +\autocite{biere-2021-kissat} and Clasp \autocite{gebser-2012-clasp}, 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