solver3: Use classical watchers for propagation

Instead of tracking dependencies and reverse dependencies,
install classical watchers. This vastly streamlines the
propagation code and allows us to easily switch to literals
in the next step.

This implementation watches _all_ solutions rather than using
the modern 2-watched literals scheme or the intermediate
head/tail watchers.

Ultimately a more effective watcher scheme would be interesting
but not a significant priority seeing as most of the solver runtime
is spent not in propagation but in problem translation.

decision trees
--------------
The new watchers produce slightly different decision trees, sometimes
subtly changing solutions. Notably in various observed examples in
Ubuntu 25.04, courier was installed as an MTA instead of postfix:

The old decision tree was:

    apcupsd:amd64 -> mailutils:amd64=1:3.18-1 -> mailutils:amd64 -> postfix:amd64=3.9.1-10ubuntu1

The new decision tree is:

    lsb:amd64 -> lsb-core:amd64 -> courier-mta:amd64=1.3.13-1

The difference here being that lsb-core declares a mail-transport-agent
dependency whereas mailutils depends on `default-mta | mail-transport-agency`;
but both are effectively subject to selection at similar time.

Further work is needed to optimize selection. A notable choice may also
be to deal with broken packages like lsb-core that declare dependencies
solely on a virtual package by reconstructing the default provider for
that package utilizing default-* dependencies or similar notions.

Likewise in the test suite, explanations are different in some
uninstallable cases.

backtracking
~~~~~~~~~~~~
The following major changes were observed in the 25.04 test suite:

-tmp/regression-remove/07f0a068-36c2-11f0-b7c1-fa163e171f02:18
+tmp/regression-remove/07f0a068-36c2-11f0-b7c1-fa163e171f02:3

-tmp/regression-remove/32078f70-3734-11f0-a75a-fa163ec8ca8c:64
+tmp/regression-remove/32078f70-3734-11f0-a75a-fa163ec8ca8c:19

Other test cases showed little deviation, +/- 1, generally
the same amount of backtracking.

performance
~~~~~~~~~~~
Running Ubuntu's regression test suite resulted in no significant
performance difference being observable.

Before: 290s user time; 16.66% solver
After:  299s user time; 17.36% solver

Tests where run with make -j 8 and solver performance extracted

    perf report --symbol-filter=ResolveExternal --stdio

2 files changed, 81 insertions, 55 deletions

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index cbe318ac7..e4449339e 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -380,65 +380,77 @@ bool Solver::Propagate()
    {
       Var var = propQ.front();
       propQ.pop();
-      if (value(var) == LiftedBool::True)
+
+      // Stale propagation. These do not happen in MiniSat, because it clears the propQ on
+      // conflict, however, we simply keep the item in here and skip it.
+      if (value(var) == LiftedBool::Undefined)
+	 continue;
+
+      Lit lit = value(var) == LiftedBool::False ? ~var : var;
+      if (not lit.sign())
+	 Discover(lit.var());
+
+      for (auto clause : watches(lit))
       {
-	 Discover(var);
-	 for (auto &clause : (*this)[var].clauses)
-	    if (not AddWork(Work{clause.get(), decisionLevel()}))
-	       return false;
-	 for (auto rclause : (*this)[var].rclauses)
-	 {
-	    if (not rclause->negative || rclause->optional || rclause->reason.empty())
-	       continue;
-	    if (unlikely(debug >= 3))
-	       std::cerr << "Propagate " << var.toString(cache) << " to NOT " << rclause->reason.toString(cache) << " for dep " << const_cast<Clause *>(rclause)->toString(cache) << std::endl;
-	    if (not Enqueue(~rclause->reason, rclause))
-	       return false;
-	 }
+	 if (Propagate(clause, lit))
+	    continue;
+	 return false;
       }
-      else if (value(var) == LiftedBool::False)
-      {
-	 for (auto rclause : (*this)[var].rclauses)
-	 {
-	    if (rclause->negative || rclause->reason.empty())
-	       continue;
-	    if (value(rclause->reason) == LiftedBool::False)
-	       continue;
+   }
+   return true;
+}
 
-	    auto count = std::count_if(rclause->solutions.begin(), rclause->solutions.end(), [this](auto var)
-				       { return value(var) != LiftedBool::False; });
+bool Solver::Propagate(const Clause *clause, Lit p)
+{
+   if (debug >= 3)
+      std::cerr << "Propagate " << p.toString(cache) << " to " << clause->toString(cache) << std::endl;
+   // Negative clauses are trivial
+   if (clause->negative)
+   {
+      // One of the solutions was set, so reject the reason
+      if (p != clause->reason)
+	 return Enqueue(~clause->reason, clause);
 
-	    if (count == 1 && value(rclause->reason) == LiftedBool::True)
-	    {
-	       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, decisionLevel()}))
-		     return false;
-	       }
-	       else
-	       {
-		  // Find the variable that must be chosen and enqueue it as a fact
-		  for (auto sol : rclause->solutions)
-		     if (value(sol) == LiftedBool::Undefined && not Enqueue(sol, rclause))
-			return false;
-	       }
-	       continue;
-	    }
-	    if (count >= 1 || rclause->optional)
-	       continue;
+      // Here we need to reject all conflicting solutions (reason -> none of solutions)
+      for (auto sol : clause->solutions)
+	 if (not Enqueue(~sol, clause))
+	    return false;
 
-	    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;
+      return true;
+   }
 
-	    if (not Enqueue(~rclause->reason, rclause)) // Last version invalidated
-	       return false;
-	 }
+   // Check if the clause is unit, conflict, or undecided
+   Lit unit;
+   for (auto sol : clause->solutions)
+   {
+      if (value(sol) == LiftedBool::False)
+	 continue;
+      if (not unit.empty() || clause->optional)
+      {
+	 // We found a second solution, so we are undecided
+	 if (p == clause->reason)
+	    return AddWork(Work{clause, decisionLevel()});
+	 return true;
       }
+
+      unit = sol;
+   }
+
+   // The clause is now either unit or conflict
+   if (not unit.empty())
+   {
+      // Unit clause. If it is an active clause, enqueue the unit literal.
+      if (value(clause->reason) == LiftedBool::True)
+         return Enqueue(unit, clause);
+      return true;
+   }
+   else
+   {
+      // Conflict clause. If this clause is non-optional; reject it's "reason".
+      if (not clause->optional)
+	 return Enqueue(~clause->reason, clause);
+      return true;
    }
-   return true;
 }
 
 void Solver::UndoOne()
@@ -591,6 +603,7 @@ bool Solver::Solve()
       }
       else
       {
+	 abort();
 	 if (unlikely(debug >= 1))
 	    std::cerr << item.toString(cache) << "\n";
 	 // Enqueue produces the right error message for us here, given that reason has been assigned true already...
@@ -852,8 +865,11 @@ const Clause *DependencySolver::RegisterClause(Clause &&clause)
 
    clauses.push_back(std::make_unique<Clause>(std::move(clause)));
    auto const &inserted = clauses.back();
-   for (auto var : inserted->solutions)
-      (*this)[var].rclauses.push_back(inserted.get());
+   // Insert all our watches
+   if (not inserted->reason.empty())
+      watches(inserted->reason).push_back(inserted.get());
+   for (auto sol : inserted->solutions)
+      watches(inserted->negative ? sol : ~sol).push_back(inserted.get());
    return inserted.get();
 }
 
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index a3ec859bb..af1d749eb 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -200,6 +200,7 @@ struct Lit
    int32_t value;
 
    public:
+   constexpr Lit() : value{0} {}
    // SAFETY: value must be 31 bit, one bit is needed for the sign.
    constexpr Lit(Var var) : value{static_cast<int32_t>(var.value)} {}
 
@@ -328,6 +329,8 @@ class Solver
    inline State &operator[](Var r);
    inline const State &operator[](Var r) const;
 
+   inline std::vector<const Clause *> &watches(Lit lit);
+
    // \brief Heap of the remaining work.
    //
    // In contrast to MiniSAT which picks undecided literals and decides them,
@@ -364,6 +367,8 @@ class Solver
    virtual void Discover(Var var) = 0;
    // \brief Propagate all pending propagations
    [[nodiscard]] bool Propagate();
+   // \brief Propagate all pending propagations
+   [[nodiscard]] bool Propagate(const Clause *clause, Lit lit);
 
    // \brief Return the current level (.size() with casting)
    level_type decisionLevel()
@@ -553,8 +558,8 @@ struct APT::Solver::Solver::State
 
    // \brief Clauses owned by this package/version
    std::vector<std::unique_ptr<Clause>> clauses;
-   // \brief Reverse clauses, that is dependencies (or conflicts) from other packages on this one
-   std::vector<const Clause *> rclauses;
+   // \brief Watches watching a clause by sign
+   std::vector<const Clause *> watches[2];
 };
 
 /**
@@ -606,3 +611,8 @@ struct std::hash<APT::Solver::Lit>
    std::hash<decltype(APT::Solver::Lit::value)> hash_value;
    std::size_t operator()(const APT::Solver::Lit &v) const noexcept { return hash_value(v.value); }
 };
+
+inline std::vector<const APT::Solver::Clause *> &APT::Solver::Solver::watches(Lit lit)
+{
+   return (*this)[lit.var()].watches[lit.sign()];
+}