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()];
+}