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
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:
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
There are two possible results here:
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.
I have been a very happy user of my two SK-8845 keyboards (one at my
office, one at home) since I bought them, in 2018 and 2021
respectively. What are they, mind you?

So it kind-of sort-of made sense, when I saw a Toshiba-IBM keyboard
being sold for quite cheap (MX$400, just over US$20) to try my luck with
it:
This is quite an odd piece of hardware, built in 2013 according to its
label. At first I was unsure whether to buy it because of the weird
interface it had, but the vendor replied they would ship a (very long!) USB
cable with it, so
As expected, connecting it to Linux led to a swift, errorless recognition:
Within minutes of receiving the hardware, I had it hooked up and started
looking at the events it generated However the romance soon started to
wane. Some of the reasons:
This morning, I went to make my usual cup of coffee. I was given an espresso machine for Christmas, and I ve developed this technique for making a warm drink that hits the spot every time.I ll start by turning on my espresso machine and starting a single shot of espresso. It dispenses and drips while I m working on the other parts.I then grab a coffee cup. Usually one of the taller ones. For maybe the bottom inch or two of the cup, that gets sugar and chocolate milk. Microwave for 45 seconds, pour in the espresso, then wash out the actual espresso from the metal cup with milk. Pour all of that in, another 45 seconds in the microwave, a few quick stirs, and you re all set.To the actual baristas out there, that probably sounds horrible. It probably sounds like the worst possible recommendation for a morning coffee ever.But, you know what? It works.So, I went to put my coffee into the microwave today, and I realized that someone else had put the glass plate for the microwave into the sink after accidentally spilling their breakfast on it.Instead of saying, well, I m not going to have my coffee this morning, I grabbed a large plate. I remembered the physics of levers from high school, and I understood that if I balanced everything just right, it would heat my coffee up.And well, here I am. With an un-spilled coffee and a story to tell.My point here is actually pretty simple, and this is before I even read any messages for the day. People with much more formal educations sometimes look at the guy engineering coffee with his microwave and think, what is this guy doing?!? All I m doing is making a really good cup of coffee. And to be honest, it tastes amazing.That s all. Have a wonderful day.













Release 0.2.8 of our
TGV train I rode from Luxembourg to Paris
Pasta I had in Paris
A cycling track in Paris
Luxembourg Museum
A shot of the park near to the Luxembourg Museum
Pantheon, one of the attractions of Paris.
Photo with Joenio and Mari
Notre Dame, another tourist attraction of Paris.
My photo with Eiffel Tower in the background
Items at a bakery in Paris. Items from left to right are: Chocolate Twist, Sugar briochette, Pain au Chocolat, Croissant with almonds, Croissant, Croissant with chocolate hazlenut filling.
The Paris subway
Inside a Paris subway
A random building and road in Paris
A shot near Seine river
A view of Seine river
Apt in Trixie (Debian 13) has the annoying function to tell you
"Notice: Some sources can be modernized. Run 'apt modernize-sources' to do so." ... every single time you run 

For a long time I ve been wanting to try GitOps tools, but I haven t had the chance to try them for real on the projects
I was working on.
As now I have some spare time I ve decided I m going to play a little with 
Back when I setup my home automation I ended up with one piece that used an external service:
The new FAI release 6.4 comes with some nice new features.
It now supports installing the Xfce edition of Linux Mint
22.1 'Xia'. There's now an additional
Hi, I m Melissa, a GPU kernel driver developer at Igalia and today I ll be
giving a very inclusive talk to not let your motivation go by saving time with
kworkflow.
So, you re a kernel developer, or you want to be a kernel developer, or you
don t want to be a kernel developer. But you re all united by a single need:
you need to validate a custom kernel with just one change, and you need to
verify that it fixes or improves something in the kernel.
And that s a given change for a given distribution, or for a given device, or
for a given subsystem
Look to this diagram and try to figure out the number of subsystems and related
work trees you can handle in the kernel.
So, whether you are a kernel developer or not, at some point you may come
across this type of situation:
There is a userspace developer who wants to report a kernel issue and says:
What s the problem of this situation? The problem is that you keep creating new
scripts!
Every time you change distribution, change architecture, change hardware,
change project - even in the same company - the development setup may change
when you switch to a different project, you create another script for your new
kernel development workflow!
You know, you have a lot of babies, you have a collection of my precious
scripts , like Sm agol (Lord of the Rings) with the precious ring.
Instead of creating and accumulating scripts, save yourself time with
kworkflow. Here is a typical script that many of you may have. This is a
Raspberry Pi 4 script and contains everything you need to memorize to compile
and deploy a kernel on your Raspberry Pi 4.
With kworkflow, you only need to memorize two commands, and those commands are
not specific to Raspberry Pi. They are the same commands to different
architecture, kernel configuration, target device.
I don t know if you will get this analogy, but kworkflow is for me a megazord
of scripts. You are combining all of your scripts to create a very powerful
tool.
This is the list of commands you can run with kworkflow.
The first subset is to configure your tool for various situations you may face
in your daily tasks.
So how can you save time building and deploying a custom kernel?
First, you need a .config file.
Then you want to build the kernel:
Finally, to deploy the kernel in a target machine.
You can also save time on debugging kernels locally or remotely.
You can save time on managing multiple kernel images in the same work tree.
Finally, you can save time when submitting kernel patches. In kworkflow, you
can find everything you need to wrap your changes in patch format and submit
them to the right list of recipients, those who can review, comment on, and
accept your changes.
This is a demo that the lead developer of the kw patch-hub feature sent me.
With this feature, you will be able to check out a series on a specific mailing
list, bookmark those patches in the kernel for validation, and when you are
satisfied with the proposed changes, you can automatically submit a reviewed-by
for that whole series to the mailing list.
