solver3: Remove work rescoring in favor of unit propagation

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.

2 files changed, 26 insertions, 60 deletions

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index 06008fb5d..945d912db 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -365,9 +365,6 @@ bool APT::Solver::Enqueue(Var var, bool decision, Var reason)
    solved.push_back(Solved{var, std::nullopt});
    propQ.push(var);
 
-   if (not decision)
-      needsRescore = true;
-
    return true;
 }
 
@@ -397,14 +394,36 @@ bool APT::Solver::Propagate()
       {
 	 for (auto rclause : (*this)[var].rclauses)
 	 {
-	    if (rclause->negative || rclause->reason.empty() || rclause->optional ||
-		std::any_of(rclause->solutions.begin(), rclause->solutions.end(), [this](auto var)
-			    { return (*this)[var].decision != Decision::MUSTNOT; }))
+	    if (rclause->negative || rclause->reason.empty())
 	       continue;
-
 	    if ((*this)[rclause->reason].decision == Decision::MUSTNOT)
 	       continue;
 
+	    auto count = std::count_if(rclause->solutions.begin(), rclause->solutions.end(), [this](auto var)
+				       { return (*this)[var].decision != Decision::MUSTNOT; });
+
+	    if (count == 1 && (*this)[rclause->reason].decision == Decision::MUST)
+	    {
+	       if (unlikely(debug >= 3))
+		  std::cerr << "Propagate NOT " << var.toString(cache) << " to unit clause " << rclause->toString(cache);
+	       if (rclause->optional)
+	       {
+		  // Enqueue duplicated item, this will ensure we see it at the correct time
+		  if (not AddWork(Work{rclause, depth()}))
+		     return false;
+	       }
+	       else
+	       {
+		  // Find the variable that must be chosen and enqueue it as a fact
+		  for (auto sol : rclause->solutions)
+		     if ((*this)[sol].decision == Decision::NONE && not Enqueue(sol, true, rclause->reason))
+			return false;
+	       }
+	       continue;
+	    }
+	    if (count >= 1 || rclause->optional)
+	       continue;
+
 	    if (unlikely(debug >= 3))
 	       std::cerr << "Propagate NOT " << var.toString(cache) << " to " << rclause->reason.toString(cache) << " for dep " << const_cast<Clause *>(rclause)->toString(cache) << std::endl;
 
@@ -740,40 +759,6 @@ bool APT::Solver::AddWork(Work &&w)
    return true;
 }
 
-void APT::Solver::RescoreWorkIfNeeded()
-{
-   if (not needsRescore)
-      return;
-
-   needsRescore = false;
-   std::vector<Work> resized;
-   for (auto &w : work)
-   {
-      if (w.erased)
-	 continue;
-      size_t newSize = std::count_if(w.clause->solutions.begin(), w.clause->solutions.end(), [this](auto V)
-				     { return (*this)[V].decision != Decision::MUSTNOT; });
-
-      // Notably we only insert the work into the queue if it got smaller. Work that got larger
-      // we just move around when we get to it too early in Solve(). This reduces memory usage
-      // at the expense of counting each item we see in Solve().
-      if (newSize < w.size)
-      {
-	 Work newWork(w);
-	 newWork.size = newSize;
-	 resized.push_back(std::move(newWork));
-	 w.erased = true;
-      }
-   }
-   if (unlikely(debug >= 2))
-      std::cerr << "Rescored: " << resized.size() << "items\n";
-   for (auto &w : resized)
-   {
-      work.push_back(std::move(w));
-      std::push_heap(work.begin(), work.end());
-   }
-}
-
 bool APT::Solver::Solve()
 {
    startTime = time(nullptr);
@@ -788,8 +773,6 @@ bool APT::Solver::Solve()
       if (work.empty())
 	 break;
 
-      // Rescore the work if we need to
-      RescoreWorkIfNeeded();
       // *NOW* we can pop the item.
       std::pop_heap(work.begin(), work.end());
 
@@ -799,19 +782,6 @@ bool APT::Solver::Solve()
 	 work.pop_back();
 	 continue;
       }
-
-      // If our size increased, queue again.
-      size_t newSize = std::count_if(work.back().clause->solutions.begin(), work.back().clause->solutions.end(), [this](auto V)
-				     { return (*this)[V].decision != Decision::MUSTNOT; });
-
-      if (newSize > work.back().size)
-      {
-	 work.back().size = newSize;
-	 std::push_heap(work.begin(), work.end());
-	 continue;
-      }
-      assert(newSize == work.back().size);
-
       auto item = std::move(work.back());
       work.pop_back();
       solved.push_back(Solved{Var(), item});
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 796f198b1..d4a584f2d 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -193,8 +193,6 @@ class Solver
    // be able to iterate over the queued work and see if a choice would
    // invalidate any work.
    heap<Work> work{};
-   // \brief Whether RescoreWork() actually needs to rescore the work.
-   bool needsRescore{false};
 
    // \brief Backlog of solved work.
    //
@@ -271,8 +269,6 @@ class Solver
    void UndoOne();
    // \brief Add work to our work queue.
    [[nodiscard]] bool AddWork(Work &&work);
-   // \brief Rescore the work after a reject or a pop
-   void RescoreWorkIfNeeded();
 
    // \brief Basic solver initializer. This cannot fail.
    Solver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags);