diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 03aa235..7955c51 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -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 diff --git a/assets/glossary.tex b/assets/glossary.tex index 42f2a3a..9deef15 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -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}, diff --git a/assets/table/half_flat_sat.tex b/assets/table/half_flat_sat.tex index 908fa96..a4a6495 100644 --- a/assets/table/half_flat_sat.tex +++ b/assets/table/half_flat_sat.tex @@ -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} diff --git a/assets/table/half_mznc.tex b/assets/table/half_mznc.tex index 7d0938a..0687df6 100644 --- a/assets/table/half_mznc.tex +++ b/assets/table/half_mznc.tex @@ -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} diff --git a/chapters/2_background.tex b/chapters/2_background.tex index df68b9a..3189c52 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -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} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 504cbea..59fdc36 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -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}