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

Update lexicographic_minimize definition

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-09 13:32:31 +10:00
parent 3a623816c8
commit 8f6d5f1835
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 17 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
chapters/5_incremental.tex
View File

@ -207,28 +207,20 @@ We can model this strategy restarts as such:
\begin{mzn} \begin{mzn}
predicate lex_minimize(array[int] of var int: o) = predicate lex_minimize(array[int] of var int: o) =
let { let {
var index_set(o): stage var min(index_set(o))..max(index_set(o))+1: stage;
array[index_set(o)] of var int: best;
} in if status() = START then } in if status() = START then
stage = min(index_set(o)) stage = min(index_set(o))
else elseif status() = UNSAT then
if status() = UNSAT then
if lastval(stage) < l then
stage = lastval(stage) + 1 stage = lastval(stage) + 1
else else /* status() = SAT */
complete() % we are finished
endif
else
stage = lastval(stage) stage = lastval(stage)
/\ best[stage] = sol(_objective) /\ o[stage] < sol(o[stage])
endif endif
/\ for(i in min(index_set(o))..stage-1) ( /\ forall(i in min(index_set(o))..stage-1) (
o[i] = lastval(best[i]) o[i] = sol(o[i])
) )
/\ if status() = SAT then /\ if stage > max(index_set(o)) then
o[stage] < sol(_objective) complete()
endif
/\ _objective = o[stage]
endif; endif;
\end{mzn} \end{mzn}