diff --git a/chapters/6_incremental.tex b/chapters/6_incremental.tex index 16b60ba..209269b 100644 --- a/chapters/6_incremental.tex +++ b/chapters/6_incremental.tex @@ -366,10 +366,31 @@ on. We can model this strategy restarts as such: \highlightfile{assets/mzn/6_lex_minimize.mzn} -Another optimisation +The lexicographic objective changes the objective at each stage in the +evaluation. Initially the stage is 1. Otherwise is we have an UNSAT result, then +the last stage has been completed (proved optimal). We increase the stage by one +if we have stages to go otherwise we finish. Otherwise if the last all was SAT +we maintain the same stage, and store the objective value (for this stage) in +the \mzninline{best} array. For normal computation we fix all the earlier stage +variables to their best value. If we are not in the first run for a stage we add +the branch and bound cut to try to find better solutions. Finally we set the +objective to be the objective for the current stage. + +There is not always a clear order of importance for different objectives in a +problem. In these cases we might instead look for a number of diverse solutions +and allow the user to pick the most acceptable options. The following fragment +shows a \gls{meta-search} for the pareto optimality of a pair of objectives: \highlightfile{assets/mzn/6_pareto_optimal.mzn} +In this implementation we keep track of the number of solutions found so far +using \mzninline{nsol}. There is a maximum number we can handle +(\mzninline{ms}). At the start the number of solutions is 0. If we find no +solutions we finish the entire search. Otherwise we record that we have one more +solution. We store the solution values in \mzninline{s1} and \mzninline{s2} +arrays. Before each restart we add constraints removing pareto dominated +solutions, based on each previous solution. + \section{Compilation of Meta-Search Specifications} \label{sec:6-solver-extension}