Skip to content

Conversation

@aszady
Copy link
Contributor

@aszady aszady commented Oct 6, 2025

SAT construction used an implication that one provided dependency implies all dependencies from that package. That's effectively an equivalence relation between all these variables and thus can be merged into one.

This reduces generated SAT size a bit.

//pkg/sat:sat_determinsitic_test runs ~3× faster;
//pkg/sat:sat_test runs ~30× faster.

@github-actions
Copy link

github-actions bot commented Oct 6, 2025

⚠️ Optional job e2e-bzlmod-toolchain-circular-dependencies failed ⚠️

  • exit status: 1

"A": []string{"0:1.0-1"},
})
expectedVars(g, model, "A-0:1.0-1(A)")
expectedVars(g, model, "A-0:1.0-1")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This parenthesis requirement duplicates appears on real RPM requires, I feel dropping this from tests may actually break real resolution
Why are you dropping them?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure what do you mean :(

This follows directly from the change in func (v Var) String() string, as Var no longer has info about specific resources the package provides.
Is there some case not covered by tests?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is what I mean https://g.co/gemini/share/f453cd2e46af, as you can see an RPM may say it depends on feature(modifier) I think we're dropping the modifier part with this change set, we will only notice the breaking change at runtime not while rendering the required RPMs

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that at no point bazeldnf parses the content of provides/requires/conflicts name, so there's no place to drop that modifier.

What this change does for e.g. glibc-related SAT variables, would be this transformation of a debug string for Var struct. For example:
SAT variables:

  • glibc(libc.so.6(GLIBC_2.16))
  • glibc(libc.so.6(GLIBC_2.17))

  • will be replaced by single one:
  • glibc.

The info about particular resource provided (e.g. libc.so.6(GLIBC_2.16)) is now processed only at the previous stage of SAT construction – in the ProvidedResource struct.

The intention of this change is to keep behaviour the same, while simplifying the internals.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have to echo @manuelnaranjo 's comment - it looks like in some of the later tests we're previously expecting multiple distinct qualifiers for the same package? The belief is that theyre not being used?

expectedIgnores(g, model)
expectedAnds(g, model,
bf.Eq(x1, x2), // Equivalence (platform-python)
bf.True, // Nothing to install
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what is causing this change and why is it desirable?

"A": []string{"0:1.0-1"},
})
expectedVars(g, model, "A-0:1.0-1(A)")
expectedVars(g, model, "A-0:1.0-1")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have to echo @manuelnaranjo 's comment - it looks like in some of the later tests we're previously expecting multiple distinct qualifiers for the same package? The belief is that theyre not being used?

@aszady
Copy link
Contributor Author

aszady commented Jan 23, 2026

Perhaps it's hard to explain the nature of this change with such a big patch.
I split it into smaller substeps. Maybe that will allow us to pinpoint which one is so controversial.
Let's start with #177, #178, #179, #180, #181, #182, and #183, and more to follow after these merge.

@aszady aszady marked this pull request as draft January 23, 2026 17:04
aszady added 12 commits January 24, 2026 13:32
Variable generation is separated into two parts:
- extracting `Resource`s provided by the package – data most useful for the `Loader`;
- creating SAT variable related to that resource – data most useful for the `Resolve` (`Model`).

This modularization of code should facilitates future code changes.

The `VarTypeResource` vs. `VarTypeFile` distinction was not used,
therefore these were merged for further simplification.
After rmohr#171, we're allowed to require the same package multiple times from another package.
As the `Resolve` function just divides the input set of `*api.Package` in three different classes
(installed, excluded, ignored), there is no need to use `VarContext` as a key
in intermediary structs.
The refactored logic more clearly implements this intention.
Also, this enables removing the `VarContext` in the future.
The purpose of the code removed in this change was to keep the iteration over `pkgProvideKeys` stable
for deterministic SAT formulation.
This can be achieved easier – `packages` already have deterministic order and also `explodePackageToVars` is deterministic.
Therefore the dependency on `VarContext` can be removed and code simplified.
The `Loader` already has the needed data to derive the second argument.
Decreasing risk of errors and making future changes easier.
by reworking for loop in the results interpretation code.

Previously, the code iterated through SAT model and filtered only `VarTypePackage` vars.
The new version iterates through all the vars in our model and filters similar type of vars.

The problem was: when a given variable is not used in any constraint, it won't appear in the SAT model.
This is not happening yet, as each variable is used, but it's not guaranteed for this assumption to hold in the future.
With this change we will be able to correctly identify the excluded packages.
For each package we had this set of implication over all `provided`:
one `provided` is on ⇒  all `provided` are on as well.

This is effectively the equivalence between all these variables,
and therefore can be represented by `bf.Eq` instead.

Such formulation is easier for the used SAT solver, as example runs show:

before:
//pkg/sat:sat_determinsitic_test                                         PASSED in 20.3s
//pkg/sat:sat_test                                                       PASSED in 118.7s

after:
//pkg/sat:sat_determinsitic_test                                         PASSED in 8.9s
//pkg/sat:sat_test                                                       PASSED in 6.8s

Note that tests under `sat/loader_test.go` guarantee that we're still solving the same problem.

This change focuses on improving the performance.
Follow-up changes are recommended to cleanup the code from these redundant variables.
SAT construction used an implication that one provided dependency implies all dependencies from that package.
That's effectively an equivalence relation between all these variables and thus can be merged into one.

This reduces generated SAT size a bit.

//pkg/sat:sat_determinsitic_test runs ~3× faster;
//pkg/sat:sat_test runs ~30× faster.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants