| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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".
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
A SAT solver can run more or less forever, but that's not a good
user experience.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
operator[] is a bit annoying here, but oh well, what can we
do?
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
| |
This vastly simplifies the code at the expense of performance,
lol.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
Extract clause into a separate struct and embed a copy of it in
our Work class.
|
| | |
|
| |
|
|
| |
It's a bit silly otherwise.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
It is very important that we check the return value of all these
functions, otherwise the logic is wrong.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
This was leftover from before the groups were added.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
Do not enqueue common dependencies if a version is selected already,
this avoids test suites changing now in behavior as the ordering is
different.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
This captures the meaning better
|
| |
|
|
|
| |
Long term we should have a propagate queue, this is the minimal change
to keep the behavior identical, a first step on the road.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
These are taken roughly from the MiniSAT paper. We still have a bit
to go in actually encoding all clauses so the reasons are still
variables, and Assume() isn't fully working yet.
Adjust the existing Install()/Reject() code to use these functions,
we already see additional lines in the log that we failed to log
before, and this ensures more consistency.
This is sort of still the wrong direction: Install()/Reject() do the
propagation too; but that is tbd.
|
| | |
|
| |
|
|
|
|
|
| |
Adopt MiniSAT's strategy for dealing with assignments and choices,
having a single step undoOne() function to undo one and record them
all on the queue; this should likely speed up backtracking since we
no longer need to rescan everything.
|
| |
|
|
|
|
|
|
|
|
| |
Basically this boils down to checking that the priority of the
source candidate candidate is higher or equal than the priority
of the package's candidate that is being under consideration.
It stands to reason if we maybe we should actually calculate a
source candidate version; this will look similar but may perhaps
perform slightly different.
|
| |
|
|
| |
More code but nicer to read
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This makes more sense, as all package versions are obsolete that
are not the candidate, usually.
Pay special attention to no-strict-pinning: If we don't have
strict pinning, a package without a candidate version may still
be non-obsolete if the latest version is not obsolete.
Likewise, in no-strict-pinning any later source version that exists
will cause the package to be considered obsolete, rather than just
candidates.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This has two aspects:
1. For a dependency A | B | C we order the obsolete packages last,
that is, if A is obsolete, this gets reordered to B | C | A,
such that we try to pick non-obsolete packages first to ease
upgrade calculation.
2. When comparing two dependencies, we order dependencies into three
groups: First we satisfy dependencies mentioning only non-installed
(NEW) packages, then we satisfy "normal" dependencies, and finally
we satisfy any dependencies mentioning obsolete packages.
This means for example if you have obsolete libfoo1 and a new
libfoo1t64, that we will see Depends: libfoo1t64 before any
Depends: libfoo1 (which may expand to libfoo1 | libfoo1t64),
so we effectively will have selected "replacement" packages
this way already before getting to older packages where we
would have to choose between the obsolete package and its
replacement.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Our backtracking is chronological, so we will first
try alternative choices or skip optional items in
later groups.
So installing manually installed packages before automatically
installed ones allows manually installed packages to remove
automatically installed packages easily. If we did automatic
packages first, we'd keep back upgrades for manual packages
or change choices for their dependencies, or would have to
backtrack harder to get back to the right decision level.
That's silly.
Ordering automatically installed packages last also allows
us to calculate autoremovable packages. Since we will have
installed all dependencies from manually installed packages
by the point where we get to automatically installed packages,
everything that will be installed in those Auto groups is
inherently garbage.
|
|
|
This is a simple backtracking brute-force solver with heurisitcs,
this initial version has the following known gaps:
- Errors are not kept from branches, the error reporting after
backtracking isn't particularly useful.
- We cannot show automatically removed packages
- We cannot replace packages with others
- We do not have conflict-driven clause learning yet
Untested:
- Multi-arch
This solver is fundamentally different in key aspects:
- It solves smaller dependency groups before larger ones, leading
us to avoid installing A in A|B if B is installed more often and
more consistently.
- It only keeps the automatic packages reachable via the strongest
path. Currently it only implements autoremoval, but not display
of autoremoval as we simply enqueue all automatically installed
packages at the end when not doing automatic removal.
This will need some translation where we Solve() first, and then
Solve() again with the automatically installed packages added such
that we can mark them as Garbage for display purposes.
- It does not remove manually installed packages.
Hook the solver in via the EDSP framework, this allows us to achieve
easy initial integration without lots of issues.
A lot of this work was planned and executed in my free time and then
some leaked into work time I suppose.
Implementation notes:
- Restore the full backlog of items
The annoying thing is that we record only when an item was enqueued
and not the level at which it was installed, so when going back a
decision level we might have to reinstall packages that were queued
at an earlier decision level because they were only installed at a
later decision level.
- When picking one version, reject the others
- Propagate conflicts up to reverse dependencies
This will recursively mark every reverse dependency that can
no longer be satisfied as MUSTNOT.
Also make sure to recursively call Reject(Ver) from Reject(Pkg)
to make sure we trigger the Rejections there.
This means we now end up having Recursion in the algorithm. An
alternative approach would be to push *reject* items to the heap
and then do them, but this is not entirely straight forward and
it may simply not be necessary.
- Sort upgrades before other optional installs containing subsets
If I want to upgrade a package A, I schedule A3|A2|A1; if another
thing depends specifically on A1; we'd not be installed. Hence we
need to sort upgrades first.
This only is needed for optional packages; manual packages will
figure this out naturally.
- Rescoring is lazily implemented. Instead of calling make_heap()
after rescoring items, we just mark the items as dirty and reinsert
them. We also only rescore from the main solve loop, Reject() marks
the heap as needing a rescore due to a Conflict (as some versions will
no longer be installable), and RescoreWorkIfNeeded() then will do the
rescoring.
- Recursive unit propagation: Install() and Reject() recursively call
each other to promote decisions across single-version dependencies
(or across not-anymore satisfiable reverse-depends).
- Make Reason constructors explicit, this enhances readability
This makes calls like the one in here be
Reject(object, Reason(otherObject))
Ensuring that it's clear that the 2nd argument is a reason at the
caller side.
- Split Decision into Decision and Hint vs. first draft
When branching/deciding, we do not want to override SHOULD and MAY.
We do not actually use them yet, and we do actually clean them when
backtracking, but let's at least keep the data structure correct.
Convert the enum to a 16-bit integer so we can still fit in the same
space as before.
|
