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

Add initial number of the SAT half-reification statistics

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-16 15:43:49 +10:00
parent d4d53c488b
commit 3d172bc06c
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 39 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
assets/table/half_flat_sat.tex Normal file
View File

@ -0,0 +1,11 @@
\begin{tabular}{lrrr}
\toprule
& Full Reification & \multicolumn{2}{l}{Half Reification} \\
\midrule
Constraints & 7,654,088 & 7,310,851 & (-4.48\%) \\
Reifications & 433,761 & 263,386 & (-39.28\%) \\
Half Reifications & 42,228 & 178,984 & \\
Implications Removed & 0 & 0 & \\
Flattening Time & 614s & 604s & (-1.76\%) \\
\bottomrule
\end{tabular}

3
assets/table/half_mznc.tex
View File

@ -10,5 +10,8 @@
\midrule
\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) & 7 & (148.67s) & 28 & (150.36s) & 25 & 15 & 20 \\
OpenWBO & (Half) & 7 & (100.30s) & 29 & (187.98s) & 24 & 15 & 20 \\
\bottomrule
\end{tabular}

20
chapters/4_half_reif.tex
View File

@ -882,7 +882,6 @@ The solving of the linearised models is tested using the \gls{cbc} and \gls{cple
\jip{TODO:\ Extend this section with the \gls{sat} results once they are run.}
\begin{table}
\begin{center}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_gecode}
\caption{\label{subtab:half-flat-gecode}\gls{gecode} library}
@ -891,7 +890,10 @@ The solving of the linearised models is tested using the \gls{cbc} and \gls{cple
\input{assets/table/half_flat_linear}
\caption{\label{subtab:half-flat-lin}Linearisation library}
\end{subtable}
\end{center}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_sat}
\caption{\label{subtab:half-flat-bool}Booleanisation library}
\end{subtable}
\caption{\label{tab:half-flattening} Cumulative statistics of flattening all \minizinc{} instances from \minizinc{} Challenge 2019 \& 2020 (200 instances).}
\end{table}
@ -915,7 +917,7 @@ This replacement happens mostly 1-for-1; the difference between the number of \g
In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced.
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimisation techniques is minimal.
The figure \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearisation.
The \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearisation.
Since both \glspl{reification} and \glspl{half-reif} are decomposed during the flattening process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall constraints.
The ratio of \glspl{reification} that is replaced with \glspl{half-reif} is not as high as \gls{gecode}.
This is caused by the fact that the linearisation process requires full \gls{reification} in the decomposition of many \gls{global} \constraints{}.
@ -923,6 +925,15 @@ Similar to \gls{gecode}, the number of implications that is removed is dependent
Lastly, the flattening time slightly increases for the linearisation process.
Since there are many more constraints, the introduced optimisation mechanisms have an slightly higher overhead.
\jip{TODO:\ The \gls{sat} statistics currently only include 2019. 2020 is still WIP.}
Finally, statistics for the flattening 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{reification}.
Different, however, is that the booleanisation library is explicitly defined in terms of \glspl{half-reif}.Some constraints might manually introduce \mzninline{_imp} call as part of their definition.
Furthermore, the usage of 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 chain compression are instead aggregated into bigger clauses.
Surprisingly, the usage of \gls{half-reif} also reduces the flattening time as it reduces the workload.
\begin{table}
\input{assets/table/half_mznc}
\caption{\label{tab:half-mznc} Status overview of solving \minizinc{} Challenge 2019 \& 2020 with and without \gls{half-reif}.}
@ -960,5 +971,8 @@ Some patterns might only be detected when using a full \gls{reification}.
Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the constraints are given.
\jip{TODO:\ Is there a citation for this?} With the usage of the \constraint{} \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
\jip{TODO: \gls{sat} number are still preliminary, but look optimistic.
Only one case where the solver time is severely impacted.}
% \section{Summary}
% \label{sec:half-summary}