依存解決とバージョン制約充足（SATソルバ）

依存解決は「制約充足問題」である

パッケージマネージャがやっていることは、表面的には「必要なライブラリを集める」ですが、内部では純粋な制約充足問題（CSP）を解いています。入力は、各パッケージが宣言する依存とバージョン制約（例 requests >=2.0,<3.0）の集合。求めるのは、すべての制約を同時に満たす「パッケージ→バージョン」の割り当てです。

この問題はブール論理に機械的に変換できます。「パッケージ p のバージョン v を採用する」という命題を真偽変数 x_p_v とみなすと、依存関係は次のような節（クローズ）になります。

各パッケージは高々1バージョン:  x_p_v1, x_p_v2, ... のうち真は1つ以下
ルートが requests を要求:        (x_requests_2.0 OR x_requests_2.1 OR ...)
A@1.0 が requests <3.0 を要求:   x_A_1.0 → (満たすバージョンのOR)

これらの節をすべて真にする割り当てが存在するか——これはまさにSAT（ブール充足可能性問題）です。SATは最初にNP完全と証明された問題であり、したがって一般のバージョン解決もNP困難です。入力次第で組合せ爆発が起き、解けるが時間がかかる、あるいは矛盾の証明に時間がかかるケースが原理的に存在します。

ダイヤモンド依存：衝突はどこで起きるか

依存衝突のほぼすべてはダイヤモンド依存に帰着します。ルート R が A と B に依存し、A も B も共通のライブラリ C に依存するが、要求する制約が食い違う、という形です。

        R
       / \
      A   B
       \ /
        C        A は C >=1.0,<2.0
                 B は C >=1.5,<3.0  → 交差 [1.5, 2.0) が解
                 B が C >=2.0 なら   → 交差が空集合 = 解なし

C に課された制約の区間の交わりが空でなければ解があり、空なら充足不能です。区間が1次元なら交差判定は容易ですが、現実には数百のパッケージが相互に制約し合い、あるパッケージのバージョン選択が別の依存ツリーを開いて新たな制約を生むため、探索空間が指数的に膨らみます。ここがNP困難性の発生源です。

フラット解決は依存ツリー全体で C をただ1つに固定するため、衝突すると解決そのものが失敗します。ネスト解決（古典的な npm の node_modules 入れ子）は A 用の C と B 用の C を別々に置けるため衝突を物理的に回避できますが、同じコードが複数版ロードされる、型やシングルトンが食い違う、ディスクが膨らむ、といった代償を払います。

最新優先か、最近接優先か——選択戦略

制約を満たす解が複数あるとき、どれを選ぶかは別問題です。ここでソルバのポリシーが分かれます。

多くのソルバ（PubGrub, Cargo, 近年の pip）は最新優先で、制約を満たす範囲のなるべく新しい版を選びます。Maven は歴史的に最近接優先（ツリー上でルートに近い宣言が勝つ）で、これは高速だが「より深い場所のより新しい安全な版」を見落とすことがあります。Go modules の **MVS（Minimal Version Selection）**は逆に「要求を満たす最小版」を選び、誰も明示的に上げない限りバージョンが勝手に上がらないため、極めて決定的で高速です。

ロックファイル：解いた結果を固定する

SATを毎回解き直すのは遅く、しかも上流に新版が出ると解が変わって再現性が壊れます。これを防ぐのがロックファイル（package-lock.json, Cargo.lock, poetry.lock, go.sum/go.mod 等）です。

ロックファイルは制約（^1.2.0 のような幅のある宣言）ではなく、解決済みの確定バージョンと取得元・ハッシュを記録した成果物です。つまり「制約 = 入力」「ロックファイル = ソルバの出力をシリアライズしたもの」という関係になります。

manifest（入力）:   requests = "^2.0"         ← 幅のある制約
lockfile（出力）:   requests == 2.31.0
                   sha256 = a1b2c3...         ← 完全性検証

ロックファイルがあれば、CI も本番も同じビットのツリーを再構築でき、ハッシュ照合でサプライチェーン改ざんも検知できます。CI/CD パイプラインで npm ci や cargo build --locked のように「ロックを尊重し再解決しない」モードを使うのは、ビルドの決定性を保証するためです。逆にロックを無視して毎回解き直すと、ビルドのたびに別バージョンが入りうる非決定的ビルドになります。

NP困難性とどう付き合うか

理論上NP困難でも、実務の依存グラフの多くは現実的な時間で解けます。ソルバは充足不能を高速に証明する工夫を積んでいます。

• 節学習（CDCL）：衝突に到達したら、その原因となった制約の組合せを新しい節として学習し、同じ袋小路を二度と探索しない。PubGrub の核心はこれで、しかも人間に読める衝突説明（「A は C 2.x を要求し B は C 1.x を要求する」）を生成できます。
• 単位伝播：あるパッケージの版が一意に決まると、それが連鎖的に他の選択を確定させ、探索空間を刈り込む。
• MVS のような単純化：Go のように戦略自体を決定的・線形時間で解ける形に制限すれば、そもそもバックトラックが起きません。

依存解決のエラーに当たったら、まず「これは充足不能（解がない）か、探索の都合（解はあるが見つからない）か」を切り分けます。前者なら制約を緩めるかパッケージを更新し、後者ならソルバの提案するピン留めや、アーティファクトレジストリ でミラーした既知良好版への固定が有効です。仕組みを「SATを解いてロックに固定している」と捉えれば、エラーメッセージの意味も対処も一段クリアになります。

まとめ

• バージョン制約充足はSAT／SMT問題と等価で一般にNP困難。だから依存解決は原理的に遅く・難しくなりうる。
• 衝突の核心はダイヤモンド依存。フラット解決は単一版に統一して失敗しうる、ネスト解決は複数版共存で回避する。
• 解が複数あるときの選び方が戦略：最新優先・最近接優先・MVS。解の存在とポリシーは別問題。
• ロックファイルは「制約を解いた確定版」を固定する成果物で、再現性と完全性検証を担う。アプリはコミット、ライブラリは制約のみ公開が原則。
• CDCL（節学習）・単位伝播・MVS のような単純化により、NP困難でも実務の多くは現実的時間で解け、衝突は人間可読に説明できる。