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

Update half reification chapter with SAT experiment numbers

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-19 18:26:51 +10:00
parent 81a5efb646
commit 80b32f11e7
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
6 changed files with 54 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
assets/bibliography/references.bib
View File

@ -353,6 +353,21 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{fischetti-2014-erratiscism,
author = {Matteo Fischetti and Michele Monaci},
title = {Exploiting Erraticism in Search},
journal = {Oper. Res.},
volume = {62},
number = {1},
pages = {114--122},
year = {2014},
url = {https://doi.org/10.1287/opre.2013.1231},
doi = {10.1287/opre.2013.1231},
timestamp = {Tue, 31 Mar 2020 18:17:39 +0200},
biburl = {https://dblp.org/rec/journals/ior/FischettiM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@software{forrest-2020-cbc,
author = {Forrest, J. and Stefan Vigerske and Haroldo Gambini Santos and Ted
Ralphs and Lou Hafer and Bjarni Kristjansson and Fasano, J.P. and

11
assets/glossary.tex
View File

@ -68,6 +68,12 @@
description={A set of instructions designed to be efficiently executed by an \gls{interpreter}. Distinctive from other computer languages a byte code has a very compact representation, \eg{} using only numbers, and can not be directly read by humans},
}
\newglossaryentry{booleanisation}{
name={Booleanisation},
description={The process of \gls{rewriting} a \gls{model} to a \gls{sat} or \gls{maxsat} problem},
}
\newglossaryentry{bounds-con}{
name={bounds consistent},
description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied},
@ -404,6 +410,11 @@
description={A function defined over the \glspl{variable} of a \gls{model} to assign a numeric value to the quality of the \gls{sol}},
}
\newglossaryentry{openwbo}{
name={OpenWBO},
description={A well-known \gls{maxsat} \gls{solver} \autocite{martins-2014-openwbo}},
}
\newglossaryentry{operator}{
name={operator},
description={A syntactical symbol used as a shorthand for a function. Prefix operators, such as \mzninline{not}, appear before another expression and are a shorthand for unary functions. Infix operators, such as \mzninline{+}, \mzninline{*}, and \mzninline{div}, appear in between two expressions and are a shorthand for binary functions},

14
assets/table/half_flat_sat.tex
View File

@ -1,11 +1,11 @@
\begin{tabular}{llll}
\begin{tabular}{lrrr}
\toprule
& Full Reification & \multicolumn{2}{l}{Half Reification} \\
& Full Reification & Half Reification & \\
\midrule
Constraints & 11,351,946 & 10,959,348 & (-3.46\%) \\
Reifications & 552,928 & 357,022 & (-35.43\%) \\
Half Reifications & 171,258 & 281,655 & \\
Implications Removed & 0 & 0 & \\
Rewriting Time & 1586s & 1583s & (-0.18\%) \\
Constraints & 68,652,864 & 68,111,741 & (-0.79\%) \\
Reifications & 2,903,542 & 2,557,830 & (-11.91\%) \\
Half Reifications & 694,276 & 856,364 & \\
Implications Removed & 0 & 182 & \\
Rewriting Time & 6,030s & 5,926s & (-1.28\%) \\
\bottomrule
\end{tabular}

4
assets/table/half_mznc.tex
View File

@ -11,7 +11,7 @@
\gls{cbc} & (Full) & 2 & (11.94s) & 41 & (131.76s) & 131 & 16 & 10 \\
\gls{cbc} & (Half) & 2 & (7.01s) & 35 & (135.93s) & 135 & 17 & 11 \\
\midrule
OpenWBO & (Full) & 4 & (2.95s) & 29 & (199.27s) & 29 & 13 & 25 \\
OpenWBO & (Half) & 4 & (3.04s) & 30 & (202.70s) & 28 & 13 & 25 \\
OpenWBO & (Full) & 16 & (20.44s) & 48 & (156.01s) & 51 & 32 & 53 \\
OpenWBO & (Half) & 16 & (19.61s) & 51 & (187.73s) & 47 & 33 & 53 \\
\bottomrule
\end{tabular}

1
chapters/2_background.tex
View File

@ -791,6 +791,7 @@ Modern day \gls{sat} solvers, like Clasp \autocite{gebser-2012-clasp}, Kissat \a
Many real world problems modelled using \cmls{} directly correspond to \gls{sat}.
However, even problems that contain \variables{} with types other than Boolean can still be encoded as a \gls{sat} problem.
This process is known as \gls{booleanisation}.
Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem can still be the most efficient way to solve the problem.
\begin{example}

35
chapters/4_half_reif.tex
View File

@ -947,12 +947,11 @@ In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to
The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate the usage of \gls{half-reif} on a larger scale.
In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearisation} library, which has been adapted to use \gls{half-reif} as earlier described.
These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearisation} and \gls{booleanisation} libraries, which has been adapted to use \gls{half-reif} as earlier described.
The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable the usage of \gls{half-reif}.
The solving of the linearised \instances{} is tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
\todo{TODO:\ Extend this section with the \gls{sat} results once they are run.}
The solving of the linearised \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
The solving of the Booleanised \instances are testing using the \gls{openwbo} \solver{}.
is
\begin{table}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_gecode}
@ -960,11 +959,11 @@ The solving of the linearised \instances{} is tested using the \gls{cbc} and \gl
\end{subtable}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_linear}
\caption{\label{subtab:half-flat-lin}Linearisation library}
\caption{\label{subtab:half-flat-lin}\Gls{linearisation} library}
\end{subtable}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_sat}
\caption{\label{subtab:half-flat-bool}Booleanisation library}
\caption{\label{subtab:half-flat-bool}\Gls{booleanisation} library}
\end{subtable}
\caption{\label{tab:half-rewrite} Cumulative statistics of \gls{rewriting} all \minizinc{} \instances{} from \minizinc{} challenge 2019 \& 2020 (200 \instances{}).}
\end{table}
@ -996,15 +995,15 @@ Similar to \gls{gecode}, the number of implications that is removed is dependent
Lastly, the \gls{rewriting} time slightly increases for the linearisation process.
Since there are many more \constraints{}, the introduced optimisation mechanisms have an slightly higher overhead.
\todo{The \gls{sat} statistics currently only include 2019. 2020 is still WIP.}
Finally, statistics for the \gls{rewriting} the instances is shown in \cref{subtab:half-flat-bool}.
Like linearisation, the usage of \gls{half-reif} significantly reduces number of \constraints{} and \glspl{reif}.
Different, however, is that the booleanisation library is explicitly defined in terms of \glspl{half-reif}.
Finally, statistics for the \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} is shown in \cref{subtab:half-flat-bool}.
Unlike linearisation, the usage of \gls{half-reif} does not significantly reduces number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
We also see that that the \gls{booleanisation} library is explicitly defined in terms of \glspl{half-reif}.
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}.
Furthermore, the usage of \gls{chain-compression} does not seem to have any effect.
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into bigger clauses.
Surprisingly, the usage of \gls{half-reif} also reduces the \gls{rewriting} time as it reduces the workload.
Surprisingly, the usage of \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
The relatively small changes shown might indicate that additional work is required to correctly annotate predicates and functions in the Booleanisation library.
\begin{table}
\input{assets/table/half_mznc}
@ -1040,11 +1039,13 @@ In general, we would expect the reduction of \constraints{} in a \gls{mip} insta
However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver.
An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance.
Some patterns can only be detected when using a full \gls{reif}.
Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given.
\todo{Is there a citation for this?} With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given \autocite{fischetti-2014-erratiscism}.
With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
\todo{\gls{sat} number are still preliminary, but look optimistic.
Only one case where the solver time is severely impacted.}
The solving statistics for \gls{openwbo} might be most positive.
Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}.
It negatively impacts one \instance{}, that no longer finds any \gls{sol}.
That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change.
% \section{Summary}
% \label{sec:half-summary}