From f870bd44522d195199987b0e073d495eed060495 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Wed, 5 Feb 2025 20:11:35 +0100
Subject: solver3: Defer version selection where possible

If a dependency can be satisfied by all versions of a package,
add the package to the clause instead of the version object.

This works only if there are no providers for the package: Providers
are quite hard to enumerate over and make sure that all versions of
a package satisfy the provider dependency.

Implement arbitrary selection between packages and versions for
the CompareProviders class: We pick the best version for each package
and then pit them against each other.
---
 apt-pkg/solver3.h | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 65cd9f017..e43e1065c 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -228,6 +228,8 @@ class Solver
    bool StrictPinning{_config->FindB("APT::Solver::Strict-Pinning", true)};
    // \brief If set, we install missing recommends and pick new best packages.
    bool FixPolicyBroken{_config->FindB("APT::Get::Fix-Policy-Broken")};
+   // \brief If set, we use strict pinning.
+   bool DeferVersionSelection{_config->FindB("APT::Solver::Defer-Version-Selection", true)};
 
    // \brief Discover a variable, translating the underlying dependencies to the SAT presentation
    void Discover(Var var);
-- 
cgit v1.2.3-70-g09d2


From 222271ee0d44c8e7bc00935fbbc2615529a4cdfc Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Mon, 10 Feb 2025 17:17:35 +0100
Subject: solver3: Discover recursive dependencies

When we have discovered all clauses for a version, discover
each possible solution for the clauses. This means that when
Discover(foo) is called _anything_ that could lead to foo becoming
uninstallable is translated; so we can extend this next by keeping
a list of reverse dependencies for each package and rejecting
those.

We limit the discovery to those variables that we did not already
enqueue as a negative fact at the root level, as those can never
become true.

We are utilizing a queue here which is not the most performant
solution possible, but where it excels is in producing usable
stack traces when debugging. Traversing the entire dependency
tree using recursion can easily produce thousand levels of
recursion.

The queue means that we discover packages in a breadth-first
manner compatible with the order in which we propagate dependencies,
which is helpful for consistency.

The queue did not appear as a bottleneck in benchmarking. If it did,
we could switch to a grow-only ring buffer (std::queue's underlying
deque also shrinks automatically which is suboptimal).
---
 apt-pkg/solver3.cc                                 | 79 +++++++++++++---------
 apt-pkg/solver3.h                                  |  5 ++
 ...est-bug-549968-install-depends-of-not-installed |  1 -
 3 files changed, 52 insertions(+), 33 deletions(-)

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

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index ed781df13..b4a69d844 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -396,51 +396,66 @@ void APT::Solver::RegisterClause(Clause &&clause)
 
 void APT::Solver::Discover(Var var)
 {
-   auto &state = (*this)[var];
-
-   if (state.flags.discovered)
-      return;
-
-   state.flags.discovered = true;
+   assert(discoverQ.empty());
+   discoverQ.push(var);
 
-   if (auto Pkg = var.Pkg(cache); not Pkg.end())
+   while (not discoverQ.empty())
    {
-      Clause clause{Var(Pkg), Group::SelectVersion};
-      for (auto ver = Pkg.VersionList(); not ver.end(); ver++)
-	 clause.solutions.push_back(Var(ver));
+      var = discoverQ.front();
+      discoverQ.pop();
 
-      std::stable_sort(clause.solutions.begin(), clause.solutions.end(), CompareProviders3{cache, policy, Pkg, *this});
-      RegisterClause(std::move(clause));
+      auto &state = (*this)[var];
 
-      RegisterCommonDependencies(Pkg);
-   }
-   else if (auto Ver = var.Ver(cache); not Ver.end())
-   {
-      Clause clause{Var(Ver), Group::SelectVersion};
-      clause.solutions = {Var(Ver.ParentPkg())};
-      RegisterClause(std::move(clause));
+      if (state.flags.discovered)
+	 continue;
+
+      state.flags.discovered = true;
 
-      for (auto OV = Ver.ParentPkg().VersionList(); not OV.end(); ++OV)
+      if (auto Pkg = var.Pkg(cache); not Pkg.end())
       {
-	 if (OV == Ver)
-	    continue;
+	 Clause clause{Var(Pkg), Group::SelectVersion};
+	 for (auto ver = Pkg.VersionList(); not ver.end(); ver++)
+	    clause.solutions.push_back(Var(ver));
 
-	 Clause clause{Var(Ver), Group::SelectVersion, false, true /* negative */};
-	 clause.solutions = {Var(OV)};
+	 std::stable_sort(clause.solutions.begin(), clause.solutions.end(), CompareProviders3{cache, policy, Pkg, *this});
 	 RegisterClause(std::move(clause));
-      }
 
-      for (auto dep = Ver.DependsList(); not dep.end();)
+	 RegisterCommonDependencies(Pkg);
+      }
+      else if (auto Ver = var.Ver(cache); not Ver.end())
       {
-	 // Compute a single dependency element (glob or)
-	 pkgCache::DepIterator start;
-	 pkgCache::DepIterator end;
-	 dep.GlobOr(start, end); // advances dep
+	 Clause clause{Var(Ver), Group::SelectVersion};
+	 clause.solutions = {Var(Ver.ParentPkg())};
+	 RegisterClause(std::move(clause));
 
-	 auto clause = TranslateOrGroup(start, end, Var(Ver));
+	 for (auto OV = Ver.ParentPkg().VersionList(); not OV.end(); ++OV)
+	 {
+	    if (OV == Ver)
+	       continue;
 
-	 RegisterClause(std::move(clause));
+	    Clause clause{Var(Ver), Group::SelectVersion, false, true /* negative */};
+	    clause.solutions = {Var(OV)};
+	    RegisterClause(std::move(clause));
+	 }
+
+	 for (auto dep = Ver.DependsList(); not dep.end();)
+	 {
+	    // Compute a single dependency element (glob or)
+	    pkgCache::DepIterator start;
+	    pkgCache::DepIterator end;
+	    dep.GlobOr(start, end); // advances dep
+
+	    auto clause = TranslateOrGroup(start, end, Var(Ver));
+
+	    RegisterClause(std::move(clause));
+	 }
       }
+
+      // Recursively discover everything else that is not already FALSE by fact (MUSTNOT at depth 0)
+      for (auto const &clause : state.clauses)
+	 for (auto const &var : clause->solutions)
+	    if ((*this)[var].decision != Decision::MUSTNOT || (*this)[var].depth > 0)
+	       discoverQ.push(var);
    }
 }
 
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index e43e1065c..34da03ea0 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -205,6 +205,8 @@ class Solver
 
    // \brief Propagation queue
    std::queue<Var> propQ;
+   // \brief Discover variables
+   std::queue<Var> discoverQ;
 
    // \brief Current decision level.
    //
@@ -232,6 +234,9 @@ class Solver
    bool DeferVersionSelection{_config->FindB("APT::Solver::Defer-Version-Selection", true)};
 
    // \brief Discover a variable, translating the underlying dependencies to the SAT presentation
+   //
+   // This does a breadth-first search of the entire dependency tree of var,
+   // utilizing the discoverQ above.
    void Discover(Var var);
    // \brief Link a clause into the watchers
    void RegisterClause(Clause &&clause);
diff --git a/test/integration/test-bug-549968-install-depends-of-not-installed b/test/integration/test-bug-549968-install-depends-of-not-installed
index 7c4e76fd9..6b5e31eea 100755
--- a/test/integration/test-bug-549968-install-depends-of-not-installed
+++ b/test/integration/test-bug-549968-install-depends-of-not-installed
@@ -37,7 +37,6 @@ Solving dependencies...Install coolstuff:i386 ()
 Delete extracoolstuff:i386
 [0] Reject:extracoolstuff:i386 ()
 [0] Install:coolstuff:i386 (coolstuff:i386=1.0)
-[0] Reject:extracoolstuff:i386=1.0 (not extracoolstuff:i386)
 Optional Item (0@0) coolstuff:i386=1.0 ->  | extracoolstuff:i386
 Optional Item (0@0) coolstuff:i386 ->  | extracoolstuff:i386
 
-- 
cgit v1.2.3-70-g09d2


From a9587b39ea6776b1d1324288786176102f65cee5 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Mon, 10 Feb 2025 19:56:16 +0100
Subject: solver3: Implement a timeout, default 10s

A SAT solver can run more or less forever, but that's not a good
user experience.
---
 apt-pkg/solver3.cc           | 8 +++++++-
 apt-pkg/solver3.h            | 5 +++++
 doc/examples/configure-index | 1 +
 3 files changed, 13 insertions(+), 1 deletion(-)

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

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index b4a69d844..d363cdee7 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -32,8 +32,9 @@
 #include <apt-pkg/solver3.h>
 #include <apt-pkg/version.h>
 
-#include <algorithm>
 #include <cassert>
+#include <chrono>
+#include <ctime>
 #include <sstream>
 
 // FIXME: Helpers stolen from DepCache, please give them back.
@@ -740,6 +741,10 @@ bool APT::Solver::Pop()
       for (std::string msg; _error->PopMessage(msg);)
 	 std::cerr << "Branch failed: " << msg << std::endl;
 
+   time_t now = time(nullptr);
+   if (now - startTime >= Timeout)
+      return _error->Error("Solver timed out.");
+
    _error->RevertToStack();
 
    assert(choices.back() < solved.size());
@@ -834,6 +839,7 @@ void APT::Solver::RescoreWorkIfNeeded()
 
 bool APT::Solver::Solve()
 {
+   startTime = time(nullptr);
    while (true)
    {
       while (not Propagate())
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 34da03ea0..da75179d5 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -213,6 +213,9 @@ class Solver
    // This is an index into the solved vector.
    std::vector<depth_type> choices{};
 
+   // \brief The time we called Solve()
+   time_t startTime;
+
    /// Various configuration options
    // \brief Debug level
    int debug{_config->FindI("Debug::APT::Solver")};
@@ -232,6 +235,8 @@ class Solver
    bool FixPolicyBroken{_config->FindB("APT::Get::Fix-Policy-Broken")};
    // \brief If set, we use strict pinning.
    bool DeferVersionSelection{_config->FindB("APT::Solver::Defer-Version-Selection", true)};
+   // \brief If set, we use strict pinning.
+   int Timeout{_config->FindI("APT::Solver::Timeout", 10)};
 
    // \brief Discover a variable, translating the underlying dependencies to the SAT presentation
    //
diff --git a/doc/examples/configure-index b/doc/examples/configure-index
index 1573eaa8b..8476d733a 100644
--- a/doc/examples/configure-index
+++ b/doc/examples/configure-index
@@ -703,6 +703,7 @@ apt::solver::upgrade "<BOOL>";
 apt::solver::remove "<BOOL>";
 apt::solver::removemanual "<BOOL>";
 apt::solver::install "<BOOL>";
+apt::solver::timeout "<INT>";
 apt::keep-downloaded-packages "<BOOL>";
 apt::solver "<STRING>";
 apt::planner "<STRING>";
-- 
cgit v1.2.3-70-g09d2


From b8918cb89ada945d92c720446177f1ef5185b5a5 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Wed, 5 Feb 2025 21:31:53 +0100
Subject: solver3: Reject reverse dependencies natively

Instead of utilizing the reverse depends functionality of the cache
and marking all possible reverse dependencies for removal, mark them
ourselves by keeping track of reverse-implication-clauses.

Notably, this improves the reverse dependency rejection substantially:
The previous RejectReverseDependencies() function did not handle
Provides.

For this to work correctly right now, we need to discover optional
clauses too when queuing them. This is somewhat suboptimal as we
technically we don't care if they become unsat, we just waste time
tracking them.

The tests get a bit awkward, but oh well, we use what we can
use.
---
 apt-pkg/solver3.cc                                 | 132 ++++-----------------
 apt-pkg/solver3.h                                  |   6 +-
 test/integration/test-apt-get-build-dep-barbarian  |   6 +-
 test/integration/test-apt-never-markauto-sections  |   2 +-
 .../test-bug-618848-always-respect-user-requests   |   2 +-
 test/integration/test-multiarch-allowed            |  12 +-
 .../test-prefer-higher-priority-providers          |   5 +-
 7 files changed, 37 insertions(+), 128 deletions(-)

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

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index d363cdee7..2d9e92c99 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -383,8 +383,25 @@ bool APT::Solver::Propagate()
 	    if (not AddWork(Work{clause.get(), depth()}))
 	       return false;
       }
-      else if ((*this)[var].decision == Decision::MUSTNOT && not PropagateReject(var))
-	 return false;
+      else if ((*this)[var].decision == Decision::MUSTNOT)
+      {
+	 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; }))
+	       continue;
+
+	    if ((*this)[rclause->reason].decision == Decision::MUSTNOT)
+	       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;
+
+	    if (not Enqueue(rclause->reason, false, var)) // Last version invalidated
+	       return false;
+	 }
+      }
    }
    return true;
 }
@@ -393,6 +410,9 @@ void APT::Solver::RegisterClause(Clause &&clause)
 {
    auto &clauses = (*this)[clause.reason].clauses;
    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());
 }
 
 void APT::Solver::Discover(Var var)
@@ -460,43 +480,6 @@ void APT::Solver::Discover(Var var)
    }
 }
 
-bool APT::Solver::PropagateReject(Var var)
-{
-   if (auto Pkg = var.Pkg(cache); not Pkg.end())
-   {
-      for (auto ver = Pkg.VersionList(); not ver.end(); ver++)
-	 if (not Enqueue(Var(ver), false, Var(Pkg)))
-	    return false;
-   }
-   else if (auto Ver = var.Ver(cache); not Ver.end())
-   {
-      if (auto pkg = Ver.ParentPkg(); (*this)[pkg].decision != Decision::MUSTNOT)
-      {
-	 bool anyInstallable = false;
-	 for (auto otherVer = pkg.VersionList(); not otherVer.end(); otherVer++)
-	    if (otherVer->ID != Ver->ID && (*this)[otherVer].decision != Decision::MUSTNOT)
-	       anyInstallable = true;
-
-	 if (anyInstallable)
-	    ;
-	 else if ((*this)[pkg].decision == Decision::MUST) // Must install, but none available
-	 {
-	    _error->Error("Conflict: %s but no versions are installable",
-			  WhyStr(Var(pkg)).c_str());
-	    for (auto otherVer = pkg.VersionList(); not otherVer.end(); otherVer++)
-	       if ((*this)[otherVer].decision == Decision::MUSTNOT)
-		  _error->Error("Uninstallable version: %s", WhyStr(Var(otherVer)).c_str());
-	    return _error->Error("Uninstallable version: %s", WhyStr(Var(Ver)).c_str());
-	 }
-	 else if (not Enqueue(Var(Ver.ParentPkg()), false, Var(Ver))) // Last version invalidated
-	    return false;
-      }
-      if (not RejectReverseDependencies(Ver))
-	 return false;
-   }
-   return true;
-}
-
 void APT::Solver::RegisterCommonDependencies(pkgCache::PkgIterator Pkg)
 {
    for (auto dep = Pkg.VersionList().DependsList(); not dep.end();)
@@ -618,73 +601,6 @@ APT::Solver::Clause APT::Solver::TranslateOrGroup(pkgCache::DepIterator start, p
    return clause;
 }
 
-// \brief Find the or group containing the given dependency.
-static void FindOrGroup(pkgCache::DepIterator const &D, pkgCache::DepIterator &start, pkgCache::DepIterator &end)
-{
-   for (auto dep = D.ParentVer().DependsList(); not dep.end();)
-   {
-      dep.GlobOr(start, end); // advances dep
-
-      for (auto member = start;;)
-      {
-	 if (member == D)
-	    return;
-	 if (member == end)
-	    break;
-	 member++;
-      }
-   }
-
-   _error->Fatal("Found a dependency that does not exist in its parent version");
-   abort();
-}
-
-// This is the opposite of EnqueueOrDependencies, it rejects the reverse dependencies of the
-// given version iterator.
-bool APT::Solver::RejectReverseDependencies(pkgCache::VerIterator Ver)
-{
-   // This checks whether an or group is still satisfiable.
-   auto stillPossible = [this](pkgCache::DepIterator start, pkgCache::DepIterator end)
-   {
-      while (1)
-      {
-	 std::unique_ptr<pkgCache::Version *[]> Ts{start.AllTargets()};
-	 for (size_t i = 0; Ts[i] != nullptr; ++i)
-	    if ((*this)[Ts[i]].decision != Decision::MUSTNOT)
-	       return true;
-
-	 if (start == end)
-	    return false;
-
-	 start++;
-      }
-   };
-
-   for (auto RD = Ver.ParentPkg().RevDependsList(); not RD.end(); ++RD)
-   {
-      auto RDV = RD.ParentVer();
-      if (RD.IsNegative() || not RD.IsCritical() || not RD.IsSatisfied(Ver))
-	 continue;
-
-      if ((*this)[RDV].decision == Decision::MUSTNOT)
-	 continue;
-
-      pkgCache::DepIterator start;
-      pkgCache::DepIterator end;
-      FindOrGroup(RD, start, end);
-
-      if (stillPossible(start, end))
-	 continue;
-
-      if (unlikely(debug >= 3))
-	 std::cerr << "Propagate NOT " << Ver.ParentPkg().FullName() << "=" << Ver.VerStr() << " to " << RDV.ParentPkg().FullName() << "=" << RDV.VerStr() << " for dependency group starting with" << start.TargetPkg().FullName() << std::endl;
-
-      if (not Enqueue(Var(RDV), false, Var(Ver)))
-	 return false;
-   }
-   return true;
-}
-
 void APT::Solver::Push(Work work)
 {
    if (unlikely(debug >= 2))
@@ -1019,6 +935,10 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
 	    RegisterClause(std::move(shortcircuit));
 	    if (not AddWork(Work{rootState->clauses.back().get(), depth()}))
 	       return false;
+
+	    // Discovery here is needed so the shortcircuit clause can actually become unit.
+	    if (P.VersionList() && P.VersionList()->NextVer)
+	       Discover(Var(P));
 	 }
       }
    }
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index da75179d5..91b852c98 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -248,14 +248,10 @@ class Solver
    // \brief Enqueue dependencies shared by all versions of the package.
    void RegisterCommonDependencies(pkgCache::PkgIterator Pkg);
 
-   // \brief Reject reverse dependencies. Must call std::make_heap() after.
-   [[nodiscard]] bool RejectReverseDependencies(pkgCache::VerIterator Ver);
    // \brief Translate an or group into a clause object
    [[nodiscard]] Clause TranslateOrGroup(pkgCache::DepIterator start, pkgCache::DepIterator end, Var reason);
    // \brief Propagate all pending propagations
    [[nodiscard]] bool Propagate();
-   // \brief Propagate a rejection of a variable
-   [[nodiscard]] bool PropagateReject(Var var);
 
    // \brief Return the current depth (choices.size() with casting)
    depth_type depth()
@@ -470,6 +466,8 @@ struct APT::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;
 };
 
 /**
diff --git a/test/integration/test-apt-get-build-dep-barbarian b/test/integration/test-apt-get-build-dep-barbarian
index b8ab1211b..e070e96ca 100755
--- a/test/integration/test-apt-get-build-dep-barbarian
+++ b/test/integration/test-apt-get-build-dep-barbarian
@@ -83,7 +83,7 @@ testsuccessequal "$(installsfoosamey 'amd64' 'i386')" apt build-dep cool-foo -s
 testsuccessequal "$(installsfoosamey 'i386' 'i386')" apt build-dep bad-amd64-foo -s -a i386
 testsuccessequal "$(installsfoosamey 'amd64' 'i386')" apt build-dep bad-armel-foo -s -a i386
 testsuccessequal "$(installsfoosamey 'i386' 'i386')" apt build-dep bad-amd64-armel-foo -s -a i386
-testfailuremsg 'E: Conflict: builddeps:bad-amd64-i386-foo:i386=1 -> not foo:i386=1 -> not builddeps:bad-amd64-i386-foo:i386=1 but builddeps:bad-amd64-i386-foo:i386=1'  apt build-dep bad-amd64-i386-foo -s -a i386 --solver 3.0
+testfailuremsg 'E: Conflict: builddeps:bad-amd64-i386-foo:i386=1 -> not foo:amd64=1 -> not builddeps:bad-amd64-i386-foo:i386=1 but builddeps:bad-amd64-i386-foo:i386=1'  apt build-dep bad-amd64-i386-foo -s -a i386 --solver 3.0
 testfailureequal 'Reading package lists...
 Reading package lists...
 Building dependency tree...
@@ -96,7 +96,7 @@ The following information may help to resolve the situation:
 The following packages have unmet dependencies:
  builddeps:bad-amd64-i386-foo:i386 : Depends: foo:i386
 E: Unable to correct problems, you have held broken packages.' apt build-dep bad-amd64-i386-foo -s -a i386 --solver internal
-testfailuremsg 'E: Conflict: builddeps:bad-amd64-i386-armel-foo:i386=1 -> not foo:i386=1 -> not builddeps:bad-amd64-i386-armel-foo:i386=1 but builddeps:bad-amd64-i386-armel-foo:i386=1' apt build-dep bad-amd64-i386-armel-foo -s -a i386 --solver 3.0
+testfailuremsg 'E: Conflict: builddeps:bad-amd64-i386-armel-foo:i386=1 -> not foo:amd64=1 -> not builddeps:bad-amd64-i386-armel-foo:i386=1 but builddeps:bad-amd64-i386-armel-foo:i386=1' apt build-dep bad-amd64-i386-armel-foo -s -a i386 --solver 3.0
 testfailureequal 'Reading package lists...
 Reading package lists...
 Building dependency tree...
@@ -115,7 +115,7 @@ testsuccessequal "$(installsfoosamey 'i386' 'armel')" apt build-dep bad-amd64-fo
 testsuccessequal "$(installsfoosamey 'amd64' 'armel')" apt build-dep bad-armel-foo -s -a armel
 testsuccessequal "$(installsfoosamey 'i386' 'armel')" apt build-dep bad-amd64-armel-foo -s -a armel
 testsuccessequal "$(installsfoosamey 'armel' 'armel')" apt build-dep bad-amd64-i386-foo -s -a armel
-FAILUREMSG="E: Conflict: builddeps:bad-amd64-i386-armel-foo:armel=1 -> not foo:armel=1 -> not builddeps:bad-amd64-i386-armel-foo:armel=1 but builddeps:bad-amd64-i386-armel-foo:armel=1"
+FAILUREMSG="E: Conflict: builddeps:bad-amd64-i386-armel-foo:armel=1 -> not foo:amd64=1 -> not builddeps:bad-amd64-i386-armel-foo:armel=1 but builddeps:bad-amd64-i386-armel-foo:armel=1"
 FAILURE='Reading package lists...
 Building dependency tree...
 Some packages could not be installed. This may mean that you have
diff --git a/test/integration/test-apt-never-markauto-sections b/test/integration/test-apt-never-markauto-sections
index e60a6e648..4d7324b02 100755
--- a/test/integration/test-apt-never-markauto-sections
+++ b/test/integration/test-apt-never-markauto-sections
@@ -49,7 +49,7 @@ Remv foreignpkg:i386 [1]
 Remv nosection [1]
 Remv texteditor [1]' aptget autoremove mydesktop -s
 
-testfailuremsg 'E: Conflict: not texteditor:amd64 -> not texteditor:amd64=1 -> not mydesktop-core:amd64=1 but mydesktop:amd64 -> mydesktop-core:amd64 -> mydesktop-core:amd64=1' aptget autoremove texteditor -s --solver 3.0 #-o Debug::pkgDepCache::AutoInstall=1 -o Debug::pkgProblemResolver=1 -o Debug::pkgDepCache::Marker=1
+testfailuremsg 'E: Conflict: not texteditor:amd64 -> not bad-texteditor:amd64 -> not mydesktop-core:amd64 but mydesktop:amd64 -> mydesktop-core:amd64' aptget autoremove texteditor -s --solver 3.0 #-o Debug::pkgDepCache::AutoInstall=1 -o Debug::pkgProblemResolver=1 -o Debug::pkgDepCache::Marker=1
 testsuccessequal 'Reading package lists...
 Building dependency tree...
 Reading state information...
diff --git a/test/integration/test-bug-618848-always-respect-user-requests b/test/integration/test-bug-618848-always-respect-user-requests
index 8ba750b44..d59491af6 100755
--- a/test/integration/test-bug-618848-always-respect-user-requests
+++ b/test/integration/test-bug-618848-always-respect-user-requests
@@ -14,7 +14,7 @@ insertpackage 'unstable' 'exim4-daemon-heavy' 'all' '1.0' 'Depends: libdb4.8'
 setupaptarchive
 
 # This does not work in 3.0 solver: We do not remove manually installed packages.
-testfailuremsg "E: Conflict: exim4-daemon-light:i386 -> libdb4.8:i386 but not libdb4.8:i386" aptget remove libdb4.8 --solver 3.0 -s
+testfailuremsg "E: Conflict: not libdb4.8:i386 -> not exim4-daemon-light:i386 but exim4-daemon-light:i386" aptget remove libdb4.8 --solver 3.0 -s
 allowremovemanual
 testsuccessequal "Reading package lists...
 Building dependency tree...
diff --git a/test/integration/test-multiarch-allowed b/test/integration/test-multiarch-allowed
index 9fc49275a..fb8cb653d 100755
--- a/test/integration/test-multiarch-allowed
+++ b/test/integration/test-multiarch-allowed
@@ -64,24 +64,18 @@ Inst needsfoo:i386 (1 unstable [i386])
 Conf foo:i386 (1 unstable [i386])
 Conf needsfoo:i386 (1 unstable [i386])' aptget install needsfoo:i386 -s
 # FIXME: same problem, but two different unmet dependency messages depending on install order
-testfailuremsg "E: Conflict: needsfoo:i386=1 -> foo:i386 but no versions are installable
-E: Uninstallable version: foo:amd64=1 -> not foo:i386=1
-E: Uninstallable version: foo:amd64=1 -> not foo:i386=1" aptget install needsfoo:i386 foo:amd64 -s --solver 3.0
+testfailuremsg "E: Conflict: foo:amd64=1 -> not foo:i386=1 -> not foo:i386 but needsfoo:i386=1 -> foo:i386" aptget install needsfoo:i386 foo:amd64 -s --solver 3.0
 testfailureequal "$BADPREFIX
 The following packages have unmet dependencies:
  foo : Conflicts: foo:i386 but 1 is to be installed
  foo:i386 : Conflicts: foo but 1 is to be installed
 E: Unable to correct problems, you have held broken packages." aptget install needsfoo:i386 foo:amd64 -s --solver internal
-testfailuremsg "E: Conflict: needsfoo:i386=1 -> foo:i386 but no versions are installable
-E: Uninstallable version: foo:amd64=1 -> not foo:i386=1
-E: Uninstallable version: foo:amd64=1 -> not foo:i386=1" aptget install foo:amd64 needsfoo:i386 -s --solver 3.0
+testfailuremsg "E: Conflict: foo:amd64=1 -> not foo:i386=1 -> not foo:i386 but needsfoo:i386=1 -> foo:i386" aptget install foo:amd64 needsfoo:i386 -s --solver 3.0
 testfailureequal "$BADPREFIX
 The following packages have unmet dependencies:
  needsfoo:i386 : Depends: foo:i386 but it is not installable
 E: Unable to correct problems, you have held broken packages." aptget install foo:amd64 needsfoo:i386 -s --solver internal
-testfailuremsg "E: Conflict: needsfoo:amd64=1 -> foo:amd64 but no versions are installable
-E: Uninstallable version: foo:i386=1 -> not foo:amd64=1
-E: Uninstallable version: foo:i386=1 -> not foo:amd64=1" aptget install needsfoo foo:i386 -s --solver 3.0
+testfailuremsg "E: Conflict: foo:i386=1 -> not foo:amd64=1 -> not foo:amd64 but needsfoo:amd64=1 -> foo:amd64" aptget install needsfoo foo:i386 -s --solver 3.0
 testfailureequal "$BADPREFIX
 The following packages have unmet dependencies:
  foo : Conflicts: foo:i386 but 1 is to be installed
diff --git a/test/integration/test-prefer-higher-priority-providers b/test/integration/test-prefer-higher-priority-providers
index 5fed20a59..76a03b3fb 100755
--- a/test/integration/test-prefer-higher-priority-providers
+++ b/test/integration/test-prefer-higher-priority-providers
@@ -91,10 +91,7 @@ Inst awesome (1 unstable [all])
 Conf baz (1 unstable [all])
 Conf awesome (1 unstable [all])" aptget install awesome foo- bar- -s
 
-testfailuremsg "E: Unsatisfiable dependency: awesome:$native=1 -> foo:$native=1 | bar:$native=1 | baz:$native=1
-E: Not considered: foo:$native=1: not foo:$native -> not foo:$native=1
-E: Not considered: bar:$native=1: not bar:$native -> not bar:$native=1
-E: Not considered: baz:$native=1: not baz:$native -> not baz:$native=1" aptget install awesome foo- bar- baz- -s --solver 3.0
+testfailuremsg "E: Conflict: awesome:$native=1 -> baz:$native=1 -> baz:$native but not baz:$native" aptget install awesome foo- bar- baz- -s --solver 3.0
 testfailureequal "Reading package lists...
 Building dependency tree...
 Package 'foo' is not installed, so not removed
-- 
cgit v1.2.3-70-g09d2


From 4c48b5618ba15d4e33625cec81843891910e81a2 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Tue, 11 Feb 2025 12:11:20 +0100
Subject: solver3: Defer 3.0 'deep' autoremoval to 3.1, fix autoremove

Restore the depcache's MarkRequired logic for 3.0 solver; and
change the MarkInstall() call to pass a more correct value for
FromUser, to not override an existing automatic status.
---
 apt-pkg/depcache.cc                                            | 2 +-
 apt-pkg/edsp.cc                                                | 2 +-
 apt-pkg/solver3.cc                                             | 2 +-
 apt-pkg/solver3.h                                              | 3 ++-
 test/integration/solver3.broken                                | 5 -----
 test/integration/test-apt-get-autoremove-real-virtual-provider | 4 ++--
 6 files changed, 7 insertions(+), 11 deletions(-)

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

diff --git a/apt-pkg/depcache.cc b/apt-pkg/depcache.cc
index ef93a54bb..b66f2bc66 100644
--- a/apt-pkg/depcache.cc
+++ b/apt-pkg/depcache.cc
@@ -2496,7 +2496,7 @@ static bool MarkPackage(pkgCache::PkgIterator const &Pkg,
 // pkgDepCache::MarkRequired - the main mark algorithm			/*{{{*/
 bool pkgDepCache::MarkRequired(InRootSetFunc &userFunc)
 {
-   if (_config->Find("APT::Solver", "internal") != "internal")
+   if (_config->Find("APT::Solver", "internal") != "internal" && _config->Find("APT::Solver") != "3.0")
       return true;
 
    // init the states
diff --git a/apt-pkg/edsp.cc b/apt-pkg/edsp.cc
index 88f572f18..dd9ae18fc 100644
--- a/apt-pkg/edsp.cc
+++ b/apt-pkg/edsp.cc
@@ -754,7 +754,7 @@ static bool CreateDumpFile(char const * const id, char const * const type, FileF
 // EDSP::ResolveExternal - resolve problems by asking external for help	{{{*/
 bool EDSP::ResolveExternal(const char* const solver, pkgDepCache &Cache,
 			 unsigned int const flags, OpProgress *Progress) {
-   if (strcmp(solver, "3.0") == 0)
+   if (strstr(solver, "3.") == solver)
    {
       APT::Solver s(Cache.GetCache(), Cache.GetPolicy());
       FileFd output;
diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index 8af3275eb..44a5075da 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -976,7 +976,7 @@ bool APT::Solver::ToDepCache(pkgDepCache &depcache) const
 	 if (auto RP = reason.Pkg(); RP == P.MapPointer())
 	    reason = (*this)[P].reason;
 
-	 depcache.MarkInstall(P, false, 0, reason.empty());
+	 depcache.MarkInstall(P, false, 0, reason.empty() && not(depcache[P].Flags & pkgCache::Flag::Auto));
 	 if (not P->CurrentVer)
 	    depcache.MarkAuto(P, not reason.empty());
 	 depcache[P].Marked = 1;
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 91b852c98..93e4e5116 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -217,10 +217,11 @@ class Solver
    time_t startTime;
 
    /// Various configuration options
+   std::string version{_config->Find("APT::Solver", "3.0")};
    // \brief Debug level
    int debug{_config->FindI("Debug::APT::Solver")};
    // \brief If set, we try to keep automatically installed packages installed.
-   bool KeepAuto{not _config->FindB("APT::Get::AutomaticRemove")};
+   bool KeepAuto{version == "3.0" || not _config->FindB("APT::Get::AutomaticRemove")};
    // \brief Determines if we are in upgrade mode.
    bool IsUpgrade{_config->FindB("APT::Solver::Upgrade", false)};
    // \brief If set, removals are allowed.
diff --git a/test/integration/solver3.broken b/test/integration/solver3.broken
index 2212c34ae..540bfbca1 100644
--- a/test/integration/solver3.broken
+++ b/test/integration/solver3.broken
@@ -1,23 +1,18 @@
 test-allow-scores-for-all-dependency-types
-test-apt-get-autoremove
-test-apt-get-autoremove-kernel-module-providers
 test-apt-get-upgrade-by-source
 test-apt-install-file-reltag
 test-apt-install-order-matters-a-bit
 test-apt-move-and-forget-manual-sections
-test-apt-patterns
 test-bug-470115-new-and-tighten-recommends
 test-bug-602412-dequote-redirect
 test-bug-611729-mark-as-manual
 test-bug-675449-essential-are-protected
 test-bug-745046-candidate-propagation-fails
-test-bug-753297-upgradable
 test-bug-767891-force-essential-important
 test-bug-961266-hold-means-hold
 test-dont-forget-conflicts-via-unknown-architectures
 test-explore-or-groups-in-markinstall
 test-external-dependency-solver-protocol
-test-method-mirror
 test-parse-all-archs-into-cache
 test-phased-updates-new-depends
 test-phased-updates-upgrade
diff --git a/test/integration/test-apt-get-autoremove-real-virtual-provider b/test/integration/test-apt-get-autoremove-real-virtual-provider
index d5438f8b3..7fda4d370 100755
--- a/test/integration/test-apt-get-autoremove-real-virtual-provider
+++ b/test/integration/test-apt-get-autoremove-real-virtual-provider
@@ -31,7 +31,7 @@ The following packages will be REMOVED:
   needs-provider1 needs-provider4
 0 upgraded, 0 newly installed, 2 to remove and 0 not upgraded.
 Remv needs-provider1 [1]
-Remv needs-provider4 [1]' aptget autoremove -s --solver 3.0
+Remv needs-provider4 [1]' aptget autoremove -s --solver 3.1
 
 testsuccessequal 'Reading package lists...
 Building dependency tree...
@@ -39,4 +39,4 @@ Reading state information...
 The following packages will be REMOVED:
   needs-provider4
 0 upgraded, 0 newly installed, 1 to remove and 0 not upgraded.
-Remv needs-provider4 [1]' aptget autoremove -s --solver internal
+Remv needs-provider4 [1]' aptget autoremove -s
-- 
cgit v1.2.3-70-g09d2


From 3ae41a76c19e5ad05600188de43b46c3e2800676 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Tue, 11 Feb 2025 22:03:03 +0100
Subject: solver3: Pass EDSP flags directly rather than via config

This was a rather silly way to communicate state, and it was
in the wrong place. Notably also, multiple calls to the solver
had the options sticky, that is, if you run upgrade and then
it calls ResolveByKeep(), for example.
---
 apt-pkg/edsp.cc    |  4 ++--
 apt-pkg/solver3.cc |  5 +++--
 apt-pkg/solver3.h  | 10 ++++++----
 apt-pkg/upgrade.cc |  5 -----
 4 files changed, 11 insertions(+), 13 deletions(-)

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

diff --git a/apt-pkg/edsp.cc b/apt-pkg/edsp.cc
index dd9ae18fc..bf96dd35c 100644
--- a/apt-pkg/edsp.cc
+++ b/apt-pkg/edsp.cc
@@ -756,11 +756,11 @@ bool EDSP::ResolveExternal(const char* const solver, pkgDepCache &Cache,
 			 unsigned int const flags, OpProgress *Progress) {
    if (strstr(solver, "3.") == solver)
    {
-      APT::Solver s(Cache.GetCache(), Cache.GetPolicy());
+      APT::Solver s(Cache.GetCache(), Cache.GetPolicy(), (EDSP::Request::Flags) flags);
       FileFd output;
       bool res = true;
       if (Progress != NULL)
-	 Progress->OverallProgress(0, 100, 1, _config->FindB("APT::Solver::Upgrade") ? _("Calculating upgrade") : _("Solving dependencies"));
+	 Progress->OverallProgress(0, 100, 1, (flags & EDSP::Request::UPGRADE_ALL) ? _("Calculating upgrade") : _("Solving dependencies"));
       if (res && not s.FromDepCache(Cache))
 	 res = false;
       if (Progress != NULL)
diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index d7a468227..8d80dfb3c 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -195,7 +195,7 @@ class DefaultRootSetFunc2 : public pkgDepCache::DefaultRootSetFunc
 }; // FIXME: DEDUP with pkgDepCache.
 /*}}}*/
 
-APT::Solver::Solver(pkgCache &cache, pkgDepCache::Policy &policy)
+APT::Solver::Solver(pkgCache &cache, pkgDepCache::Policy &policy, EDSP::Request::Flags requestFlags)
     : cache(cache),
       policy(policy),
       rootState(new State),
@@ -203,7 +203,8 @@ APT::Solver::Solver(pkgCache &cache, pkgDepCache::Policy &policy)
       verStates(cache),
       pkgObsolete(cache),
       priorities(cache),
-      candidates(cache)
+      candidates(cache),
+      requestFlags(requestFlags)
 {
    // Ensure trivially
    static_assert(std::is_trivially_destructible_v<Work>);
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 93e4e5116..796f198b1 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -14,6 +14,7 @@
 
 #include <apt-pkg/configuration.h>
 #include <apt-pkg/depcache.h>
+#include <apt-pkg/edsp.h>
 #include <apt-pkg/pkgcache.h>
 #include <apt-pkg/policy.h>
 
@@ -216,6 +217,7 @@ class Solver
    // \brief The time we called Solve()
    time_t startTime;
 
+   EDSP::Request::Flags requestFlags;
    /// Various configuration options
    std::string version{_config->Find("APT::Solver", "3.0")};
    // \brief Debug level
@@ -223,13 +225,13 @@ class Solver
    // \brief If set, we try to keep automatically installed packages installed.
    bool KeepAuto{version == "3.0" || not _config->FindB("APT::Get::AutomaticRemove")};
    // \brief Determines if we are in upgrade mode.
-   bool IsUpgrade{_config->FindB("APT::Solver::Upgrade", false)};
+   bool IsUpgrade{_config->FindB("APT::Solver::Upgrade", requestFlags &EDSP::Request::UPGRADE_ALL)};
    // \brief If set, removals are allowed.
-   bool AllowRemove{_config->FindB("APT::Solver::Remove", true)};
+   bool AllowRemove{_config->FindB("APT::Solver::Remove", not(requestFlags & EDSP::Request::FORBID_REMOVE))};
    // \brief If set, removal of manual packages is allowed.
    bool AllowRemoveManual{AllowRemove && _config->FindB("APT::Solver::RemoveManual", false)};
    // \brief If set, installs are allowed.
-   bool AllowInstall{_config->FindB("APT::Solver::Install", true)};
+   bool AllowInstall{_config->FindB("APT::Solver::Install", not(requestFlags & EDSP::Request::FORBID_NEW_INSTALL))};
    // \brief If set, we use strict pinning.
    bool StrictPinning{_config->FindB("APT::Solver::Strict-Pinning", true)};
    // \brief If set, we install missing recommends and pick new best packages.
@@ -273,7 +275,7 @@ class Solver
    void RescoreWorkIfNeeded();
 
    // \brief Basic solver initializer. This cannot fail.
-   Solver(pkgCache &Cache, pkgDepCache::Policy &Policy);
+   Solver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags);
 
    // Assume that the variable is decided as specified.
    [[nodiscard]] bool Assume(Var var, bool decision, Var reason);
diff --git a/apt-pkg/upgrade.cc b/apt-pkg/upgrade.cc
index ac0b71cdf..fad47838c 100644
--- a/apt-pkg/upgrade.cc
+++ b/apt-pkg/upgrade.cc
@@ -312,11 +312,6 @@ bool pkgMinimizeUpgrade(pkgDepCache &Cache)
 // APT::Upgrade::Upgrade - Upgrade using a specific strategy		/*{{{*/
 bool APT::Upgrade::Upgrade(pkgDepCache &Cache, int mode, OpProgress * const Progress)
 {
-   _config->Set("APT::Solver::Upgrade", "true");
-   if (mode & FORBID_REMOVE_PACKAGES)
-      _config->Set("APT::Solver::Remove", "false");
-   if (mode & FORBID_INSTALL_NEW_PACKAGES)
-      _config->Set("APT::Solver::Install", "false");
    if (mode == ALLOW_EVERYTHING)
       return pkgDistUpgrade(Cache, Progress);
    else if ((mode & ~FORBID_REMOVE_PACKAGES) == 0)
-- 
cgit v1.2.3-70-g09d2


From 2050ecb34a9e18cf1d8edbff8c52d456a7229162 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Wed, 12 Feb 2025 20:39:33 +0100
Subject: 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.
---
 apt-pkg/solver3.cc                                 | 82 +++++++---------------
 apt-pkg/solver3.h                                  |  4 --
 test/integration/test-apt-never-markauto-sections  |  2 +-
 .../integration/test-bug-604222-new-and-autoremove |  1 -
 ...960705-propagate-protected-to-satisfied-depends |  1 -
 test/integration/test-bug-961266-hold-means-hold   |  2 +-
 6 files changed, 28 insertions(+), 64 deletions(-)

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

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);
diff --git a/test/integration/test-apt-never-markauto-sections b/test/integration/test-apt-never-markauto-sections
index 4d7324b02..95ba47553 100755
--- a/test/integration/test-apt-never-markauto-sections
+++ b/test/integration/test-apt-never-markauto-sections
@@ -49,7 +49,7 @@ Remv foreignpkg:i386 [1]
 Remv nosection [1]
 Remv texteditor [1]' aptget autoremove mydesktop -s
 
-testfailuremsg 'E: Conflict: not texteditor:amd64 -> not bad-texteditor:amd64 -> not mydesktop-core:amd64 but mydesktop:amd64 -> mydesktop-core:amd64' aptget autoremove texteditor -s --solver 3.0 #-o Debug::pkgDepCache::AutoInstall=1 -o Debug::pkgProblemResolver=1 -o Debug::pkgDepCache::Marker=1
+testfailuremsg 'E: Conflict: not texteditor:amd64 -> not bad-texteditor:amd64 but mydesktop:amd64 -> mydesktop-core:amd64 -> bad-texteditor:amd64' aptget autoremove texteditor -s --solver 3.0 #-o Debug::pkgDepCache::AutoInstall=1 -o Debug::pkgProblemResolver=1 -o Debug::pkgDepCache::Marker=1
 testsuccessequal 'Reading package lists...
 Building dependency tree...
 Reading state information...
diff --git a/test/integration/test-bug-604222-new-and-autoremove b/test/integration/test-bug-604222-new-and-autoremove
index 1bd7c5101..8f464ae15 100755
--- a/test/integration/test-bug-604222-new-and-autoremove
+++ b/test/integration/test-bug-604222-new-and-autoremove
@@ -103,7 +103,6 @@ Solving dependencies...MANUAL dummy-archive:i386
 [0] Install:libavcodec52:i386=4:0.5.2-6 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386)
 [0] Reject:libvtk5-dev:i386=5.4.2-8 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386)
 [0] Reject:libvtk5-dev:i386 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386 -> not libvtk5-dev:i386=5.4.2-8)
-Item (1@0) dummy-archive:i386=0.invalid.0 ->  | libvtk5-dev:i386 | libopenal-dev:i386
 [0] Install:libopenal-dev:i386 (dummy-archive:i386=0.invalid.0)
 [0] Install:libopenal-dev:i386=1:1.12.854-2 (dummy-archive:i386=0.invalid.0 -> libopenal-dev:i386)
 
diff --git a/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends b/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends
index 1e59967e4..2f82e9df0 100755
--- a/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends
+++ b/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends
@@ -31,7 +31,6 @@ Solving dependencies...Install foobar:amd64 ()
 [0] Reject:conflicts-foo:amd64 (foobar:amd64=1 -> requires-foo:amd64 -> foo:amd64 -> foo:amd64=1)
 [0] Reject:conflicts-foo:amd64=1 (foobar:amd64=1 -> requires-foo:amd64 -> foo:amd64 -> foo:amd64=1)
 [0] Install:foo-depends:amd64=1 (foobar:amd64=1 -> requires-foo:amd64 -> foo:amd64 -> foo-depends:amd64)
-Item (1@0) foobar:amd64=1 ->  | conflicts-foo:amd64 | fine-foo:amd64
 [0] Install:fine-foo:amd64 (foobar:amd64=1)
 [0] Install:fine-foo:amd64=1 (foobar:amd64=1 -> fine-foo:amd64)
 
diff --git a/test/integration/test-bug-961266-hold-means-hold b/test/integration/test-bug-961266-hold-means-hold
index 7713760d6..b33a5aca7 100755
--- a/test/integration/test-bug-961266-hold-means-hold
+++ b/test/integration/test-bug-961266-hold-means-hold
@@ -126,7 +126,7 @@ The following information may help to resolve the situation:
 
 The following packages have unmet dependencies:
  git-ng : Depends: git (> 1:2.26.2)
-E: Conflict: git-cvs:amd64=1:2.25.1-1 -> git:amd64=1:2.25.1-1 -> not git:amd64=1:2.26.2-1 -> not git-ng:amd64=1:2.26.2-1 but git-ng:amd64=1:2.26.2-1' apt install git-ng -s --solver 3.0
+E: Conflict: git-cvs:amd64=1:2.25.1-1 -> git:amd64=1:2.25.1-1 -> not git:amd64=1:2.26.2-1 but git-ng:amd64=1:2.26.2-1 -> git:amd64=1:2.26.2-1' apt install git-ng -s --solver 3.0
 
 
 msgmsg 'Now mix it up by' 'holding both'
-- 
cgit v1.2.3-70-g09d2


From 9b36a29ffebde3088cec2048505b8d644f46c2c3 Mon Sep 17 00:00:00 2001
From: Julian Andres Klode <julian.klode@canonical.com>
Date: Mon, 10 Feb 2025 23:01:36 +0100
Subject: solver3: Store clauses as the reasons for decisions

So far we only stored the last reason why something was decided,
for example, if "A depends B | C" and we assigned B=false, C=false,
we'd store "(not) C" as the reason for "(not) A".

This gives us only a partial implication graph; after all "C" was
not the *sole* reason for not installing A. This has two implications:

1. We cannot do conflict-driven clause learning
2. We cannot print excellent information about why packages cannot be
   installed (or removed)

This commit is incomplete in addressing both; in particular, we always
store a clause as a reason for something that is not a root object;
whereas MiniSAT would only store a clause on propagation. That is,
if A depends B | C, and we install A, then we have to make a choice
between B|C. Let's say we pick B, we store 'A depends B|C' as the
reason whereas MiniSAT would not store a reason (because it picked
the "next best" unassigned literal).

Hopefully this is not going to be an issue. The reason is used to
calculate the assignments that caused the decision in MiniSAT, but
the idea is that we can just treat reason clauses with unassigned
values as "no reason".

The conflict explanation (WhyStr) has been changed to print the
strongest reason; which produces the same result as the previous
solution for the test suite. What does this mean?

If we look at A depends B|C, let's analyse:

    Why not A?
        We return the first assigned value for B|C, likely B.
        We might have returned C here before as it was the
        last assignment, but we might also return C here,
        if B is not assigned.

    Why B? We return A.

If we look at A conflicts B:

    Why not A? Well B
    Why not B? Well A

Thanks to the structure of the implication graph this is quite
simple, but also generalizing this to the CNF format should not
be hard.

A future version will extend clauses with backlinks to
pkgCache::Dependency*, allowing us to print useful information
to uses such as "A Depends B | C | D (>= 2)" in the real form, rather
than the expanded form which may be "A -> B | C | D=3 | D=2".
---
 apt-pkg/solver3.cc | 49 ++++++++++++++++++++++++++++++-------------------
 apt-pkg/solver3.h  |  9 +++++----
 2 files changed, 35 insertions(+), 23 deletions(-)

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

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index f2e4360ff..c4fb567e1 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -256,18 +256,28 @@ std::string APT::Solver::Work::toString(pkgCache &cache) const
    return out.str();
 }
 
+inline APT::Solver::Var APT::Solver::bestReason(APT::Solver::Clause const *clause, APT::Solver::Var var) const
+{
+   if (not clause)
+      return Var{};
+   if (clause->reason == var)
+      for (auto choice : clause->solutions)
+	 if ((*this)[choice].decision != Decision::NONE)
+	    return choice;
+   return clause->reason;
+}
+
 // Prints an implication graph part of the form A -> B -> C, possibly with "not"
 std::string APT::Solver::WhyStr(Var reason) const
 {
    std::vector<std::string> out;
-
    while (not reason.empty())
    {
       if ((*this)[reason].decision == Decision::MUSTNOT)
 	 out.push_back(std::string("not ") + reason.toString(cache));
       else
 	 out.push_back(reason.toString(cache));
-      reason = (*this)[reason].reason;
+      reason = bestReason((*this)[reason].reason, reason);
    }
 
    std::string outstr;
@@ -337,13 +347,13 @@ bool APT::Solver::Obsolete(pkgCache::PkgIterator pkg) const
    pkgObsolete[pkg] = 2;
    return true;
 }
-bool APT::Solver::Assume(Var var, bool decision, Var reason)
+bool APT::Solver::Assume(Var var, bool decision, const Clause *reason)
 {
    choices.push_back(solved.size());
    return Enqueue(var, decision, std::move(reason));
 }
 
-bool APT::Solver::Enqueue(Var var, bool decision, Var reason)
+bool APT::Solver::Enqueue(Var var, bool decision, const Clause *reason)
 {
    auto &state = (*this)[var];
    auto decisionCast = decision ? Decision::MUST : Decision::MUSTNOT;
@@ -351,7 +361,7 @@ bool APT::Solver::Enqueue(Var var, bool decision, Var reason)
    if (state.decision != Decision::NONE)
    {
       if (state.decision != decisionCast)
-	 return _error->Error("Conflict: %s -> %s%s but %s", WhyStr(reason).c_str(), decision ? "" : "not ", var.toString(cache).c_str(), WhyStr(var).c_str());
+	 return _error->Error("Conflict: %s -> %s%s but %s", WhyStr(bestReason(reason, var)).c_str(), decision ? "" : "not ", var.toString(cache).c_str(), WhyStr(var).c_str());
       return true;
    }
 
@@ -360,7 +370,7 @@ bool APT::Solver::Enqueue(Var var, bool decision, Var reason)
    state.reason = reason;
 
    if (unlikely(debug >= 1))
-      std::cerr << "[" << depth() << "] " << (decision ? "Install" : "Reject") << ":" << var.toString(cache) << " (" << WhyStr(state.reason) << ")\n";
+      std::cerr << "[" << depth() << "] " << (decision ? "Install" : "Reject") << ":" << var.toString(cache) << " (" << WhyStr(bestReason(reason, var)) << ")\n";
 
    solved.push_back(Solved{var, std::nullopt});
    propQ.push(var);
@@ -386,7 +396,7 @@ bool APT::Solver::Propagate()
 	       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, false, var))
+	    if (not Enqueue(rclause->reason, false, rclause))
 	       return false;
 	 }
       }
@@ -416,7 +426,7 @@ bool APT::Solver::Propagate()
 	       {
 		  // 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))
+		     if ((*this)[sol].decision == Decision::NONE && not Enqueue(sol, true, rclause))
 			return false;
 	       }
 	       continue;
@@ -427,7 +437,7 @@ bool APT::Solver::Propagate()
 	    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;
 
-	    if (not Enqueue(rclause->reason, false, var)) // Last version invalidated
+	    if (not Enqueue(rclause->reason, false, rclause)) // Last version invalidated
 	       return false;
 	 }
       }
@@ -680,7 +690,7 @@ void APT::Solver::UndoOne()
 	 std::cerr << "Unassign " << solvedItem.assigned.toString(cache) << "\n";
       auto &state = (*this)[solvedItem.assigned];
       state.decision = Decision::NONE;
-      state.reason = Var();
+      state.reason = nullptr;
       state.depth = 0;
    }
 
@@ -747,7 +757,7 @@ bool APT::Solver::AddWork(Work &&w)
    if (w.clause->negative)
    {
       for (auto var : w.clause->solutions)
-	 if (not Enqueue(var, false, w.clause->reason))
+	 if (not Enqueue(var, false, w.clause))
 	    return false;
    }
    else if (not w.clause->solutions.empty())
@@ -755,7 +765,7 @@ bool APT::Solver::AddWork(Work &&w)
       if (unlikely(debug >= 3 && w.clause->optional))
 	 std::cerr << "Enqueuing Recommends " << w.clause->toString(cache) << std::endl;
       if (w.clause->solutions.size() == 1 && not w.clause->optional)
-	 return Enqueue(w.clause->solutions[0], true, w.clause->reason);
+	 return Enqueue(w.clause->solutions[0], true, w.clause);
 
       w.size = std::count_if(w.clause->solutions.begin(), w.clause->solutions.end(), [this](auto V)
 			     { return (*this)[V].decision != Decision::MUSTNOT; });
@@ -825,7 +835,7 @@ bool APT::Solver::Solve()
 	 }
 	 if (unlikely(debug >= 3))
 	    std::cerr << "(try it: " << sol.toString(cache) << ")\n";
-	 if (not Enqueue(sol, true, item.clause->reason) && not Pop())
+	 if (not Enqueue(sol, true, item.clause) && not Pop())
 	    return false;
 	 foundSolution = true;
 	 break;
@@ -878,7 +888,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
       {
 	 if (unlikely(debug >= 1))
 	    std::cerr << "Hold " << P.FullName() << "\n";
-	 if (P->CurrentVer ? not Enqueue(Var(P.CurrentVer()), true, {}) : not Enqueue(Var(P), false, Var()))
+	 if (P->CurrentVer ? not Enqueue(Var(P.CurrentVer()), true) : not Enqueue(Var(P), false))
 	    return false;
       }
       else if (state.Delete()						  // Normal delete request.
@@ -888,7 +898,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
       {
 	 if (unlikely(debug >= 1))
 	    std::cerr << "Delete " << P.FullName() << "\n";
-	 if (not Enqueue(Var(P), false, Var()))
+	 if (not Enqueue(Var(P), false))
 	    return false;
       }
       else if (state.Install() || (state.Keep() && P->CurrentVer))
@@ -915,7 +925,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
 	 if (not isOptional)
 	 {
 	    // Pre-empt the non-optional requests, as we don't want to queue them, we can just "unit propagate" here.
-	    if (depcache[P].Keep() ? not Enqueue(Var(P), true, {}) : not Enqueue(Var(depcache.GetCandidateVersion(P)), true, {}))
+	    if (depcache[P].Keep() ? not Enqueue(Var(P), true) : not Enqueue(Var(depcache.GetCandidateVersion(P)), true))
 	       return false;
 	 }
 	 else
@@ -977,9 +987,10 @@ bool APT::Solver::ToDepCache(pkgDepCache &depcache) const
 	    if ((*this)[V].decision == Decision::MUST)
 	       cand = V;
 
-	 auto reason = (*this)[cand].reason;
+	 auto reasonClause = (*this)[cand].reason;
+	 auto reason = reasonClause ? reasonClause->reason : Var();
 	 if (auto RP = reason.Pkg(); RP == P.MapPointer())
-	    reason = (*this)[P].reason;
+	    reason = (*this)[P].reason ? (*this)[P].reason->reason : Var();
 
 	 if (cand != P.CurrentVer())
 	 {
@@ -996,7 +1007,7 @@ bool APT::Solver::ToDepCache(pkgDepCache &depcache) const
       }
       else if (P->CurrentVer || depcache[P].Install())
       {
-	 depcache.MarkDelete(P, false, 0, (*this)[P].reason.empty());
+	 depcache.MarkDelete(P, false, 0, not(*this)[P].reason);
 	 depcache[P].Marked = 0;
 	 depcache[P].Garbage = 1;
       }
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index d4a584f2d..65a201222 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -259,6 +259,7 @@ class Solver
    {
       return static_cast<depth_type>(choices.size());
    }
+   inline Var bestReason(Clause const *clause, Var var) const;
 
    public:
    // \brief Create a new decision level.
@@ -274,9 +275,9 @@ class Solver
    Solver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags);
 
    // Assume that the variable is decided as specified.
-   [[nodiscard]] bool Assume(Var var, bool decision, Var reason);
+   [[nodiscard]] bool Assume(Var var, bool decision, const Clause *reason = nullptr);
    // Enqueue a decision fact
-   [[nodiscard]] bool Enqueue(Var var, bool decision, Var reason);
+   [[nodiscard]] bool Enqueue(Var var, bool decision, const Clause *reason = nullptr);
 
    // \brief Apply the selections from the dep cache to the solver
    [[nodiscard]] bool FromDepCache(pkgDepCache &depcache);
@@ -340,7 +341,7 @@ struct APT::Solver::Var
    {
       return IsVersion == 0 && MapPtr == 0;
    }
-   bool operator==(Var const other)
+   bool operator==(Var const other) const
    {
       return IsVersion == other.IsVersion && MapPtr == other.MapPtr;
    }
@@ -447,7 +448,7 @@ struct APT::Solver::State
    // doesn't increase to unwind.
    //
    // Vars < 0 are package ID, reasons > 0 are version IDs.
-   Var reason{};
+   const Clause *reason{};
 
    // \brief The depth at which the decision has been taken
    depth_type depth{0};
-- 
cgit v1.2.3-70-g09d2