feat: adding edge-finding for disjunctive #141
Draft
+16,107
−13,536
Conversation
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
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]>
When using lazy explanations, the propagator receives the internal `Assignments` structure. However, we want them to access more than just the assignments. So we introduce a dedicated context to expose a wider API. Since it is likely undesirable that propagators can access the `Assignments` directly, the accessor is marked deprecated. The only spot where we use this is now explicitly allowed but may need to be refactored.
When preprocessing a nogood, if it becomes a unit nogood, the propagator would assign the negation of the predicate with an empty reason. However, from the perspective of the proof log, that is invalid as the input to the propagator was a non-unit nogood.
Running `cargo build` in the project root directory (not necessarily
useful, I did it by accident) means you also build `pumpkin-py`.
However, I have a new laptop so I didn't yet have need to install the
development headers for Python (`python3-dev` package on APT). This
causes the the build to fail with the below linker error:
```
= note: /usr/bin/ld: cannot find -lpython3.13: No such file or directory
collect2: error: ld returned 1 exit status
```
This confused me (I've used PyO3 before), it's just an extension module
(you're calling Rust from Python so you always have an interpreter) so
why would you need the dev headers, which you usually only need if
you're calling Python from a Rust executable
(https://pyo3.rs/v0.22.6/index.html?highlight=python3-dev#using-python-from-rust).
I then noticed the `extension-module` feature is not enabled in the
`Cargo.toml`. It is enabled in the `pyproject.toml` so it works fine if
you build from `maturin`. However I think it's useful (to prevent
confusion) to have `cargo build` when invoked on the whole workspace to
still not fail. Plus, I think it's nice you can still just run `cargo
build` even in `pumpkin-py` without needing a global package that isn't
really required under these circumstances. It also means the
dependencies in the `Cargo.toml` don't really match what you are
actually building when you use `maturin`.
There's a tiny wrinkle, though. Maybe it's the reason you removed the
feature from the `Cargo.toml` in the first place. When using workspaces
and an IDE that runs `cargo check` on save, probably the Python
interpreter will not match the one in the virtualenv that you use for
maturin. This causes PyO3 to recompile on most builds. Thankfully I've
had this problem and this can be fixed, see
PyO3/pyo3#1708. This does mean that by default
someone who will develop the python interface will need to add something
to their config manually. The alternative solution however means that
cargo build will also fail without some manual work by the user
(installing a venv to the right place).
When testing, I found that the current version of the Python script
actually fails, so I fixed that and updated the README with the correct
path to the file to run. So even if you disagree with the main change
that part is definitely useful.
The `AlternatingBrancher` did not call the correct methods on the default brancher meaning that the solver had poor performance during free search (since it did not restore any keys to the heap upon backtracking). This has been fixed by performing the right calls
When creating a new domain, it could be that the lb/ub is a hole, or that there are holes outside of the bounds. This is currently not post processed before creating the domain, so this happens after minimisation for the first time. This can cause the number of literals after minimisation to be higher than before, causing an overflow: https://github.com/ConSol-Lab/Pumpkin/blob/d66ecb6e541b9d15562dc7db223b8a86b3bade13/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs#L65 Post-processing the new domain fixes this problem.
There are three spots in the flatzinc parser & constraint constructors that I believe to contain unnecessary variable creation: - `create_domains` for `BooleanLessThanOrEqual` and `BooleanEqual` - `compile_bool2int` It seems like we can directly used the parsed literals instead of creating a new variable and a linking clause. It only requires access to the underlying `integer_variable` of the literal, but I don't see that as a problem. Is there any reason for doing it this way, or is it because of the legacy structure?
The check for whether a profile overflowed the resource capacity contained an additional term; this PR removes this term
Profiling has shown that the variable/value selectors are oftentimes too slow due to the fact that they need to find the minimum/maximum value over some condition. It is also currently unclear what would be a good backup strategy for VSIDS; @maartenflippo suggested that a fully random strategy would likely be a good idea. To this end, this PR aims to implement a random variable selector which keeps track of the variables using a sparse set and a value selector which picks a random value within the lower-bound and upper-bound and randomly splits the domain on that value. The PR sets this as the default backup strategy. _The PR also includes some small fixes to the sparse set_ _Edit: Due to failing test cases, this PR is now dependent on #136_
The Flatzinc parser was not able to parse Boolean arrays. Besides, I fixed that negative integers are also parsed correctly.
Re-opening #130 due to a change in my repository. The `element` propagator improves the bounds of the RHS based on the items in the array. For this, it takes the full array into account. However, it could be that some of these items are not possible anymore due to a (partial) assignment of the `index`. The propagator doesn't currently take this into account, and I believe this can be improved.
maartenflippo
previously requested changes
Feb 3, 2025
pumpkin-solver/src/propagators/disjunctive/disjunctive_propagator.rs
Outdated
Show resolved
Hide resolved
…#114) Hi, another tiny fix while getting everything running. I'm pretty sure the negation of `literal => s_y - s_x <= -p_y` is as follows: $$l => s_y - s_x <= -p_y$$ $$\neg l => s_y - s_x > -p_y$$ $$\neg l => s_y - s_x >= -p_y + 1$$ $$\neg l => -s_y + s_x <= p_y - 1$$ Also the literal was not actually negated in the second case, so I added that as well in the way I think you're supposed to do it.
|
Also run a benchmark to see the performance implications compared to decomposition |
A well-known concept in CP is variables which are automatically updated to their previous values by the solver. This PR (based on [this PR](https://bitbucket.org/EmirD/pumpkin-private/pull-requests/58)) aims to implement these variables by creating a new trail for changes to these stateful variables. Upon backtracking, these changes are undone. As a potential application area, I have implemented it in the `LinearLeq` propagator such that it does not have to recalculate the incremental state from scratch.
…dge cases (#146) This PR addresses 2 issues: - Debug clone was backtracking to level 0 which could throw an exception for `TrailedAssignments` - The `RandomSplitter` had edge cases related to bounds
The debug propagate currently also attempts to propagate deleted nogoods
Currently, we only support upper-bounding search (LSU) in the solver; however, it makes sense to also support lower-bounding search (LUS) in the solver. This PR aims to implement lower-bounding search using assumptions. --------- Co-authored-by: Maarten Flippo <[email protected]>
The Python API does not enforce a particular optimisation routine. At the moment, we support: - LSU - LUS Both are, therefore, present in Python as well.
For some instances (e.g. `2023/code-generator/unison.mzn`, with `2023/code-generator/mips_gcc.flow.find_regno_partial.dzn`), it showed up in profiling that the dynamic brancher went through a lot of branchers upon certain events (in this case the `on_unassign_integer` event, even though only a single brancher was interested in these events). To alleviate this issue, this PR adds a method for `Brancher`s, `VariableSelector`s, and `ValueSelector`s which allows them to indicate which events they are interested in; this allows the `DynamicBrancher` to only call the `Brancher`s which are interested in it.
Previously, submitting a lazy reason in a reified propagator would crash the solver. Implementing this is non-trivial, as reasons used in conflict analysis were returned as slices. However, we need to insert a reification literal into that slice somehow. One approach would be to always return some owned buffer like a `Vec` from the reason store, so that it can insert the reification literal there. However, that would entail allocating when we ideally want to avoid that. Instead, the solution implemented here is to provide the buffer that the reason should be written in to. Then it is up to the caller to either allocate or reuse an existing allocation.
I added a script that automatically generates a bunch of constraints and posts them through the Python API. Some bugs I have found (annotated with TODO in the script): - Scaling with "0" results in division-by zero errors for some constraints - The reified propagator for Element seems to be unimplemented for now? Ideally, we can also test whether the constraint is indeed satisfied by the solution found by the solver, but I'm not sure how to that.
I have ran benchmarks on some MiniZinc challenge/MiniZinc benchmark repository instances with these results:
It is a limited dataset and, of course, on some instances there is a deterioration but these results indicate that it can be beneficial to make use of the disjunctive propagator. It could also indicate that for other instances we need different reasoning (e.g. detectable precedences) |
github-actions
bot
dismissed
maartenflippo’s stale review
Review re-requested
maartenflippo
requested changes
Feb 27, 2025
| use crate::propagators::disjunctive_task::ArgDisjunctiveTask; | ||
|
|
||
| #[test] | ||
| fn propagator_propagates_lower_bound() { |
There was a problem hiding this comment.
Since we use a view to update the upper-bounds!
| /// # Bibliography | ||
| /// \[1\] P. Vilím, ‘Filtering algorithms for the unary resource constraint’, Archives of Control | ||
| /// Sciences, vol. 18, no. 2, pp. 159–202, 2008. | ||
| pub(crate) struct Disjunctive<Var: IntegerVariable + 'static> { |
There was a problem hiding this comment.
Don't specify bounds on struct definitions. Or is there a reason why they exist here? DisjunctiveTask also does not enforce a trait bound.
Comment on lines
66
to
67
| /// TODO: this explanation could be lifted and should take into account which subset of tasks was | ||
| /// responsible for the propagation itself. |
There was a problem hiding this comment.
Clarify why this is not done yet
There was a problem hiding this comment.
I have added it now and I am running experiments again to see the impact!
Comment on lines
192
to
200
| let reverse_tasks = self | ||
| .tasks | ||
| .iter() | ||
| .map(|task| DisjunctiveTask { | ||
| start_variable: task.start_variable.offset(task.processing_time).scaled(-1), | ||
| processing_time: task.processing_time, | ||
| id: task.id, | ||
| }) | ||
| .collect::<Vec<_>>(); |
There was a problem hiding this comment.
Can this not be done once, in Disjunctive::new?
| /// # Bibliography | ||
| /// \[1\] P. Vilím, ‘Filtering algorithms for the unary resource constraint’, Archives of Control | ||
| /// Sciences, vol. 18, no. 2, pp. 159–202, 2008. | ||
| #[allow(dead_code, reason = "Will be part of the public API")] |
There was a problem hiding this comment.
Which parts are now dead_code? And will this be part of the public API? It seems like an implementation detail of the Disjunctive propagator.
This is enforced by the fact that everything on ThetaTree is pub(super).
There was a problem hiding this comment.
The ThetaTree is currently not constructed since we only create a ThetaLambdaTree.
It depends a bit, currently, it is only used in the Disjunctive but we might consider making a generic ThetaTree which is also applicable for the cumulative
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.
Currently, we decompose the disjunctive
This PR aims to address this by implementing edge-finding based on this PhD thesis. Any feedback would be appreciated!
TODOS