Add support for a CDCL-type SAT solver using the Resolvo crate #1179
Conversation
This file contains 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
|
Something of a PSA for anyone trying this code out, we've discovered that #1130 introduced a bug that makes the original solver not respect host options. We're working on a fix. |
|
An update on the topic we discussed in the weekly meeting about getting different results from the solver between different runs. I realized that what is happening is currently builds of a version are not being sorted and so the build the solver will pick is subject to one or more per-process random seeds. If I ask for python and it depends on gcc, it will first try to use the highest version of python available, but it might by chance pick a build of python that depends specifically on gcc/6. This is all due to how the candidates of python are ordered. I will revisit the sort logic to make it behave more like the original solver. This should make the solve result deterministic between runs if the repo contents are the same. |
jrray
force-pushed
the
resolvo
branch
2 times, most recently
from
03ee415 to
daa4be4
Compare
Resolvo is a CDCL sat solver for package managers and will hopefully prove to be much better at solving quickly than our mostly brute-force approach. Making a checkpoint here after achieving a simple "solve" to get a feel for how spk type map onto Resolvo's concepts. Although currently the smallest unit the solver works with is a package, and that likely needs to change to a component. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
This supports package-specific vars but not non-namespaced vars. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
A necessary step towards supporting solving for specific components and handling their dependencies. Signed-off-by: J Robert Ray <[email protected]>
Resolvo doesn't offer a way to declare constraints that aren't associated with a package. The strategy employed here is to create synthetic packages to represent global variables. Whenever a new possible value for a global variable is discovered, the solver needs to be restarted so when "candidates" for a global variable are requested, it returns a "package" (solvable) for each possible value that variable might take. Then, the requirement for packages that have that specific value can be models as a dependency on the synthetic package. It is not too common for packages to have install requirements on non-namespaced vars, so in practice this solver restart may not be a frequent occurrence. Also, top level options (not yet implemented) will allow packages that expect vars with other values to be excluded instead of having to ingest those different values. Of course it would be preferable for the solver to support this concept without the restart mechanic, but maybe it is worth considering making it a requirement for packages to only have namespaced var requirements. Another option is to maintain a cache of known var values somehow either in the repo or in an external service. This could cut down on the number of instances where the solver needs to be restarted. Signed-off-by: J Robert Ray <[email protected]>
Since PackageSource::Repository includes the repo, the debug output would include the entire repository contents, making the debug output too verbose. Signed-off-by: J Robert Ray <[email protected]>
For now just focusing on solving for a runtime environment with existing builds. Signed-off-by: J Robert Ray <[email protected]>
Start modifying the original solver tests to run the test against both solvers. Signed-off-by: J Robert Ray <[email protected]>
Not all solver tests are applicable. Where possible, for tests the cdcl solver doesn't pass yet, add #[should_panic] so the test suite still passes as a whole. As the cdcl solver can pass more tests, this will highlight the tests that can then be enabled for the cdcl solver. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
At least well enough to make a handful of tests pass. Signed-off-by: J Robert Ray <[email protected]>
Well enough to satisfy the one test. Signed-off-by: J Robert Ray <[email protected]>
Stop completely excluding all source builds. Signed-off-by: J Robert Ray <[email protected]>
This required rethinking the type backing NameIds to subdivide a package into its components. For example, "python:run" and "python:build" are considered separate packages by the solver. It's not possible for a single request to resolve to multiple resolvables. Either a request for "All" would have to be expanded into requests for the individual components, or there has to be a [virtual] package "python:all" that represents a dependency on all the components of that package. Since it is not possible to know the full set of components for a request like "python:all", where the set of components may differ between the different versions of python, then only the latter approach is feasible. Dependencies are needed to ensure the solve only contains components from the same spk package build. Signed-off-by: J Robert Ray <[email protected]>
Though the use of the run component is still hard coded. Signed-off-by: J Robert Ray <[email protected]>
Pass another test. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
By using an enum here, the global var handling can use its own enum variant instead of the flawed string prefix approach. Now it is simply not possible for a package name to be confused for a global var. Signed-off-by: J Robert Ray <[email protected]>
Messed up the logic when checking :all cases. Add test for this case. Signed-off-by: J Robert Ray <[email protected]>
These are effectively turned into more requests. Now the host options are being looked at. Signed-off-by: J Robert Ray <[email protected]>
It is safe to update the known values without restarting the solve here, since these functions are only called before starting the solve. But that's not enforced by the code in any way at the moment. Signed-off-by: J Robert Ray <[email protected]>
The requested by column is not populated. Signed-off-by: J Robert Ray <[email protected]>
At SPI the newest python version available on centos is an embedded package, but it is undesirable for `spk env python` to choose an embedded python package. It also follows that it would have preferred to build from source a newer version of a package instead of use an existing build of an older version. Signed-off-by: J Robert Ray <[email protected]>
Improve performance by not reading builds for packages that are for versions that are not applicable to the root requests. Signed-off-by: J Robert Ray <[email protected]>
Just printing something to stderr for now, in order to gauge how many retries are happening in practice. Signed-off-by: J Robert Ray <[email protected]>
The abstract solver now has a `run_and_print_resolve` that takes a formatter, which makes it possible to run either the old or new solver in a consistent way. The original `run_and_print_resolve` function has become `pub(crate)` to catch all the places that needed to be modified to use the new function. Signed-off-by: J Robert Ray <[email protected]>
Making the original function `pub(crate)` to force code to change to use the trait instead. Remove the unused `run_and_log_decisions` function. Signed-off-by: J Robert Ray <[email protected]>
AbstractSolver was split into multiple traits with some blanket implementations for refs while chasing compile errors but this may not have actually been necessary. Add the "solver" flags to more commands so the user can choose what solver to use in more cases. Working towards being able to choose between the original solver and the new solver for all operations. More tests now run the test with both solves. Signed-off-by: J Robert Ray <[email protected]>
Making it possible to choose what solver to use when running spk tests. Signed-off-by: J Robert Ray <[email protected]>
However, this can still become a recursive call that blows out the stack if the bounds on Solver don't fit the bounds on the "real" `test` implementation. Signed-off-by: J Robert Ray <[email protected]>
In order for `flags::Solver::get_solver` to offer a choice in what solver is returned, it needs to have access to the `solver_to_run` setting in `flags::DecisionFormatterSettings`. This change continues the theme of changing from a DecisionFormatter "containing" a solver to a solver "containing" a DecisionFormatter. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
`key_entry_names` is unused after it is cloned into `ordered_names`. Signed-off-by: J Robert Ray <[email protected]>
In order to reuse this logic for the resolvo solver, extract it to an external function. It is not practical for the resolvo solver to directly use a SortedBuildIterator. Signed-off-by: J Robert Ray <[email protected]>
Potential speedup by avoiding doing the reversal as a separate step. Signed-off-by: J Robert Ray <[email protected]>
Reuse the same build sorting logic as the original solver in order to get a deterministic result out of the solve. The solve can change drastically based on which build is selected first. Signed-off-by: J Robert Ray <[email protected]>
This is a public repo. Signed-off-by: J Robert Ray <[email protected]>
Signed-off-by: J Robert Ray <[email protected]>
When populating the Solution object, embedded packages need to be categorized properly or else when calculating the layers for the solution it ends up with an empty blob as one of the layers, which is an error. Handle source builds in resolvo solve When not building from source. Signed-off-by: J Robert Ray <[email protected]>
The case where a stub only depended on the Run component of the parent still needs to declare a dependency to bring it in. Signed-off-by: J Robert Ray <[email protected]>
To promote better test coverage, the build_package family of macros now require the name of the solver to use, and all the tests using these macros now run the test against all three solver choices (ignoring "all"). Workaround too many arguments lint and rstest la10736/rstest#226 (comment) Bumped to the latest version of rstest first to see if that would help. Signed-off-by: J Robert Ray <[email protected]>
The solver tests were not passing if this feature is enabled, and this exposed a few problems in not handling ':all' requests correctly. When generating the "VersionSet" for dependencies, the PkgRequest needs to have the correct component populated. The logic for skipping or not skipping candidates when build from source needed to handle ':all' and it was restructured for clarity. When filtering candidates for a request of a component of a specific build, source builds needed to be filtered out. Signed-off-by: J Robert Ray <[email protected]>
Fix commented out code in cmd_test for build stage tests and add a new test that checks the basic behavior of a build stage test that the test environment includes the build dependencies of the package being tested. Lift the old solver's configure_for_build_environment method to AbstractSolver. Although the other test stages have code that only lives in the cmd_test crate to configure the solver properly, the build stage uses this method that was defined in the solver itself. While the logic of configure_for_build_environment could be duplicated in cmd_test, it is also reused by other code in the solver so it made sense to preserve the logic as a reusable solver method. Signed-off-by: J Robert Ray <[email protected]>
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.
🚧 Work in Progress 🚧
It has been frequently requested over the life of this project to adopt a SAT solver in the hopes that it would provide faster solves and/or better messages when things can't solve. The Resolvo looked promising as it supports lazy solving and attempts to present solve errors in a relatively easy to understand format.
I have implemented Resolvo's DependencyProvider trait for spk packages and got enough of the spk package compatibility concepts right that the existing solver tests are all passing when run against the new solver.
I have also started to hard code changing all uses of the original solver into using the new solver just to expedite being able to test the new solver with some real world solves at SPI. There will be more work required to make it possible to choose between these solvers at runtime.
The new solver doesn't return a Graph because it doesn't use Node or State. It doesn't use Decision or Change. It doesn't use the existing validator types since those are designed to validate against a State. Solves aren't run via a SolverRuntime or through a DecisionFormatter. What is similar is the way a Solver is configured, and it still returns a Solution, although the Solution is not necessarily populated with the same details. It does well enough to pass all the tests (we need more tests!).
The high level view of how Resolvo works is that the DependencyProvider needs to be able to return a list of candidates for a request, filter those down based on compatibility, then enumerate all the dependencies of a given candidate. Rather than how our solver validates a package based on the state of the partial solve, Resolvo just needs to know if a given package (build) is compatible with a given request (python/3.11).
One of the first challenges was dealing with global var requests, meaning var requests that have no namespace. Resolvo requires that all requirements are attached to a specific package name. In order to handle global vars, each global var, for example, debug/true, is turned into a pseudo package called "debug". Then, since the DependencyProvider has to return the list of candidates (values) for "debug", all possible values that var can have has to be known in advance. To make that possible, the solve is restarted as new values are discovered. It is likely going to be necessary to maintain a cache that can be reused between solves to minimize the need to restart the solve.
Another challenge I haven't found a better approach for yet is that since all the candidates need to be returned upfront, when getting the candidates for a package, all the builds of all the versions of that package need to be visited, which includes reading in each build's package spec. This would benefit greatly from some kind of package index in the repo so this data could be read in bulk. I tried something where the list of candidates is first just the list of versions available for a package, but then it wasn't giving me the ability to filter those versions later after reading the builds.
What comes next is getting a test build up and running inside SPI and experimenting with some solves.