The solver forms the core of the computation engine used by pkg(5) to determine the packages that can be installed, updated, or removed, given the constraints in the image and constraints introduced by any new packages for installation.
This problem is an example of a Boolean satisfiability problem, and can be solved by a SAT solver.
The various possible choices for all the packages are assigned Boolean variables, and all the dependencies between those packages, any required packages, and so on, are cast as Boolean expressions in conjunctive normal form.
The set of expressions generated is passed to MiniSAT. If MiniSAT cannot find any solution, the error handling code attempts to walk the set of installed packages and the attempted operation and print the reasons that each possible choice was eliminated.
If the currently installed set of packages meets the requirements but no other set does, pkg reports that there is nothing to do.
As mentioned previously, the error message generation and specificity is determined by the inputs to pkg. Being as specific as possible in commands issued to pkg produces the most useful error messages.
If MiniSAT finds a possible solution, the optimization phase begins.