From f8dd5ea23c6a7fccf643329c50ae1f11f48b1a09 Mon Sep 17 00:00:00 2001 From: Julian Andres Klode Date: Tue, 20 May 2025 13:13:45 +0200 Subject: solver3: Remove Push() and refactor Solve() This method is no longer needed technically speaking, we should use Assume() instead. It turns out that there is a slight bug in the propagation and some clauses that are unit end up on the heap rather than having been propagated away, so we temporarily need to keep an if for that around. To accomodate the switch from Push() to Assume() we need to make sure that the work item is pushed to our trail *after* we have assumed it, such that reverting pushes it back to the work heap. Refactor the code to consistently use Assume() rather than supporting Enqueue(), this vastly simplifies things. This is not fully accurate in the current model and leads to unnecessary decision levels, since sometimes we seem to be reaching unit clauses here. This preserves traversal order by first removing the item from the heap and then adding it back if we need to solve it again. --- apt-pkg/solver3.h | 2 -- 1 file changed, 2 deletions(-) (limited to 'apt-pkg/solver3.h') diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index f66b3cf62..facba4d39 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -370,8 +370,6 @@ class Solver inline LiftedBool value(Lit lit) const; public: - // \brief Create a new decision level. - void Push(Var var, Work work); // \brief Revert to the previous decision level. [[nodiscard]] bool Pop(); // \brief Undo a single assignment / trail work item -- cgit v1.2.3-70-g09d2