summaryrefslogtreecommitdiff
path: root/apt-pkg/solver3.cc
Commit message (Collapse)AuthorAgeFilesLines
* solver3: Fix error stack handlingJulian Andres Klode2025-02-181-7/+7
| | | | | | | | | | | | Pushing the stack in push and popping it in pop did not really work correctly and is more complex than needed. Instead, push the error stack at the start of the Solve() method and revert at the end, such that we leave exactly at the same error stack level we entered. To handle error clearing on backtracking, just discard any pending errors.
* solver3: Fix test-apt-move-and-forget-manual-sectionsJulian Andres Klode2025-02-181-2/+24
| | | | | Implement the moving of the auto bit. The whole auto-bit management is not entirely optimal yet, but this works.
* solver3: Store clauses as the reasons for decisionsJulian Andres Klode2025-02-141-19/+30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | So far we only stored the last reason why something was decided, for example, if "A depends B | C" and we assigned B=false, C=false, we'd store "(not) C" as the reason for "(not) A". This gives us only a partial implication graph; after all "C" was not the *sole* reason for not installing A. This has two implications: 1. We cannot do conflict-driven clause learning 2. We cannot print excellent information about why packages cannot be installed (or removed) This commit is incomplete in addressing both; in particular, we always store a clause as a reason for something that is not a root object; whereas MiniSAT would only store a clause on propagation. That is, if A depends B | C, and we install A, then we have to make a choice between B|C. Let's say we pick B, we store 'A depends B|C' as the reason whereas MiniSAT would not store a reason (because it picked the "next best" unassigned literal). Hopefully this is not going to be an issue. The reason is used to calculate the assignments that caused the decision in MiniSAT, but the idea is that we can just treat reason clauses with unassigned values as "no reason". The conflict explanation (WhyStr) has been changed to print the strongest reason; which produces the same result as the previous solution for the test suite. What does this mean? If we look at A depends B|C, let's analyse: Why not A? We return the first assigned value for B|C, likely B. We might have returned C here before as it was the last assignment, but we might also return C here, if B is not assigned. Why B? We return A. If we look at A conflicts B: Why not A? Well B Why not B? Well A Thanks to the structure of the implication graph this is quite simple, but also generalizing this to the CNF format should not be hard. A future version will extend clauses with backlinks to pkgCache::Dependency*, allowing us to print useful information to uses such as "A Depends B | C | D (>= 2)" in the real form, rather than the expanded form which may be "A -> B | C | D=3 | D=2".
* solver3: Only enqueue shared dependencies at the package levelJulian Andres Klode2025-02-141-0/+10
| | | | | | | | | | | | | | | | | | | | | Dependencies shared by all versions are enqueued at the package level, so avoid enqueuing duplicates at the version level. This presumably has no meaningful impact on performance, potentially a negative performance impact on some workloads as we now need to find the duplicates again; it can become useful when there is a lot of backtracking. More importantly though this improves error messages, because now we can say that "all versions of foo depend on X", rather than saying "foo=1 depends on X" and you are left wondering why we did not select "foo=2". In this commit though, improved error messages are not implemented, they depend on redesigning the reason tracking to use clauses. Also the rationale tracking includes a lot more dependencies of the form "pkg:arch=version -> pkg:arch" which are annoying. Improved error messages should fold them into one node.
* solver3: Remove work rescoring in favor of unit propagationJulian Andres Klode2025-02-141-56/+26
| | | | | | | | | | | | | Instead of expensive rescoring of all outstanding items, use unit propagation to find new units after conflicts. We still count the items when adding them; but unless they are 0 or 1, which they should not be, they don't have any effect: The size field is now effectively static. If the size of an optional clause changed to 1, it is inserted a second time, and then moves up to the top of the optional items per the Work::operator< rules.
* solver3: Refactor a debug messageJulian Andres Klode2025-02-141-6/+1
| | | | | Use Var::toString() to print the variable, instead of duplicating the code :D
* solver3: Pass EDSP flags directly rather than via configJulian Andres Klode2025-02-141-2/+3
| | | | | | | This was a rather silly way to communicate state, and it was in the wrong place. Notably also, multiple calls to the solver had the options sticky, that is, if you run upgrade and then it calls ResolveByKeep(), for example.
* solver3: Fix ordering of or groupsJulian Andres Klode2025-02-141-6/+10
| | | | | | | | | | | | | | | | | | | | | | We inadvertently performed a global ordering of all possible solutions for the or group using CompareProviders3. This however is not correct, as we lose the ordering of the dependency group *too* much. Mostly this has no effect, but you can see for example in test-explore-or-groups-in-markinstall various instances of it. Adjust said test case to work with the 3.0 solver to the extent possible under the current design. The 3.0 solver does Recommends after processing any manually installed packages; as such the various Recommends test cases do not work: A `Recommends: okay|upgrade` will not upgrade `upgrade` if it visited `upgrade` first. This may change at a future time, but the correct semantics for Recommends are not entirely clear. Notably, the existing solver is not always consistent. You can see here where they matter, but recently I added test-solver-recommends-depends in which the Recommends do not influence the choice of other Depends.
* solver3: Implement phasing as part of strict pinning rulesJulian Andres Klode2025-02-141-1/+3
| | | | | | | | Phased updates are ignored when strict pinning is on; such that only the installed version will be available. By design of SAT solvers, this means that the version selection clause is unit, and hence the version can be directly propagated, i.e. that choice is safe.
* solver3: Promote various Recommends to DependsJulian Andres Klode2025-02-141-0/+12
| | | | | | | | | | Already satisfied Recommends should be promoted to Depends; as well as Recommends that are new, if the version they are from is an upgrade (such that upgrading does not introduce unsat Recommends). This only works for the case where the new Recommends actually exist; test-resolve-by-keep-new-recommends is not yet implemented, but this means the phasing tests will behave correctly.
* solver3: Correctly call MarkKeep() for kept back packagesJulian Andres Klode2025-02-141-11/+15
| | | | | | This fixes the difference in test-unpack-different-version-unpacked, but more importantly this is needed for phasing to be displayed correctly once that is implemented.
* solver3: Install Essential on dist-upgradeJulian Andres Klode2025-02-141-0/+14
| | | | | | | | This is a bit gnarly, but dist-upgrade is mapped to is an upgrade + removals allowed + installs allowed :D
* solver3: Defer 3.0 'deep' autoremoval to 3.1, fix autoremoveJulian Andres Klode2025-02-141-1/+1
| | | | | | Restore the depcache's MarkRequired logic for 3.0 solver; and change the MarkInstall() call to pass a more correct value for FromUser, to not override an existing automatic status.
* solver3: Reject reverse conflicts on installJulian Andres Klode2025-02-141-0/+9
| | | | | | We forgot this in the previous iteration. This makes the reasoning in the test cases much nicer and apt-test's mantic-to-noble-jak.edsp now finishes rather than running into the timeout (potentially forever).
* solver3: Reject reverse dependencies nativelyJulian Andres Klode2025-02-141-106/+26
| | | | | | | | | | | | | | | | | | Instead of utilizing the reverse depends functionality of the cache and marking all possible reverse dependencies for removal, mark them ourselves by keeping track of reverse-implication-clauses. Notably, this improves the reverse dependency rejection substantially: The previous RejectReverseDependencies() function did not handle Provides. For this to work correctly right now, we need to discover optional clauses too when queuing them. This is somewhat suboptimal as we technically we don't care if they become unsat, we just waste time tracking them. The tests get a bit awkward, but oh well, we use what we can use.
* solver3: Implement a timeout, default 10sJulian Andres Klode2025-02-141-1/+7
| | | | | A SAT solver can run more or less forever, but that's not a good user experience.
* solver3: Discover recursive dependenciesJulian Andres Klode2025-02-141-32/+47
| | | | | | | | | | | | | | | | | | | | | | | | | | | When we have discovered all clauses for a version, discover each possible solution for the clauses. This means that when Discover(foo) is called _anything_ that could lead to foo becoming uninstallable is translated; so we can extend this next by keeping a list of reverse dependencies for each package and rejecting those. We limit the discovery to those variables that we did not already enqueue as a negative fact at the root level, as those can never become true. We are utilizing a queue here which is not the most performant solution possible, but where it excels is in producing usable stack traces when debugging. Traversing the entire dependency tree using recursion can easily produce thousand levels of recursion. The queue means that we discover packages in a breadth-first manner compatible with the order in which we propagate dependencies, which is helpful for consistency. The queue did not appear as a bottleneck in benchmarking. If it did, we could switch to a grow-only ring buffer (std::queue's underlying deque also shrinks automatically which is suboptimal).
* solver3: Defer version selection where possibleJulian Andres Klode2025-02-141-12/+20
| | | | | | | | | | | | | If a dependency can be satisfied by all versions of a package, add the package to the clause instead of the version object. This works only if there are no providers for the package: Providers are quite hard to enumerate over and make sure that all versions of a package satisfy the provider dependency. Implement arbitrary selection between packages and versions for the CompareProviders class: We pick the best version for each package and then pit them against each other.
* solver3: Avoid std::vector for statically sized arraysJulian Andres Klode2025-02-071-11/+11
| | | | | | | | | | The bounds checking on the vector accesses is killing performance, so switch from vector to a basic array, given that we don't actually need _any_ functionality from vector... Of course while we are at it, let us define a safe wrapper around it so we cannot accidentally index arrays for package IDs with version IDs and whatnot.
* solver3: Add const where helpfulJulian Andres Klode2025-02-071-4/+4
| | | | | operator[] is a bit annoying here, but oh well, what can we do?
* solver3: Point to stored clauses, do not copy themJulian Andres Klode2025-02-071-36/+39
| | | | | | This makes Work trivially destructible, and in turn solved, allowing their queues to be destructed without running destructors, and avoiding the copy should have a nice performance improvement.
* solver3: Use a package clause for optional rootsJulian Andres Klode2025-02-071-4/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of iterating over the version here and picking it, just enqueue the package as well, which should allow us to select the version at a later time. This also causes a funny inverse problem now, though, as was evidenced in one of the test cases: To summarize, if our optional roots are all single items, they will be considered soft-unit, causing them to be processed in order. However it can be that an optional root has a specific version selected because another version was rejected. Consider X Conflicts A (= 1) A, B have 2 versions: '2' available, '1' installed B (= n) Depends A (= n) Run `apt install X`. The expected result is for A and B to be upgraded to version 2. With only a package root, if B appears in the cache before A however, we will get: Install X Reject A (= 1) Install B Install B (= 1) # keep it installed Reject A (= 2) => A is being removed as both versions are rejected Hence we do also need to re-introduce the additional version clause, now we get: Install X Reject A (= 1) Install A (= 2) # it got "promoted" to a 'stronger' soft-unit Install B Fail B (= 1) # keep it installed Install B (= 2) Introduce a root state to hold all the clauses that don't have another owner. moo
* solver3: Refactor Dump() to toString()Julian Andres Klode2025-02-071-50/+25
| | | | | This vastly simplifies the code at the expense of performance, lol.
* solver3: Support comparing packages and versionsJulian Andres Klode2025-02-071-8/+15
| | | | | | | | | | | When comparing packages, we compare the best version for the package. To determine the best version, the rules for comparisons are applied normally. This allows us to mix packages and versions in a clause as the solutions for a dependency, which means we'll be able to defer the selection of a particular version of a package to a later time.
* solver3: Replace PropagateInstall() with Discover()Julian Andres Klode2025-02-071-75/+65
| | | | | | | | | | | | | | | Just propagate the stored clauses after we have discovered them; this is quite straightforward. We now more reliably discover common dependencies at the package level, adjust the test case accordingly. The next step is to make discovery recursive, or iterative, to build an entire recursive tree from all roots, and then we can reject reverse dependencies based on it. A bunch of refactorings are needed in the process. We remove the useless Hint enumeration and insert a flags struct into the State, such that we can record whether a package/version has been discovered, to avoid spending double time on discovery.
* solver3: Extract TranslateOrGroup() out of EnqueueOrGroup()Julian Andres Klode2025-02-071-39/+36
| | | | | | | This is not *purely* a refactoring, we accidentally used the version of the dependency when enqueuing conflicts rather than the reason, so the conflict string in the test case is different; the logging had the same issue.
* solver3: Extract Clause out of WorkJulian Andres Klode2025-02-071-54/+57
| | | | | Extract clause into a separate struct and embed a copy of it in our Work class.
* solver3: Simplify WhyStr()Julian Andres Klode2025-02-071-16/+5
| | | | Reuse the generic variable rendering
* solver3: Cache all configuration callsJulian Andres Klode2025-02-071-9/+4
|
* solver3: Cache calls to policyJulian Andres Klode2025-02-071-6/+8
| | | | It's a bit silly otherwise.
* solver3: Propagate single choice clauses as factsJulian Andres Klode2025-02-071-9/+11
| | | | | | | | | | | | This removes a bunch of complexity, and generalizes the propagation behavior, such that we don't need to do if (w.solutions.size() == 1 && not w.optional) Enqueue() else AddWork(w); in our callers.
* solver3: Early exit when propagating satisfied clausesJulian Andres Klode2025-02-071-4/+5
|
* solver3: Partially generalize work items from Version to VarJulian Andres Klode2025-02-071-29/+33
| | | | | | | | Store all possible solutions and choices as Var. Currently any Var in here must be a Version because CompareProviders3 cannot compare versions against packages yet, but in the future (TM), this will allow storing packages directly in clauses, which allows defering version selection to a later point.
* solver3: Simplify work orderingJulian Andres Klode2025-02-071-14/+4
| | | | | | | | | | Moving the optional != b.optional comparison ahead of the group one allows us to get a better behavior; and now we avoid the nested if. Also remove the special cases that ordered based on the reason of the work item, these have been superseded by groups a while ago.
* solver3: Drop unused upgrade flagJulian Andres Klode2025-02-071-2/+2
| | | | This was leftover from before the groups were added.
* solver3: Credit MiniSATJulian Andres Klode2025-01-301-0/+11
| | | | Gbp-Dch: ignore
* solver3: Use a propagation queueJulian Andres Klode2025-01-301-8/+24
| | | | | | | | | | | | | | | | | | | Instead of directly propagating in a recursive fashion, queue propagations in a queue and work on them in a loop per the miniSAT paper. We call Propagate() only at the end of the FromDepCache() function and then in the Solve loop. Delaying the initial propagation means that we get a stronger reasoning: Assume you have x->a->b->c, y->c and you install x,y: - Previously we traversed: x, y, x->a, a->b, b->c, (y->c) - but now we traverse: x, y, x->a, y->c, a->b, (b->c) Notably c now has the implication y->c instead of x->a->b->c. Inside the solver we need to call Propagate in a loop: Propagating facts can fail and we then backtrack. If backtracking is succesful, we have gained a new fact to propagate.
* solver3: Replace Install() with Enqueue(), and PropagateInstall()Julian Andres Klode2025-01-301-41/+33
| | | | | | Do not enqueue common dependencies if a version is selected already, this avoids test suites changing now in behavior as the ordering is different.
* solver3: Remove NewUnsatRecommends groupJulian Andres Klode2025-01-301-2/+0
| | | | | | This is more or less unused; but it particularly has the bad problem of forcing new unsat recommends to be solved *before* dependencies. Which is awkward.
* solver3: Soft unit propagation for optional itemsJulian Andres Klode2025-01-301-2/+7
| | | | | If both items are optional, unit items should be processed first.
* Drop usage of macro APT_OVERRIDE for simple overrideDavid Kalnischkies2025-01-051-2/+2
| | | | | | | | | We were rather inconsistent in using it and as our public headers contain deduction guides (a c++17 feature) it seems silly to try to hide a c++11 feature in a macro, so lets stop this charade and drop the macro and while we are changing all these lines lets apply [[nodiscard]] (another c++17 feature) and other suggestions from clang-tidy and formatting for a little more consistency.
* solver3: Reject all non-candidates outright for strict pinningJulian Andres Klode2024-12-031-25/+18
| | | | | | | | Reimplement strict pinning by rejecting the non-candidates when translating the problem from the depcache to the solver. This is substantially better than restricting the list of alternatives for an or group to only include allowed ones for debugging purposes, albeit a bit slower.
* solver3: Add a missing debug level checkJulian Andres Klode2024-12-031-1/+2
|
* solver3: Fix intransitivity of version comparison on upgradeJulian Andres Klode2024-12-021-11/+17
| | | | | | | | | | | | | | | | | | | | | | | | | We only compared candidate to installed version, but candidate should dominate all versions, otherwise we end up in the fancy problem of elpa-notmuch in upgrade-noble-t64-remove-desktop-2024-03-29.edsp Where we had three versions: not-installable 0.38.3-1ubuntu1 candidate 0.38.2-1.1ubuntu2 installed 0.38.2-1ubuntu2 And received an ordering: installed > non-installable > candidate despite candidate > installed This is only visible with no-strict-pinning right now, as we are otherwise filtering out invalid choices (and hence we only have candidate and installed otherwise).
* solver3: Refactor Install(Ver) to PropagateInstall(Ver)Julian Andres Klode2024-11-021-30/+34
| | | | | | | | | | This is the first part of changing from Install() to Enqueue() for installs, affecting only the versions. For packages, we still have to resolve the group changing: When propagating cleanly, we don't have the information as to which group the package was part of, hence we are no longer able to queue the version selection of upgrades before obsolete packages, for example, which needs solving.
* solver3: Check whether installable versions are allowedJulian Andres Klode2024-11-021-7/+10
| | | | | | | We only checked if they were still installable, but not if they were allowed. We should removed the allowed version handling altogether presumably - we should just mark non-allowed versions as rejected early on.
* solver3: A version selected for install already is allowed.Julian Andres Klode2024-11-021-1/+1
|
* Add a FIXME around the heap compactionJulian Andres Klode2024-11-021-0/+2
| | | | | | | | | | | | | | Our work heap is currently cleaned from deeper levels by removing the entries from the heap and then remaking the heap which is very inefficient. We should mark the items as erased instead, and only do the remove & make_heap dance if we have a lot of erased entries in there. Possibly we maybe should use a structure that actually allows removing entries, that is, an std::set, but that warrants more investigation on performance aspects.
* solver3: Rename the 'dirty' bit to 'erased'Julian Andres Klode2024-11-021-6/+6
| | | | This captures the meaning better
* solver3: Remove the Reject() function, propagate in Enqueue() insteadJulian Andres Klode2024-11-021-52/+37
| | | | | Long term we should have a propagate queue, this is the minimal change to keep the behavior identical, a first step on the road.
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2026-07-18 23:12:21 +0000