Small adjustments

This commit is contained in:
Jip J. Dekker 2021-05-18 16:07:47 +10:00
parent 5b49833905
commit 369e21134e
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 109 additions and 43 deletions

View File

@ -287,6 +287,14 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @software{gecode-2021-gecode,
author = {{Gecode Team}}, author = {{Gecode Team}},
title = {Gecode: A Generic Constraint Development Environment}, title = {Gecode: A Generic Constraint Development Environment},
@ -396,6 +404,21 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @manual{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}}, author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual}, title = {Gurobi Optimizer Reference Manual},
@ -573,6 +596,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @book{marriott-1998-clp,
location = {Cambridge, Mass}, location = {Cambridge, Mass},
title = {Programming with constraints: an introduction}, title = {Programming with constraints: an introduction},
@ -586,17 +620,6 @@
programming}, 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, @article{marriott-2008-zinc,
author = {Kim Marriott and Nicholas Nethercote and Reza Rafeh and author = {Kim Marriott and Nicholas Nethercote and Reza Rafeh and
Peter J. Stuckey and Maria Garcia de la Banda and Mark Peter J. Stuckey and Maria Garcia de la Banda and Mark
@ -704,6 +727,16 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @inproceedings{rendl-2009-enhanced-tailoring,
author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher
Jefferson}, Jefferson},
@ -785,6 +818,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @book{schrijver-1998-mip,
title = {Theory of Linear and Integer Programming}, title = {Theory of Linear and Integer Programming},
author = {Schrijver, A.}, author = {Schrijver, A.},
@ -812,17 +856,6 @@
bibsource = {dblp computer science bibliography, https://dblp.org} 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, @inproceedings{schulte-2000-deep,
author = {Christian Schulte}, author = {Christian Schulte},
editor = {Enrico Pontelli and V{\'{\i}}tor Santos Costa}, editor = {Enrico Pontelli and V{\'{\i}}tor Santos Costa},
@ -1015,23 +1048,6 @@
combinatorial optimization} 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, @software{forrest-2020-cbc,
author = {Forrest, J. and author = {Forrest, J. and
Stefan Vigerske and Stefan Vigerske and
@ -1055,6 +1071,39 @@
url = {https://doi.org/10.5281/zenodo.3700700} 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, @book{wolsey-1988-mip,
title = {Integer and Combinatorial Optimization}, title = {Integer and Combinatorial Optimization},
author = {Wolsey, L.A. and Nemhauser, G.L.}, author = {Wolsey, L.A. and Nemhauser, G.L.},

View File

@ -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 search decision. Furthermore, because propagation is performed to a
\gls{fixpoint}, it is guaranteed that no duplicate propagation is required. \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}% \begin{example}%
\label{ex:back-nqueens} \label{ex:back-nqueens}
Consider as an example the N-Queens problem. Given a chess board of size 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 \(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 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} \begin{mzn}
int: n; 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 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. 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 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 When solving the problem, initially no values can be eliminated from the
\glspl{domain} of the \glspl{variable}. The first propagation will happen when \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 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. 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}% \subsection{Mathematical Programming}%
\label{subsec:back-mip} \label{subsec:back-mip}
\glsreset{lp} \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 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 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 \autocite{biere-2021-sat}. Modern day \gls{sat} solvers, like Kissat
the problem with thousands of \glspl{variable} and clauses. \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}. Many real world problems modelled in \cmls\ directly correspond to \gls{sat}.
However, even problems that contain \glspl{variable} with types other than However, even problems that contain \glspl{variable} with types other than