A SomewhatMaxSAT Solver

Summary

As you may recall from previous posts and elsewhere I have been busy writing a new solver for APT. Today I want to share some of the latest changes in how to approach solving. The idea for the solver was that manually installed packages are always protected from removals – in terms of SAT solving, they are facts. Automatically installed packages become optional unit clauses. Optional clauses are solved after manual ones, they don’t partake in normal unit propagation. This worked fine, say you had A # install request for A B # manually installed, keep it A depends on: conflicts-B | C Installing A on a system with B installed installed C, as it was not allowed to install the conflicts-B package since B is installed. However, I also introduced a mode to allow removing manually installed packages, and that’s where it broke down, now instead of B being a fact, our clauses looked like: A # install request for A A depends on: conflicts-B | C Optional: B # try to keep B installed As a result, we installed conflicts-B and removed B; the steps the solver takes are: A is a fact, mark it A depends on: conflicts-B | C is the strongest clause, try to install conflicts-B We unit propagate that conflicts-B conflicts with B, so we mark not B Optional: B is reached, but not satisfiable, ignore it because it’s optional. This isn’t correct: Just because we allow removing manually installed packages doesn’t mean that we should remove manually installed packages if we don’t need to. Fixing this turns out to be surprisingly easy. In addition to adding our optional (soft) clauses, let’s first assume all of them! But to explain how this works, we first need to explain some terminology: The solver operates on a stack of decisions “enqueue” means a fact is being added at the current decision level, and enqueued for propagation “assume” bumps the decision level, and then enqueues the assumed variable “propagate” looks at all the facts and sees if any clause becomes unit, and then enqueues it “...