Merge branch 'solver3' into 'main'

solver3: Use classical watchers and minor refactorings

See merge request apt-team/apt!548

2 files changed, 89 insertions, 73 deletions

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index a09c27f2a..e4449339e 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -123,8 +123,6 @@ std::string APT::Solver::Clause::toString(pkgCache &cache, bool pretty, bool sho
 std::string Solver::Work::toString(pkgCache &cache) const
 {
    std::ostringstream out;
-   if (erased)
-      out << "Erased ";
    if (clause->optional)
       out << "Optional ";
    out << "Item (" << ssize_t(size <= clause->solutions.size() ? size : -1) << "@" << level << ") ";
@@ -382,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()
@@ -506,11 +516,9 @@ bool Solver::Pop()
       UndoOne();
 
    // We need to remove any work that is at a higher level.
-   // FIXME: We should just mark the entries as erased and only do a compaction
-   //        of the heap once we have a lot of erased entries in it.
    trailLim.pop_back();
    work.erase(std::remove_if(work.begin(), work.end(), [this](Work &w) -> bool
-			     { return w.level > decisionLevel() || w.erased; }),
+			     { return w.level > decisionLevel(); }),
 	      work.end());
    std::make_heap(work.begin(), work.end());
 
@@ -572,9 +580,6 @@ bool Solver::Solve()
       auto item = work.front();
       std::pop_heap(work.begin(), work.end());
       work.pop_back();
-      // This item has been replaced with a new one. Remove it.
-      if (item.erased)
-	 continue;
 
       if (std::any_of(item.clause->solutions.begin(), item.clause->solutions.end(), [this](auto ver)
 		      { return value(ver) == LiftedBool::True; }))
@@ -598,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...
@@ -859,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();
 }
 
@@ -885,7 +894,7 @@ bool DependencySolver::ObsoletedByNewerSourceVersion(pkgCache::VerIterator cand)
       if (priority == 0 || priority < candPriority)
 	 continue;
 
-      pkgObsolete[pkg] = 2;
+      pkgObsolete[pkg] = LiftedBool::True;
       if (debug >= 3)
 	 std::cerr << "Obsolete: " << cand.ParentPkg().FullName() << "=" << cand.VerStr() << " due to " << ver.ParentPkg().FullName() << "=" << ver.VerStr() << "\n";
       return true;
@@ -898,8 +907,8 @@ bool DependencySolver::Obsolete(pkgCache::PkgIterator pkg, bool AllowManual) con
 {
    if ((*this)[pkg].flags.manual && not AllowManual)
       return false;
-   if (pkgObsolete[pkg] != 0)
-      return pkgObsolete[pkg] == 2;
+   if (pkgObsolete[pkg] != LiftedBool::Undefined)
+      return pkgObsolete[pkg] == LiftedBool::True;
 
    auto ver = GetCandidateVer(pkg);
 
@@ -909,7 +918,7 @@ bool DependencySolver::Obsolete(pkgCache::PkgIterator pkg, bool AllowManual) con
    {
       if (debug >= 3)
 	 std::cerr << "Obsolete: " << pkg.FullName() << " - not installable\n";
-      pkgObsolete[pkg] = 2;
+      pkgObsolete[pkg] = LiftedBool::True;
       return true;
    }
 
@@ -921,14 +930,14 @@ bool DependencySolver::Obsolete(pkgCache::PkgIterator pkg, bool AllowManual) con
    {
       if (ver.Downloadable())
       {
-	 pkgObsolete[pkg] = 1;
+	 pkgObsolete[pkg] = LiftedBool::False;
 	 return false;
       }
    }
 
    if (debug >= 3)
       std::cerr << "Obsolete: " << ver.ParentPkg().FullName() << "=" << ver.VerStr() << " - not installable\n";
-   pkgObsolete[pkg] = 2;
+   pkgObsolete[pkg] = LiftedBool::True;
    return true;
 }
 void DependencySolver::Discover(Var var)
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 4a2b4ac8d..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()
@@ -442,7 +447,7 @@ class DependencySolver : public Solver
    bool KeepSuggests{_config->FindB("APT::AutoRemove::SuggestsImportant", true)};
 
    // Helper functions for detecting obsolete packages
-   mutable FastContiguousCacheMap<pkgCache::Package, char> pkgObsolete;
+   mutable FastContiguousCacheMap<pkgCache::Package, LiftedBool> pkgObsolete;
    bool Obsolete(pkgCache::PkgIterator pkg, bool AllowManual = false) const;
    bool ObsoletedByNewerSourceVersion(pkgCache::VerIterator cand) const;
 
@@ -509,9 +514,6 @@ struct APT::Solver::Solver::Work
    /// Number of valid choices at insertion time
    size_t size{0};
 
-   // \brief This item should be removed from the queue.
-   bool erased{false};
-
    bool operator<(APT::Solver::Solver::Work const &b) const;
    std::string toString(pkgCache &cache) const;
    inline Work(const Clause *clause, level_type level) : clause(clause), level(level) {}
@@ -556,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];
 };
 
 /**
@@ -609,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()];
+}