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.

2 files changed, 29 insertions, 8 deletions

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index a00da5716..6f445328c 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -342,16 +342,23 @@ bool APT::Solver::Enqueue(Var var, bool decision, Var reason)
       std::cerr << "[" << depth() << "] " << (decision ? "Install" : "Reject") << ":" << var.toString(cache) << " (" << WhyStr(state.reason) << ")\n";
 
    solved.push_back(Solved{var, std::nullopt});
+   propQ.push(var);
 
    if (not decision)
-   {
-      if (not PropagateReject(var))
-	 return false;
       needsRescore = true;
-   }
-   else
+
+   return true;
+}
+
+bool APT::Solver::Propagate()
+{
+   while (!propQ.empty())
    {
-      if (not PropagateInstall(var))
+      Var var = propQ.front();
+      propQ.pop();
+      if ((*this)[var].decision == Decision::MUST && not PropagateInstall(var))
+	 return false;
+      else if ((*this)[var].decision == Decision::MUSTNOT && not PropagateReject(var))
 	 return false;
    }
    return true;
@@ -822,8 +829,17 @@ void APT::Solver::RescoreWorkIfNeeded()
 
 bool APT::Solver::Solve()
 {
-   while (not work.empty())
+   while (true)
    {
+      while (not Propagate())
+      {
+	 if (not Pop())
+	    return false;
+      }
+
+      if (work.empty())
+	 break;
+
       // Rescore the work if we need to
       RescoreWorkIfNeeded();
       // *NOW* we can pop the item.
@@ -993,7 +1009,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
       }
    }
 
-   return true;
+   return Propagate();
 }
 
 bool APT::Solver::ToDepCache(pkgDepCache &depcache)
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> solved{};
 
+   // \brief Propagation queue
+   std::queue<Var> 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