Summer of Math Exposition

Cool connection between software and logic

This was a fun way to introduce SAT solvers to a programming audience.

I’ve seen some explanations elsewhere about using SAT solvers for dependency resolution, but I especially like how you walked through very concrete examples to make everything accessible. The game was also nice (though I got confused about how to “submit my answer” that there was no solution).

The text is generally written in a very accessible way, except I would argue, the info box about Boolean Proposition formulas at the very beginning. The content becomes completely clear with the later examples/applications of these formulas, but if it’s to remain right at the beginning it could benefit from some more additional explanation. Small suggestion about the dependency graph: Have first an arrow pointing towards the package (e.g.) beta, then have it split up to the different versions, to make clear visually that alpha does not depend on beta 1.3 AND beta 1.4. Also, importantly, the text states beta 1.3 depends on gamma 0.5, and 1.4 on gamma 0.6, but then this becomes beta 1.3 on gamma 0.5 and 0.6, and beta 1.4 on 0.7. A small delve into a solver algorithm would have been fun, but all in all great read!

Although not the core topic, it does a better job of explaining SAT, and P and NP problems than most resources.

Interesting and well explained formulation of the problem. I was keen to see a solution method. I wonder if it could be formulated as a linear optimization with inequality and equality constraints, potentially preferring newer versions for the objective function. The basics of a general purpose linear optimization solver are described here.

https://mathsfromnothing.au/simplex-method/

I expect there will be many improvements possible to make it a solver for this particular problem.

There are some mistakes, e.g. writing “Beta-1.4 is dependent on Gamma-0.6”, while showing that it depends on Gamma-0.7.

I would prefer a more contained exposition on boolean logic at the start, and then writing the remainder of the blog assuming this knowledge as given, such that both do not intertwine too much. Someone who is comfortable with boolean logic already could then more easily skip the intro, and learn about how it is applied to the specific case of package managers.

It is an interesting quick topic. The game is a nice extra to the written blog post, though it could be a bit more user friendly (finding the constraints to satisfy took a while).

I never heard of this topic, very very interesting choice. However, perhaps that a bit of interactivity or live demo would really improve what is explained, as it is a bit harsh to read. Like a little demo, step by step, based on one specific experiment.

It was very interesting to find out how package managers deal with import collisions.