refactor(pumpkin-solver): Force checkers to be registered in propagator constructor - #457
Conversation
|
An incomplete review from my side to keep things from being blocked (I am guessing that perhaps not too detailed reviews are ok for now, and once everything is in place, we do a detailed review?): Overall looks like nice design. ConstructedPropagator -> I like the idea of having a struct as a return type. I am not sure about the name, since it holds the propagator plus additional info. Some potential alternative names: PropagatorDefinition/Spec/Description? In some sense, it is a specification of the propagator. About the name "RuntimeCheckers". I like this name. But we previously used "ConsistencyCheckers", which is more descriptive in what it does, but RuntimeChecker is more descriptive of when it does checking. What is better, should we also use this name in our paper? I am slightly in favour of RuntimeCheckers, but not sure. Is there a world in which we want to have empty runtime checkers? We have support for it in the code with the builder, just to check! pub trait StoresCheckers -> why is this a trait? I am not too opposed to this so that we keep things going but just wondering.
|
ImkoMarijnissen
left a comment
ImkoMarijnissen
left a comment
There was a problem hiding this comment.
Looks good overall, I left some small comments for now!
I like
For me the term RuntimeCheckers is more natural. I am struggling to remember that
Yes! The nogood propagator only posts checkers when nogoods are added. So at construction the checkers are empty.
To decouple this module from the rest of the solver details. Allows for easier testing in isolation.
Actually, I think this a natural consequence of the fact that our checkers are sound but not complete. If any checker accepts an inference it is (should be) sound. |
It would be useful if you could elaborate on this, so that we can also make the change in the paper, in particular the part of what is so confusing about the consistency checking term. In my mind, 'checking consistency' means we want to be sure the propagator is at its advertised level of consistency. To do that, we need to check every removal from the domain (propagator checker, which is composed on inference checking plus checking the applicability of the explanation given the trail) and we need to check for every value we kept in the domain (retention checkers). Then Consistency Checkers for both of these makes sense. But maybe runtime checking sounds nice because it shows when these checkers are used, and it is perhaps clearer that these are not 'conventional' checkers used in proof systems.
Ah yes, so probably also in the hypercube propagator, or any compound propagator that is not a constraint on its own but a collection of constraints.
Great, like in the other PR, small traits -> good!
Technically, our checkers are not complete. However, the way we use checkers is quite deliberate. For all other uses of checkers, if a checker fails, we know we have a problem and we know exactly where the problem is, e.g., a propagation cannot be justified even though we expect that it should, despite the checkers not being complete. In fact, we might not even want complete checkers, since we want to know that our components are working exactly as they should, and not be right for reasons we did not foresee! When it comes to 'any_checker_accepts_inference', it is very different from the above cases, since we do not know what to check; we use all these checkers and expect one of them to trigger. It would be more natural if we could pinpoint exactly which one, which would make more sense given how we do things. We do not need to make changes to this now because it is not critical for this PR, but I do feel that it sticks out a bit! |
dbd0edc to
e8ae6eb
Compare
commit f6cce03 Author: Maarten Flippo <maartenflippo@outlook.com> Date: Tue Jul 28 20:12:59 2026 +0200 refactor(pumpkin-solver): Force checkers to be registered in propagator constructor (#457) Updates the interface of `PropagatorConstructor::create` to explicitly require a bag of checkers to be provided. This makes it harder to forget and requires explicit opt-out of registering checkers. Based on discussions for #449. ## Changes - Introduce `ConstructedPropagator` as the return type of `PropagatorConstructor::create` - Remove `PropagatorConstructorContext::add_inference_checker` - Remove `PropagatorConstructor::add_inference_checkers` commit 8e61fec Author: Maarten Flippo <maartenflippo@outlook.com> Date: Mon Jul 27 13:13:12 2026 +0200 fix(pumpkin-core): Handle predicates over constants in inference consequent (#516) When we write an inference `A -> p` where `p` is a predicate over a constant domain, we should substitute it for false. Otherwise, the log will contain a variable that is not named in the input model. For example, for a constraint $x \times y = 5$, we may log `[x >= 5] /\ [y >= 2] = ["5" >= 10]`. Obviously the consequent should just be false, not the stringified version of the constant 5. commit 8629bbd Author: Imko Marijnissen <50290518+ImkoMarijnissen@users.noreply.github.com> Date: Mon Jul 27 10:11:02 2026 +0200 chore: Update README to include MiniZinc challenge 2026 results (#518) commit 83f78da Author: Imko Marijnissen <50290518+ImkoMarijnissen@users.noreply.github.com> Date: Mon Jul 27 09:54:53 2026 +0200 feat(pumpkin-solver): Start looking for new watcher from the previous watcher location (#496) Closes #489. Starts looking for the new watcher from the location of the previous watcher. Currently, this is stored as an additional `PredicateId` in the `ArenaAllocator` for quick retrieval. - [x] We could consider storing both the length of the nogood and the last traversed watcher in a single `PredicateId` (assuming that nogoods do not exceed a length of 65,535). - [x] Test with the new packed length + last-traversed combination. - This turned out to perform worse (for unknown reasons), and it appears that for the instance `2021_pentominoes_size_10_tiles_10_seed_17_strategy_target.fzn`, there is a nogood whose length exceeds 16 bits... **Small Note** - Normally, we could like to look at the range $(l..|N|) \cup [2..l]$ (where $l$ is the index of the last-traversed watcher and $N$ is the nogood). However, this leads to issues with indices when nogoods are binary (since $l$ will be out-of-range). This is easily fixed by traversing $(l..|N|) \cup [2..\min\\{l, |N| - 1\\}]$, but this looks somewhat messy in practice. --- ## Result Interpretation The experimental results indicate that avoiding retraversing the watchers indeed speeds up the performance of the solver, solving 3 more instances to optimality, improving the MiniZinc score by 23 points (in a 1-to-1 comparison) and reducing the average primal integral by about 3. ### Overall Results `main` ``` {'ERROR': 47, 'OPTIMAL': 104, 'SATISFIABLE': 141, 'UNKNOWN': 96, 'UNSATISFIABLE': 5} ``` `new` ``` {'ERROR': 46, 'OPTIMAL': 107, 'SATISFIABLE': 140, 'UNKNOWN': 95, 'UNSATISFIABLE': 5} ``` ### MiniZinc Score ``` { 'main': 117, ' new': 140 } ``` ### Average Primal Integral ``` { 'main': 33.4, 'new': 30.6 } ``` commit 94cd166 Author: Matthias van Vliet <112569120+MatvV04@users.noreply.github.com> Date: Mon Jul 27 08:38:14 2026 +0200 fix(pumpkin-checker): Incorrect rejection of unsatisfiable optimisation problem (#515) Proposed fixes to the two issues in #514 . The unit test that tested the acceptation of unsatisfiable optimisation problems is also fixed here, as the assertion was opposite to what it was supposed to be. commit 4c8c74d Author: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Date: Sun Jul 26 16:09:42 2026 +0100 chore(deps): bump enumset from 1.1.13 to 1.1.14 (#511) Bumps [enumset](https://github.com/Lymia/enumset) from 1.1.13 to 1.1.14. <details> <summary>Changelog</summary> <p><em>Sourced from <a href="https://github.com/Lymia/enumset/blob/main/RELEASES.md">enumset's changelog</a>.</em></p> <blockquote> <h1>Version 1.1.14 (2026-07-20)</h1> <ul> <li>Fixes building on <code>#[no_std]</code> targets with <code>serde</code> enabled.</li> <li>Small improvements and clarifications to the documentation.</li> </ul> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/Lymia/enumset/commit/fde6b36448e50e8904ac7a80cfef4ef7dedfbd51"><code>fde6b36</code></a> Bump version to 1.1.14</li> <li><a href="https://github.com/Lymia/enumset/commit/eb1e5c96d278728b334e7ffd3f943ff746766f4e"><code>eb1e5c9</code></a> Fix serde default-features.</li> <li><a href="https://github.com/Lymia/enumset/commit/dcac512ed2bb25a808223595ed6f1bdee71012aa"><code>dcac512</code></a> Test serde configuration on embedded.</li> <li><a href="https://github.com/Lymia/enumset/commit/a254f1c5be56409504d58d1a5389ae0a38cd67ec"><code>a254f1c</code></a> Fix broken links in the documentation.</li> <li><a href="https://github.com/Lymia/enumset/commit/dac15503e68dc748f429740b2855b038d37e8957"><code>dac1550</code></a> Improve documentation for the deprecated functions in enumset.</li> <li><a href="https://github.com/Lymia/enumset/commit/9f0629f25af1ebefe8f4cd9661b201610eb71b13"><code>9f0629f</code></a> Correct changelog.</li> <li>See full diff in <a href="https://github.com/Lymia/enumset/compare/v1.1.13...v1.1.14">compare view</a></li> </ul> </details> <br /> [](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) --- <details> <summary>Dependabot commands and options</summary> <br /> You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot show <dependency name> ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself) </details> Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
3 participants
Updates the interface of
PropagatorConstructor::createto explicitly require a bag of checkers to be provided. This makes it harder to forget and requires explicit opt-out of registering checkers.Based on discussions for #449.
Changes
ConstructedPropagatoras the return type ofPropagatorConstructor::createPropagatorConstructorContext::add_inference_checkerPropagatorConstructor::add_inference_checkers