From 3523efb15d48ce3c6f9212f50dfc892497ba9dcb Mon Sep 17 00:00:00 2001 From: Julian Andres Klode Date: Sat, 2 Nov 2024 13:55:39 +0100 Subject: solver3: Use a propagation queue 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. --- apt-pkg/solver3.h | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'apt-pkg/solver3.h') diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index 5c67faff2..4f6f83d15 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -132,6 +132,9 @@ class Solver // queue to be concerned about std::vector solved{}; + // \brief Propagation queue + std::queue propQ; + // \brief Current decision level. // // This is an index into the solved vector. @@ -155,6 +158,8 @@ class Solver bool RejectReverseDependencies(pkgCache::VerIterator Ver); // \brief Enqueue a single or group bool EnqueueOrGroup(pkgCache::DepIterator start, pkgCache::DepIterator end, Var reason); + // \brief Propagate all pending propagations + bool Propagate(); // \brief Propagate a "true" value of a variable bool PropagateInstall(Var var); // \brief Propagate a rejection of a variable -- cgit v1.2.3-70-g09d2