From 3523efb15d48ce3c6f9212f50dfc892497ba9dcb Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
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.cc | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

(limited to 'apt-pkg/solver3.cc')

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)
-- 
cgit v1.2.3-70-g09d2