Context provided to lazy reason calculation can be inconsistent #25
Labels
bug
Something isn't working
Comments
maartenflippo
pushed a commit
that referenced
this issue
Sep 9, 2024
…on (#24) There were 2 mistakes in the not equal propagator: - The notify method checks whether the context is fixed before updating the number of fixed variables; this could be wrong due to the notification taking place after backtracking. Removing this check fixes this issue - The `unfixed_variable_has_been_updated` was wrongly set to true if no update took place; it could be argued that the variable should be true but then we do not currently detect the case when this value becomes part of the domain again (which could be due to a bound update). This issue was fixed by only setting this variable if the propagator removes the variable. Additionally, oftentimes the propagators assume that they first get notified of all the "forward" events (i.e. tightening of the bounds/removals/assignments) and then of the backtrack events. This issue is now fixed by first processing the "forward" events when notifying the propagators of the backtrack events. **Update** This PR also addresses the issue mentioned in #25 by eagerly calculating the reason rather than relying on the context during lazy reason computation.
ImkoMarijnissen
added a commit
that referenced
this issue
Sep 12, 2024
…on (#24) There were 2 mistakes in the not equal propagator: - The notify method checks whether the context is fixed before updating the number of fixed variables; this could be wrong due to the notification taking place after backtracking. Removing this check fixes this issue - The `unfixed_variable_has_been_updated` was wrongly set to true if no update took place; it could be argued that the variable should be true but then we do not currently detect the case when this value becomes part of the domain again (which could be due to a bound update). This issue was fixed by only setting this variable if the propagator removes the variable. Additionally, oftentimes the propagators assume that they first get notified of all the "forward" events (i.e. tightening of the bounds/removals/assignments) and then of the backtrack events. This issue is now fixed by first processing the "forward" events when notifying the propagators of the backtrack events. **Update** This PR also addresses the issue mentioned in #25 by eagerly calculating the reason rather than relying on the context during lazy reason computation.
maartenflippo
pushed a commit
that referenced
this issue
Sep 13, 2024
We thought that we could use a lazy reason for explaining the not equals constraint but we did not fix the underlying problem mentioned in #25 . This PR reverts to eager reason calculation!
ImkoMarijnissen
added a commit
that referenced
this issue
Nov 8, 2024
We thought that we could use a lazy reason for explaining the not equals constraint but we did not fix the underlying problem mentioned in #25 . This PR reverts to eager reason calculation!
ImkoMarijnissen
added a commit
that referenced
this issue
Dec 4, 2024
TODOS - [x] `compute_new` and all the others should be removed or refactored - [x] There used to be an option for turning off clause-minimisation - [x] TODOs in conflict analysis - [x] Restore test cases in constraint satisfaction solver - [x] Proof logging - [x] Core extraction - [x] `get_conflict_info` now clones but should not - [x] Doc tests - [x] Refactor `get_reason_simple` - [x] Check python interface - [x] Remove the backtracking method from conflict analysis context Issues: - Closes #116 - Closes #81 - Closes #25 - Closes #3 --------- Co-authored-by: Maarten Flippo <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When using a closure as a lazy reason, it takes as input the final
PropagationContextat the time of the conflict.However, this domain can be inconsistent (e.g. it can contain the empty domain
x in [6, 5]). This goes against the assumption from certain propagators that domains which are assigned do not change (this was used in the linear not equal propagator to create lazy explanations) which resulted in incorrect explanations.An example of an instance on which this occurs is with this model and this data file as it results in incorrect explanations leading to the semantic minimiser learning a clause which is always true.
Preferably, we would provide the final consistent state to the reason calculation.
The text was updated successfully, but these errors were encountered: