solver3: Use a propagation queue

Instead of directly propagating in a recursive fashion,
queue propagations in a queue and work on them in a loop
per the miniSAT paper.

We call Propagate() only at the end of the FromDepCache()
function and then in the Solve loop. Delaying the initial
propagation means that we get a stronger reasoning:

Assume you have x->a->b->c, y->c and you install x,y:
- Previously we traversed: x, y, x->a, a->b, b->c, (y->c)
- but now we traverse:     x, y, x->a, y->c, a->b, (b->c)
Notably c now has the implication y->c instead of x->a->b->c.

Inside the solver we need to call Propagate in a loop:
Propagating facts can fail and we then backtrack. If backtracking
is succesful, we have gained a new fact to propagate.

1 files changed, 5 insertions, 0 deletions

diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index 5c67faff2..4f6f83d15 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -132,6 +132,9 @@ class Solver
    // queue to be concerned about
    std::vector<Solved> solved{};
 
+   // \brief Propagation queue
+   std::queue<Var> propQ;
+
    // \brief Current decision level.
    //
    // This is an index into the solved vector.
@@ -155,6 +158,8 @@ class Solver
    bool RejectReverseDependencies(pkgCache::VerIterator Ver);
    // \brief Enqueue a single or group
    bool EnqueueOrGroup(pkgCache::DepIterator start, pkgCache::DepIterator end, Var reason);
+   // \brief Propagate all pending propagations
+   bool Propagate();
    // \brief Propagate a "true" value of a variable
    bool PropagateInstall(Var var);
    // \brief Propagate a rejection of a variable