ソルバーは、イメージ内の制約およびインストール用の新しいパッケージによって導入された制約を考慮に入れてインストール、更新、または削除できるパッケージを判断するために pkg(5) によって使用される演算処理エンジンの中核を成しています。
この問題は、ブール型の充足可能性問題の一例であり、SAT ソルバーによって解決できます。
すべてのパッケージの可能性のあるさまざまな選択肢がブール型変数に割り当てられ、それらのパッケージ間のすべての依存関係や必須パッケージなどが論理積正規形のブール式としてキャストされます。
生成された一連の式は MiniSAT に渡されます。MiniSAT がソリューションを 1 つも見つけられない場合は、エラー処理コードが、インストールされた一連のパッケージと試された操作を調べて、可能性のあるそれぞれの選択肢が除外された理由を出力します。
現在インストールされているパッケージのセットは要件を満たしており、ほかに満たしているセットがない場合、pkg は何もすることがないことを報告します。
前述のように、エラーメッセージの生成と具体性は pkg への入力によって決まります。pkg に発行されるコマンド内をできるだけ具体的にすると、もっとも役立つエラーメッセージが生成されます。
MiniSAT が可能性のあるソリューションを見つけた場合は、最適化フェーズが開始されます。