高速なパッケージ依存関係解決のためのSAT

1. はじめに

Pythonで仮想環境を作成する際、皆さんは何を使っていますか？
私はuv一択です。uvは非常に高速で、依存関係の解決も迅速に行うことができます。
こちらの記事とかみていただけると、uvの速さの秘密は代替キャッシュなんやな、ってことがよくわかると思います。
それで終わってしまうと面白くないので、今回はuvの依存関係解決のアルゴリズムであるPubGrupについて解説します。
今回の記事の実装はC++で行なっています。

2. PubGrubとは

PubGrubは、パッケージ依存関係の解決に特化したrust製のライブラリです。
SAT(充足可能性問題)に関する主要なアルゴリズムであるCDCL(Conflict-Driven Clause Learning)をベースにしており、非常に高速に依存関係の解決を行うことができます。
といっても何がなんだかよくわからないと思うので、まずはどのような問題に定式化されているのかから説明します。

2.1 パッケージ依存関係解決問題の定式化

パッケージA (1) → [パッケージB(>=1, <3)]
パッケージB (1) → [パッケージC(>=1, <3)]
パッケージC (1) → []
パッケージC (2) → []

上のようなパッケージ依存関係があったとします。この時にパッケージAのバージョン1をインストールしたいとすると、選ばれるパッケージの組み合わせは(パッケージA:1, パッケージB:1, パッケージC:2)となります。
これを論理式で書くと以下のようになります。

A@1 ∧ (A@1 → B@[1,3)) ∧ (B@1 → C@[1, 3)) ∧ (C@1 → true) ∧ (C@2 → true)

これをA→Bを¬A∨Bに変換してCNF記法($\bigwedge_{i}\bigvee_{j}l_{i,j}$)に直すと以下のようになります。

(A@1) ∧ (¬A@1 ∨ B@[1, 3)) ∧ (¬B@1 ∨ C@[1, 3)) ∧ (¬C@1 ∨ true) ∧ (¬C@2 ∨ true)

この時、A@1をリテラル(論理変数)といい、true またはfalseが割り当てられる対象を意味します。これらのリテラルが∧でつながっている(¬A@1 ∨ B@[1, 3))のような各項のことをここでは節(clause)と呼びます。
そしてこれを元にSATソルバーで解くこともできるんですが、PubGrubではさらにこの形式に対して一手間加えて次のような式に変換します。

(A@1) ∧ ¬(A@1 ∧ B@¬[1, 3)) ∧ ¬(B@1 ∧ C@¬[1, 3)) ∧ ¬(C@1 ∧ false) ∧ ¬(C@2 ∧ false)

節の¬を前に出しただけじゃん、これはなんやねん、と思うかもしれません。これは本質的な問題というよりは実装上の都合によるものです。
PubGrubでは節を辞書式で管理しているのですが、それのインデックスとして¬(A@1 ∧ B@¬[1, 3))であれば先頭のA@1を使って管理しています。¬A@1をインデックスに使ってもいいんですが、なんか綺麗ではないのでこのような形にしています。
そしてこの形式に変換したときの(A@1 ∧ B@¬[1, 3))のような各項のことを不整合(incompatibility)と呼びます。
Aにバージョン1を選択したのに、Bに1未満、3以上のバージョンを選択するのは不整合ですよね、という感じです。
(C@1 ∧ false)このような不整合は常にfalseなので、追加する必要もないのでは？と思われるかもしれませんが、これはCのバージョンの候補としてC@1が存在することを示すために使っています。今回の例ではC@3とかが選べないことを示すために必要になります。

2.2 単位伝播(unit propagation)

これは古のSATソルバーからある技術で、PubGrubでも使われています。
単位伝播とは、ある特定のリテラルに対してtrue/falseを割り当てたときに、他のリテラルの値が強制的に決定されることを指します。
例えば、¬(A@1 ∧ B@¬[1, 3))に対して、A@1=trueが割り当てられた場合、B@¬[1, 3)=falseが強制的に割り当てられます。つまり、B@[1, 3)=trueが割り当てられます。
この時B@[1,3)が導出されたといいます。なので、今度はB@2とB@1を試していきます。これを繰り返していき、もし矛盾が発生した場合は仮定したリテラルの割り当てを変更する、ことで解を探索していきます。
これをナイーブに実装したのがDPLL(Davis–Putnam–Logemann–Loveland)アルゴリズムです。
(実際にはDPLLをバージョン管理用に少し拡張しているので、元のSATソルバーの話とかをみたければこちらが参考になると思います。)

今現在見ているパッケージのバージョンを新しい順に試していく
そのバージョンが関連している不整合を全て調べる
もし2のチェックを全て通過したら実際にそのバージョンを割り当てとして追加し、次に見るべきパッケージの候補集合からパッケージを1つ取り出して、1に戻る
もしそれで全てのパッケージのバージョンが決定されたら成功、そうでなければ失敗

こんな感じのアルゴリズムになります。擬似コードで書くと以下のようになります。
実際に私が実装したコードもこちらにあるので、興味があれば見てみてください。

dpll(
    現時点でのパッケージに対するバージョンの割り当て S,
    不整合の集合 I,
    対象のパッケージ P,
    次にみるべきパッケージの候補集合 C
) -> 成功: true/失敗: false
    versions = IからPのバージョン候補を抽出
    versionsを降順にソート(新しいバージョンが先頭)

    for v in versions:
        can_assign = true

        deps = IからPが含まれる不整合を全て抽出
        for dep in deps:
            if P@vがdepを満たす:
                continue
            else if 矛盾が発生:
                can_assign = false
            else:
                // 不整合を構成しているもう一方のパッケージQがまだ決定されていない
                CにQを追加
        
        if can_assign:
            all_deps_satisfied = true
            SにP@vを追加
            while Cが空でない:
                Q = Cからパッケージを1つ取り出す
                if dpll(S, I, Q, C):
                    SからP@vを削除
                    all_deps_satisfied = false
                    break

            if all_deps_satisfied:
                return true

    return false

3. CDCLアルゴリズム

先ほど説明したDPLLアルゴリズムは非常にシンプルでわかりやすいのですが、PubGrubではさらに高速化するためにCDCLアルゴリズムを採用しています。
本家のCDCLアルゴリズムの説明はこちらやこちらが非常にわかりやすいので、興味があれば見てみてください。
このアルゴリズムのベースはDPLLと同じ単位伝播なのですが、ある点においてDPLLと異なります。
それは、矛盾が発生したときの対処方法です。
DPLLでは矛盾が発生した場合、直前に割り当てたリテラルの割り当てを変更して再度探索を行います。
一方、CDCLでは矛盾が発生した場合、その矛盾を引き起こした原因となる割り当てを特定し、その割り当てをした時点まで戻って再度探索を行います。
つまり、ミスが起きた時にそのミスの原因に直接戻ることで、無駄な探索を減らすことができるのです。

3.1 単位伝播(再び)

CDCLアルゴリズムも単位伝播をベースとしていると言ったばかりですが、実はDPLLの単位伝播よりも少し強力で情報量が増えています。DPLLでは現時点でのパッケージに対するバージョンの割り当てのみを部分解として持っていましたが、CDCLではパッケージに対するバージョンの制約も部分解として持っています。
例えば、(¬A@1 ∨ B@[1, 3))という不整合があり、A@1=trueの割り当てが決まった時点で、B@[1, 3)=trueが導出されます。DPLLではこの時点ではBのバージョンが確定したわけではないので、Bに関する情報は部分解には含まれません。
一方、CDCLではB@[1, 3)=trueが導出された時点で、Bに関する制約が部分解に追加されます。また、それに加えてこのBに関する導出はA@1=trueの割り当てによるものである、という情報も部分解に含まれます。
また、B@[1, 3)=trueが導出された後に、B@2=trueが割り当てられたとしたら、Bに関する部分解は[B@[1, 3)=true, B@2=true]となって、時系列的に情報が蓄積されていきます。
この時系列的な情報に対して時刻のようなものが定義されており、これをdecision levelと呼びます。
decision levelとはA@1=trueのようにパッケージに対してひとつのバージョンの割り当てを行った時に上がる値で、単位伝播で導出された制約はそのdecision levelに紐づけられます。
例えば、A@1=trueがdecision level 1で割り当てられたときにB@[1, 3)=trueが導出された場合、B@[1, 3)=trueはdecision level 1に紐づけられます。
もしA@1=trueがコンフリクトの原因であると断定できた場合、decision level 1以降に紐づけられた導出が全て無効化されるというような仕組みになっています。
これで原因が特定されれば、巻き戻す方法はわかったので、次はその原因の特定方法について説明します。

3.2 矛盾の原因特定とバックトラック

矛盾が発生した場合の対処方法について説明します。
まず不整合は¬(A@1 ∧ B@¬[1, 3))このような形をしていることを思い出してください。
この不整合がFalseになってしまうということは、A@1=trueかつB@¬[1, 3)=trueが同時に成り立ってしまう、ということです。
この時点ではAへの割り当てとBへの割り当てのどちらが原因で矛盾が発生したのかはわかりません。
なので、 3.1で説明した導出の時系列を辿っていきます。

矛盾が発生した不整合を構成している全てのパッケージに対して以下の操作を行う
- そのパッケージに関する導出の時系列を逆順に辿っていく
- どの導出において初めて不整合を構成しているパッケージの制約を満たすようになったかを調べる
  (例えばパッケージBであれば、B@¬[1, 3)を満たすようになった導出を探す)
- その導出に紐づけられたdecision levelを記録
1で記録したdecision levelの中で最大のものを見つける

これを行うことで、A@1=trueかつB@¬[1, 3)=trueが同時に成立してしまった原因となるdecision levelを特定することができます。

3.3 学習と再探索

3.2の手順で、矛盾の直接的な引き金となったパッケージ（Satisfier）と、そのDecision Level（$L_{max}$）を特定しました。しかし、すぐにそのレベルを取り消して（バックトラックして）良いとは限りません。

(A@[1,1] ∧ B@¬[1,3) ∧ C@[1,1]) 
(B@[2,2] ∧ D@¬[1,2))
(B@[1,1] ∧ false)
(C@[1,1] ∧ false)
(D@[1,1] ∧ B@[2,2])

このようなケースが存在していたとしましょう。この時矛盾は次のように発生します。

A=1に決定 (Decision1) → B=[1,3)とC=[1,1]が導出
B=2に決定 (Decision2) → D=[1,2)が導出
C=1に決定 (Decision3)
D=1に決定 (Decision4) → (D@[1,1] ∧ B@[2,2])で💥コンフリクト

この時に3.2で決定する不整合を満たしてしまう最大のDecision levelはどこかというとSatisfierがパッケージDの時で、Decision Level4になります(ここでは$[1,2)!=[1,1]$となっています) しかし、根本的な原因はDecision level2にあるので、4に戻ってもD=1にするしかなく同じ結果が導かれるだけでなんの意味もありません。
そこで、PubGrubでは不整合になる直前のSatisfierのバージョンの集合と、コンフリクトが起きた不整合でのSatisfierのバージョンの集合の否定の積集合を撮ります。こうすることでコンフリクトが起きないSatisfierのバージョン集合を得ることができます。今回それを行うと[1,2)∧(1,∞)=(1,2)となります。そしてこれを満たすような最大のDに関するDecisionを探すのですが、最初にDが導出されたのがDecision2の時に[1,2)なので、この時点で(1,2)を満たせません。よって、この決定が間違っていたことがわかり、Decision 2へとジャンプします。この時のDecision 2のレベルを$L_{prev}$と書きます。
それでは$L_{prev}$まで巻き戻して処理を再開しましょう！と言いたいんですが、もう少し考えなければならないことがあります。それが下のケース2のような状況です。

ケース1：Decision Levelが異なる場合

($L_{max} > L_{prev}$)
この時は素直に$L_{prev}$まで巻き戻して大丈夫です。

ケース2：Decision Levelが同じ場合

($L_{max} == L_{prev}$)
あるレベルでパッケージAを決定した結果、依存関係で自動的にパッケージBも決まり、そのAとBの両方が不整合の条件に含まれているような状況です。

(A@[1,1] ∧ B@¬[1,1]) 
(A@[1,1] ∧ B@[1,2))

まあなんとも作為的ですが、このような例を考えます。
この場合、$L_{max}$ はDecision level 1です。そして　$L_{prev}$ を計算するために、Satisfierであるパッケージ B に注目します。BはAによって導出されたので、Bの現在の制約は [1, 1] です。一方、不整合が起きているBの条件は [1, 2)です。$[1, 1]∧[2,∞)= \emptyset$で空集合になります。空集合は最初に導出された地点まで戻るので$L_{prev}=1$になり、Decision Levelが同じになってしまいます

ここの論理が実はいまいち理解しきれていませんがPubGrubでは導出原理（Resolution）を使って、不整合の式を書き換えています。(参考)

現在の不整合: $\neg(A@1 \land B@[1, 2))$「Aが1で、かつBが1〜2の間だとダメ」
Bの導出理由: $\neg(A@1 \land B \neq 1)$「Aが1で、かつBが1じゃない、というのはダメ（＝Aが1ならBは1だ）」
この2つを、共通項である B に注目して合成します。Bに関しては、「$[1, 2)$ である」かつ「$1$ ではない（$\neq 1$）」というのは矛盾（空集合）します。よってBの項は消去され、残った A の項が合体します。
新しい不整合（学習）: $\neg(A@1)$「Aが1であること自体がダメ」
この新しい不整合を得て初めて、不整合の対象がAのみとなり、$L_{prev}$ が0（あるいはAの依存元）まで下がります。ここでようやく $L_{max} (1) > L_{prev} (0)$ となり、「A=1 という決定自体を取り消す」バックトラックが可能になるのです。

4. 性能比較

PubGrubアルゴリズムを実装したものと、DPLLアルゴリズムを実装したものの性能比較を行いました。
テストケースとしてはランダムに生成した5000個のパッケージと、その依存関係を用いました。
以下がその結果です。

========================================
Results
========================================
Solution package count: 3050

Performance timing (microseconds)
  DPLL:    1982087 us (packages=3050)
  CDCL:   1566088 us (packages=3050)
  Speedup:  1.26563x (naive/solver)
  *** PubGrub solver is 1.26563x FASTER! ***

最終的にrootパッケージをインストールするのに3050個のパッケージが必要で、その解決にかかった時間はDPLL実装で約1982ミリ秒、PubGrub実装で約1566ミリ秒となりました。ちょっとコンフリクトで大きく戻るケースが少なかったので、あまり差が出ていませんが、PubGrub実装の方が約1.27倍くらい高速であることがわかりました。