At prefix.dev we’re invested in the conda ecosystem.
A key part of conda is the SAT solver. SAT stands for “Boolean Satisfiability”.
This class of solvers makes it possible to solve complicated dependency problems – for example if two packages require different ranges of a common dependency, the SAT solver will figure out the working solution (if it exists).
The size of the conda-forge repository makes this a pretty challenging task for regular SAT solvers. When mamba was started, the “key innovation” was to use a specialized solver for package management, called libsolv.
Over time, and with the growth of the conda-forge ecosystem, the original solver for the conda package manager had become a severe bottleneck (solve times of ~minutes where commonly seen, with sometimes even reaching hours, far too long for enjoyable use).
Libsolv has offered us great performance, and it is also what we used in our low-level library for handling conda packages – rattler – that is using some custom bindings to the libsolv C library.
However, one disadvantage of libsolv has always been that it is quite difficult to read – the code is very expert level C code that implements many low-level tricks for extra performance. Additionally, we had some trouble getting some PRs into libsolv.
And lastly, the way libsolv is designed is completely not thread safe, which makes use cases with multi-threaded solving impossible.
For these reasons we made the difficult decision to try to create a port of libsolv in Rust.
And luckily we are able to report that it has succeeded! Along the way we discovered some interesting theories about SAT solvers.
For example, we found that libsolv implements many of the best practices for implementing high-performance SAT solvers, such as “conflict-driven clause learning” (CDCL) and 2-literal watching (a cool trick to make decisions very quickly).
Our port does not implement all features of libsolv (there are some features specific to RPM that we skipped, such as recommends, suggests, and obsoletes).
It does implement everything needed for conda packages: dependencies (with full matchspec support), constrains (for optional dependencies), and most importantly beautiful error messages when no solution can be found.
You can find our port of libsolv (rattler_libsolv_rs) on Github!
SAT solving for package management
A SAT solver knows about “rules” and “literals”.
Each literal corresponds to one specific version of a package.
Rules are the constraints that are imposed on the literals.
For example, if package A requires package B, then there is a rule that says “if A is installed, then B must be installed”.
The two main rule c
