Conversation
art-w
marked this pull request as draft
September 2, 2026 15:57
art-w
force-pushed
the
sat-incremental
branch
from
September 2, 2026 16:40
24abcc3 to
a77a882
Compare
Alizter
added a commit
that referenced
this pull request
Sep 2, 2026
In preparation for the on-demand loading of opam packages by the `opam_solver`, this refactoring introduces a small abstraction `At_most_group` to represent a (growing) set of SAT variables of which at most `n` may be true (e.g. for conflict classes with `n=1` or in the future for minimizing `avoid-version`). Currently we don't make use of the fact that those groups may grow as every constraint is preloaded ahead of time (so we only `seal` those groups once before the SAT solver starts, just like before). With on-demand parsing of opam files however, we'll have to handle the incremental discovery of additional elements bounded by these at-most-size groups. Growing a group incrementally is possible (e.g. from `[y;z]` to `[x;y;z]`) because the new constraint `at_most n [x;y;z]` is strictly stronger than the previous one `at_most n [y;z]` (we could even get rid of the old clause, but currently this removal operation is not available nor critical for performances). It's possible to merge this PR before or after the incremental SAT clauses (#16303), although it's not that useful atm (it's just easier to review as an independent refactoring).
Alizter
reviewed
Sep 2, 2026
art-w
force-pushed
the
sat-incremental
branch
from
September 3, 2026 09:58
a77a882 to
68442c1
Compare
art-w
marked this pull request as ready for review
September 3, 2026 09:59
art-w
marked this pull request as draft
September 3, 2026 12:38
Signed-off-by: Arthur Wendling <arthur@tarides.com>
Signed-off-by: Arthur Wendling <arthur@tarides.com>
Signed-off-by: Arthur Wendling <arthur@tarides.com>
art-w
force-pushed
the
sat-incremental
branch
from
September 3, 2026 16:40
68442c1 to
9b22370
Compare
Contributor
Author
|
After more testing, I removed the optimization to skip backtracking for toplevel facts: it always backtrack now (when necessary), otherwise the deductions resulting from toplevel facts would be undone at the wrong level. With that correction, the (incoming) incremental |
art-w
marked this pull request as ready for review
September 3, 2026 16:51
Alizter
self-requested a review
September 9, 2026 14:20
Collaborator
|
I got a bit lost following the logic last week, and will resume this eventually. |
Alizter
reviewed
Sep 9, 2026
| | Union lits as clause -> | ||
| watch_lit (neg lits.(0)) clause; | ||
| watch_lit (neg lits.(1)) clause | ||
| | At_most _ -> () (* already watched *) |
Collaborator
There was a problem hiding this comment.
As a reminder for myself, I was trying to understand why we aren't tracking watchers here.
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
2 participants
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.
To allow the on-demand loading of opam packages by the
opam_solver, we need the SAT solver to support the addition of constraints after the search has started (otherwise we have to build the whole SAT problem upfront, which requires reading every potentially relevant opam files ahead of time).This is slightly tricky to implement, so the fuzzer was updated to show that clauses added incrementally produce the exact same solution as before.
In particular:
at_least_one [ a ; ... ]whenais already true is automatically satisfied, but we can't drop the constraint if the solver could backtrack and changeato be false, so we only do those simplifications at the "toplevel").trailwould be wrong as it wouldn't reflect the logical deduction order anymore). A special case here is that toplevel deductions ("facts") do not require backtracking since they are never undone.I acknowledge that this is going to be hard to review, so you may want to wait on the incremental
opam_solverto confirm that this PR actually works.