Push down negation before decompose#916
Open
IgnaceBleukx wants to merge 22 commits into
Open
Conversation
Collaborator
|
you will have to rebase/merge master in I guess, now that push down negation rewrite is in (in a different form) |
tias
reviewed
May 7, 2026
Collaborator
tias
left a comment
There was a problem hiding this comment.
almost there.
I guess you checked that no global cons/func introduces a negation, even on the latest master?
Also, we since have 'scip' as a solver, can you check that all solvers on master that need changing are changed?
Collaborator
Author
|
Processed the review, there were indeed a couple of cases where the decomposition/negation of a global might introduce negation. Updated scip and docs |
Collaborator
Author
|
Also updated the newly added highs solver, should be ready to go in after tests complete? |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Re-order the transformations such that negation is pushed down into the arguments of a "not" operator before we call decompose.
This allows to implement efficient implementations of negated global constraints (e.g.,
~Tablebecomes Negtable).We can also do this for some more (e.g., ~AllDiff(x) becomes NValue(x) < len(x)). We should probably do some small experiments to see what is more efficient? Also depends on the decomp of NValue of course if that one is not supported...
Downside is that no transformation can explicitly introduce negation, and needs to call
recurse_negationthemself. This turned out to be simpler to implement than I first thought.Efficiency-wise, there might be some gains because we now have one transformation less to be called in each recursive
flatten_constraintcall. I then also noticed we call simplify_boolean in each recursive flatten call, I've added a flag to disable it when we can. Not sure if this should remain in this PR