Julian Andres Klode: A SomewhatMaxSAT Solver
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
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
conflicts-B and removed B; the steps the solver takes are:
Ais a fact, mark itA depends on: conflicts-B Cis the strongest clause, try to installconflicts-B- We unit propagate that
conflicts-Bconflicts withB, so we marknot B Optional: Bis reached, but not satisfiable, ignore it because it s optional.
- 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
- unit is when a clause has a single literal left to assign
-
We introduce all our facts, and if they conflict, we are unsat:
for fact in facts: enqueue(fact) if not propagate(): return False -
For each optional literal, we register a soft clause and assume it. If the assumption fails,
we ignore it. If it succeeds, but propagation fails, we undo the assumption.
for optionalLiteral in optionalLiterals: registerClause(SoftClause([optionalLiteral])) if assume(optionalLiteral) and not propagate(): undo() -
Finally we enter the main solver loop:
while True: if not propagate(): if not backtrack(): return False elif <all clauses are satisfied>: return True elif it := find("best unassigned literal satisfying a hard clause"): assume(it) elif it := find("best literal satisfying a soft clause"): assume(it)
A,B,C and B is not possible, we will have also undone C. But since
C is also enqueued as a soft clause, we will then later find it again:
- Assume
A:State=[Assume(A)],Clauses=[SoftClause([A])] - Assume
B:State=[Assume(A),Assume(B)],Clauses=[SoftClause([A]),SoftClause([B])] - Assume
C:State=[Assume(A),Assume(B),Assume(C)],Clauses=[SoftClause([A]),SoftClause([B]),SoftClause([C])] - Solve finds a conflict, backtracks, and sets
not C:State=[Assume(A),Assume(B),not(C)] - Solve finds a conflict, backtracks, and sets
not B:State=[Assume(A),not(B)]C is no longer assumed either - Solve, assume
Cas it satisfiesSoftClause([C])as next best literal:State=[Assume(A),not(B),Assume(C)] - All clauses are satisfied, solution is
A,not B, andC.
Optional: A
Optional: B
Optional: C
B Conflicts with A
C Conflicts with A
AIf we assumeAfirst, we are unable to satisfyBorC.B,CIf we assume eitherBorCfirst,Ais unsat.
2**n times for n soft clauses, whereas our heuristic only needs n runs.
For dependency solving, it seems we do not seem have a strong need for a global maximum:
There are various other preferences between our literals, say priorities;
and empirically, from evaluating hundreds of regressions without the initial assumptions,
I can say that the assumptions do fix those cases and the result is correct.
Further improvements exist, though, and we can look into them if they are needed, such as:
- Use a better heuristic: If we assume 1 clause and solve, and we cause 2 or more clauses to become unsatisfiable, then that clause is a local minimum and can be skipped. This is a more common heuristical MaxSAT solver. This gives us a better local maximum, but not a global one. This is more or less what the Smart package manager did, except that in Smart, all packages were optional, and the entire solution was scored. It calculated a basic solution without optimization and then toggled each variable and saw if the score improved.
-
Implement an actual search for a global maximum:
This involves reading the literature.
There are various versions of this, for example:
- Find unsatisfiable cores and use those to guide relaxation of clauses.
-
A bounds-based search, where we translate sum(satisifed clauses) > k into SAT, and then search in one of the following ways:
- from 0 upward
- from n downward
- perform a binary search on [0, k] satisfied clauses.
When you learn to write, one of the major pieces is writing an introduction. You could say quite a bit about the formal process and the way formal writing is typically structured.That being said, I m not your typical writer. I didn t exactly plan to be in this spot, and honestly, it s just a hobby of mine. If you enjoy reading my posts, great. I appreciate it.My entire point, from the very beginning of this week, has been to bootstrap my own platform, on my own two feet. As you all know, rumors were going around, and I felt as if I wasn t in that great of a position to go out and say everything that I ve said, in one long post. I ve needed to break it apart, and work through some of my own notes again. Prove myself, rather than asking for it to be handed to me. Keep people guessing on some elements, to let the people who have been doing wrong firmly prove themselves. At least twelve people at this point have sent me undeniable proof. I don t want to do anything with it. I want to move on, and I want to write about technology, and other things I actually enjoy writing about.I really don t enjoy conflict, or writing about it, at all. I just know how to defend myself if I need to. If you think I actively want to make everyone mad for no good reason, you re honestly fooling yourself.I already know that I m not going to agree with everything I write in a few years, or maybe even weeks. But I ll hold myself to the same standard I hold everyone else. If you say something and a few years pass, I m not going to assume you still have the same opinion. I ll give you the opportunity to correct it. I d ask you lend me the same courtesy.I do this because I enjoy it, not out of anger, sadness, or anything like that. A number of people have approached me now simply asking why I m doing what I m doing. I planned to write this blog post at the very end all along. I just haven t revealed the plans before publishing. [I wrote the outline for this more than a day ago.]My entire point here is to give the common person a voice. I know exactly what it s like to start from nothing, and work your way up to a comfortable spot. I didn t only do it once, I did it twice. This is my third time. I genuinely don t appreciate it when people silence other people s voices just because they don t like them. I wasn t raised that way, and that s not how I run my own projects. In fact, I d say that if you silence opinions or values that don t exactly match yours, you re missing out on the variety of life.You can lead a horse to water, but you can t make them drink. If you still think there are issues on my end, you re being misinformed. Plain and simple. I m not going to spend any more time on it, I actually want to start what I ve always wanted to do for years, just never had the opportunity to.This is my last post for the week. I feel like I ve bootstrapped enough where next week I can focus on another topic, as originally planned.Thanks for reading. I appreciate your support. Talk to you on Monday. If you have topic suggestions, feel free to leave them in the comments. Feel free to leave your hate mail too, so I know where I m at.If you read Piaget, you know that silence is concerning with respect to socialization. I just took a look at the view count for the first time, and I m already up to more than 2k views. In the first week. Without actually digging into the content I want to write about, yet.I don t mean to say that to brag, I m just telling you for a fact that I m not ranting into thin air. I m not even ranting at all. In fact, every single one of my posts has been written either calmly or with happiness, including this one.My entire point is this: debate me on the merits of the subject, not on me as a person. If you don t like me, that s okay. Go play elsewhere.But, I m still going to keep writing. Next week, different metaphors.We re bootstrapped now.
Like each month, have a look at the work funded by 
To build our local voice satellite on a Debian system rather than using the 
On 26th and 27th April we held a Debian bug-squashing party near
Leuven, Belgium. Several longstanding and new Debian contributors
gathered to work through some of the highest priority bugs affecting
the upcoming release of Debian 13 trixie .
We were hosted by the 
After my previous posts related to 
I ve been using Procmail to filter mail for a long time. Reading Antoine s blog
post 
Usage is driven by deployment in continuous integration (as for
example the Ubuntu-use at GitHub makes this both an easy and obvious
choice), cloud computing (as it is easy to spin up Ubuntu instances, it
is as easy to add ,_Sea_Point,_Nachtansicht_--_2024_--_1867-70_-_2.jpg){kind=link}
.jpg){kind=link}