Skip to content

NoOverlapOptional and CumulativeOptional mapping to MiniZinc - #1083

Open
WoutPiessens wants to merge 9 commits into
masterfrom
fix/966-optional-globals-minizinc
Open

WoutPiessens wants to merge 9 commits into
masterfrom
fix/966-optional-globals-minizinc

Conversation

@WoutPiessens

Copy link
Copy Markdown
Collaborator

This PR addresses the two global constraints left in #966: NoOverlapOptional and CumulativeOptional, which were not yet mapped to the MiniZinc interface. Similar to the mappings for NoOverlap and Cumulative respectively, except for the necessary changes for optional tasks.

@IgnaceBleukx IgnaceBleukx left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can use a bunch more minizinc features actually, so you don't have to manually handle all of the opt-stuff : )

Comment thread tests/test_globalconstraints.py Resolved
Comment thread cpmpy/solvers/minizinc.py Resolved
Comment thread cpmpy/solvers/minizinc.py Outdated

# absent tasks consume no resources
demand_str = "[{}]".format(",".join(
"if {} then {} else 0 endif".format(self._convert_expression(p), self._convert_expression(d))

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not actually required, minizinc handles this themself.
The only difference between the non-optional cumulative and the optinonal one should be the array of start vars (it does get some getting used to)
https://docs.minizinc.dev/en/2.9.3/lib-globals-scheduling.html#mzn-ref-globals-scheduling-cumulative

The starts become optional integers, which you can do just using an if statement

[s | i, s in enumerate(_convert_expression(start)) if is_present[i]]

I forgot what the exact minizinc-equivalent is of enumerate(start) but you get the point : )

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes that's better, also more similar to NoOverlapOptional that way. I'll also use the same syntax as NoOverlapOptional, for the same reason as discussed in that comment

@IgnaceBleukx

Copy link
Copy Markdown
Collaborator

Lets first determine what we do with #1103, we might need to change to disjunctive_strict here as well

@WoutPiessens

Copy link
Copy Markdown
Collaborator Author

Because we decided on non-strict semantics in all cases (see #1105), this PR already respects the desired semantics.

@IgnaceBleukx

Copy link
Copy Markdown
Collaborator

Merged current master in this one with the new tests for nooverlap and cumulative. There two tests failing locally on my macine

@WoutPiessens

Copy link
Copy Markdown
Collaborator Author

It seems to have something to do with an inconsistency in how Gecode handles CumulativeOptional. It seems that Gecode has the strict semantics here, unlike Chuffed and CP-SAT. We can just hard code in our transformation that zero-duration tasks are always inactive to fix it. But I'll try to understand a bit better what's happening exactly first.

@WoutPiessens

Copy link
Copy Markdown
Collaborator Author

Under certain conditions, MiniZinc’s cumulative_optional global can fall back to Gecode’s native cumulative_optional, which uses strict semantics. Because zero-duration tasks are not treated consistently, a preventive fix is to treat zero-duration tasks as inactive.

@IgnaceBleukx

Copy link
Copy Markdown
Collaborator

This seems to be a MiniZinc issue then, so we should tell them : )
Can you find the exact cases where it falls back to the strict semantics?

@WoutPiessens

Copy link
Copy Markdown
Collaborator Author

The following code (minizinc/gecode/fzn_cumulative_opt.mzn) decides in which case it's delegated to the native cumulative_optional, so it happens when durations, usages and capacity are fixed. That's indeed the case for the two tests that were previously failing.

predicate gecode_schedule_cumulative_optional(array[int] of var int: start,
  array[int] of int: duration, array[int] of int: usage,
  array[int] of var bool: m, int: capacity);

predicate fzn_cumulative_opt(array[int] of var opt int: s,
                     array[int] of var int: d,
                     array[int] of var int: r, var int: b) =
    if
        forall (i in index_set(d)) (is_fixed(d[i])) /\
        forall (i in index_set(r)) (is_fixed(r[i])) /\
        is_fixed(b)
    then
        gecode_schedule_cumulative_optional(
            [ if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s ],
            [ fix(di) | di in d ],
            [ fix(ri) | ri in r ],
            [ occurs(si) | si in s ],
            fix(b)
        )
    else
        fzn_cumulative_opt_decomp(s,d,r,b)
    endif;

The reason why disjunctive_optional doesn't have the same issue is because there is no native Gecode override. The default decomposition respects the non-strict semantics, just like for cumulative_optional.

On which repo should we open an issue for this?

@IgnaceBleukx

Copy link
Copy Markdown
Collaborator

Ok good, you can open an issue at https://github.com/MiniZinc/libminizinc with an example model and the expected output.
Best to also reference this issue so we can easily track when its resolved upstream : )

@WoutPiessens

Copy link
Copy Markdown
Collaborator Author

Issue opened: MiniZinc/libminizinc#1070

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants