From 3d172bc06cc6781d83eca28a57f5c36945b9b496 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 16 Jun 2021 15:43:49 +1000 Subject: [PATCH] Add initial number of the SAT half-reification statistics --- assets/table/half_flat_sat.tex | 11 +++++++++++ assets/table/half_mznc.tex | 3 +++ chapters/4_half_reif.tex | 36 +++++++++++++++++++++++----------- 3 files changed, 39 insertions(+), 11 deletions(-) create mode 100644 assets/table/half_flat_sat.tex diff --git a/assets/table/half_flat_sat.tex b/assets/table/half_flat_sat.tex new file mode 100644 index 0000000..5cf53fa --- /dev/null +++ b/assets/table/half_flat_sat.tex @@ -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} diff --git a/assets/table/half_mznc.tex b/assets/table/half_mznc.tex index 504fec5..2b9ef53 100644 --- a/assets/table/half_mznc.tex +++ b/assets/table/half_mznc.tex @@ -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} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index a3dc402..7d9f41a 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -882,16 +882,18 @@ 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} - \end{subtable} - \begin{subtable}[b]{\linewidth} - \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_gecode} + \caption{\label{subtab:half-flat-gecode}\gls{gecode} library} + \end{subtable} + \begin{subtable}[b]{\linewidth} + \input{assets/table/half_flat_linear} + \caption{\label{subtab:half-flat-lin}Linearisation library} + \end{subtable} + \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}