From 93675680fca31004d5ea9e011d025c0ff189fc81 Mon Sep 17 00:00:00 2001 From: Julian Andres Klode Date: Mon, 22 Dec 2025 18:14:38 +0100 Subject: solver3: Rename key concepts to MiniSAT names This should make it easier for people with MiniSAT knowledge to onboard themselves to the solver. --- apt-pkg/solver3.h | 57 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 29 insertions(+), 28 deletions(-) (limited to 'apt-pkg/solver3.h') diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index c4b87e9fe..eff2c50d6 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -89,7 +89,7 @@ class Solver struct State; struct Clause; struct Work; - struct Solved; + struct Trail; friend struct std::hash; friend struct std::hash; @@ -202,30 +202,25 @@ class Solver // \brief Heap of the remaining work. // - // We are using an std::vector with std::make_heap(), std::push_heap(), - // and std::pop_heap() rather than a priority_queue because we need to - // be able to iterate over the queued work and see if a choice would - // invalidate any work. + // In contrast to MiniSAT which picks undecided literals and decides them, + // we keep track of unsolved active clauses in a priority queue. This allows + // us to for example, solve Depends before Recommends (see Group). heap work; - // \brief Backlog of solved work. - // - // Solved work may become invalidated when backtracking, so store it - // here to revisit it later. This is similar to what MiniSAT calls the - // trail; one distinction is that we have both literals and our work - // queue to be concerned about - std::vector solved; + /// \brief Trail of assignments done, and clauses solved. + /// + /// Record past assignments and solved clauses such that we can revert them when + /// backtracking. + std::vector trail; + + /// \brief Separator indices for different decision levels in trail + std::vector trailLim{}; // \brief Propagation queue std::queue propQ; // \brief Discover variables std::queue discoverQ; - // \brief Current decision level. - // - // This is an index into the solved vector. - std::vector choices{}; - // \brief The time we called Solve() time_t startTime{}; @@ -273,10 +268,10 @@ class Solver // \brief Propagate all pending propagations [[nodiscard]] bool Propagate(); - // \brief Return the current depth (choices.size() with casting) - depth_type depth() + // \brief Return the current depth (.size() with casting) + depth_type decisionLevel() { - return static_cast(choices.size()); + return static_cast(trailLim.size()); } inline Var bestReason(Clause const *clause, Var var) const; inline LiftedBool value(Lit lit) const; @@ -286,7 +281,7 @@ class Solver void Push(Var var, Work work); // \brief Revert to the previous decision level. [[nodiscard]] bool Pop(); - // \brief Undo a single assignment / solved work item + // \brief Undo a single assignment / trail work item void UndoOne(); // \brief Add work to our work queue. [[nodiscard]] bool AddWork(Work &&work); @@ -472,7 +467,7 @@ struct APT::Solver::Work // \brief The depth at which the item has been added depth_type depth; - // Number of valid choices + /// Number of valid choices at insertion time size_t size{0}; // \brief This item should be removed from the queue. @@ -539,16 +534,22 @@ struct APT::Solver::State }; /** - * \brief A solved item. + * \brief A trail item. + * + * In MiniSAT, a trail item is an assigned literal. However, we store an assigned variable instead, + * since the assignment is still recorded when we need to access the trail; there does not appear + * to be a substantial value in recording the sign here; but it produces a risk for a disagreement + * between the actual state and the sign recorded in the trail. * - * Here we keep track of solved clauses and variable assignments such that we can easily undo - * them. + * In addition to MiniSAT's trail, we also need to keep a trail of solved Work items; that is + * clauses that were being solved, as when undoing the trail, we need to mark those clauses + * active again by putting them back on the work heap. */ -struct APT::Solver::Solved +struct APT::Solver::Trail { - // \brief A variable that has been assigned. We store this as a reason (FIXME: Rename Var to Var) + /// \brief A variable that got assigned True or False. May be reset to Undefined on backtracking. Var assigned; - // \brief A work item that has been solved. This needs to be put back on the queue. + /// \brief A work item (a clause) that was solved. Needs to be put back on the work heap on backtracking. std::optional work; }; -- cgit v1.2.3-70-g09d2