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

Mention specific maxsat solvers and version used

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-26 13:13:32 +10:00
parent 062941712c
commit 205b25d74b
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 19 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
assets/bibliography/references.bib
View File

@ -588,6 +588,23 @@
year = 2020, year = 2020,
} }
@article{ignatiev-2019-rc2,
title = {RC2: an Efficient MaxSAT Solver},
keywords = {Maximum Satis ability, Relaxable/Soft Cardinality Constraints,
Python},
author = {Alexey Ignatiev and Antonio Morgado and Joao Marques-Silva},
year = 2019,
month = 9,
day = 1,
language = {English},
volume = {11},
pages = {53--64},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
issn = {1574-0617},
publisher = {IOS Press},
number = 1,
}
@inproceedings{ingmar-2020-diverse, @inproceedings{ingmar-2020-diverse,
author = {Linnea Ingmar and Maria Garcia de la Banda and Peter J. Stuckey and author = {Linnea Ingmar and Maria Garcia de la Banda and Peter J. Stuckey and
Guido Tack}, Guido Tack},

2
chapters/2_background.tex
View File

@ -841,7 +841,7 @@ It is, again, possible to rewrite a \cmodel{} with an \gls{objective} as a \gls{
A naive approach to encode an integer objective is, for example, to encode each possible result of the \gls{objective} as a Boolean \variable{}. A naive approach to encode an integer objective is, for example, to encode each possible result of the \gls{objective} as a Boolean \variable{}.
This Boolean \variable{} then forms a singleton clause with the result value as its weight. This Boolean \variable{} then forms a singleton clause with the result value as its weight.
For many problems the use of \gls{maxsat} \solvers{} offers a very successful method to find an \gls{opt-sol} to a problem. For many problems the use of \gls{maxsat} \solvers{}, such as \gls{openwbo} \autocite{martins-2014-openwbo} and RC2 \autocite{ignatiev-2019-rc2}, offers a very successful method to find an \gls{opt-sol} to a problem.
\section{Constraint Modelling Languages}% \section{Constraint Modelling Languages}%
\label{sec:back-other-languages} \label{sec:back-other-languages}

2
chapters/A2_benchmark.tex
View File

@ -145,7 +145,7 @@ In this thesis we use four different versions of the \gls{gecode} solver:
In this thesis we use \gls{cplex} version 20.1 under an academic licence in our experiments. In this thesis we use \gls{cplex} version 20.1 under an academic licence in our experiments.
\paragraph{OpenWBO} is an open source \gls{maxsat} \solver{} \autocite{martins-2014-openwbo}. \paragraph{OpenWBO} is an open source \gls{maxsat} \solver{} \autocite{martins-2014-openwbo}.
In this thesis we use version \todo{xxx} in our experiments. In this thesis we use version 2.1 in our experiments.
The source code for this version can be found here: The source code for this version can be found here:
\begin{center} \begin{center}