apt/apt-pkg/solver3.cc, branch 2.9.31

solver3: Fix error stack handling

2025-02-18T13:31:48Z

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-sections

2025-02-18T09:56:45Z

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 decisions

2025-02-14T18:08:45Z

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 level

2025-02-14T18:08:45Z

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 propagation

2025-02-14T18:08:45Z

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 message

2025-02-14T18:08:45Z

Use Var::toString() to print the variable, instead of duplicating the code :D

solver3: Pass EDSP flags directly rather than via config

2025-02-14T18:08:45Z

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 groups

2025-02-14T18:08:45Z

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 rules

2025-02-14T18:08:45Z

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 Depends

2025-02-14T18:08:45Z

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.