バージョンの充足可能性問題

(注:2017/02/06、いただいたフィードバックを元に翻訳を修正いたしました。)

Dependency HellとはNP完全のことですが、この状態から脱することができるかもしれません。

パッケージにおけるバージョン選択の問題は、完全である(全ての依存関係を満たしている)かつ互換性のある(2つの非互換性のパッケージが選択されていない)トップレベルパッケージPをビルドするのに使うことができる依存関係のセットを見つけることです。ただし、菱形依存問題があるので、このようなセットは存在しない可能性があります。菱形依存問題とは、AはBとCが必要、BはDのバージョン2ではなくバージョン1が必要、CはDのバージョン1ではなくバージョン2が必要といったような問題のことです。この場合、Dの両方のバージョンを選択することはできないため、Aをビルドすることができないわけです。


パッケージのバージョンを選択するために、パッケージ管理システムにはアルゴリズムが必要となります。つまり、apt-get install perlを実行する際、システムがPerlの最新バージョンのことを指していると決めてかかるかもしれません。しかしこの場合、Perlの推移的依存関係を満たす方法を見つけるか、なぜPerlがインストールできないのか納得のいく説明を出力しなければなりません。この問題を解決するのに、最悪どのくらいのコストがかかるのかと、疑問に思うことでしょう。Perlをインストールすることができるかどうか判断するのに、パッケージ管理システムが何時間または何日、もしくは何年という時間を費やしてほしくないはずです。

残念ながら、バージョンを選択する問題はNP完全で、全ての入力に対して素早い実行が保証されたアルゴリズムを見つけられる見込みは非常に低いのです。この記事では、バージョン選択におけるNP完全性の検証を紹介するとともに、既存のパッケージ管理がどのように対処しているのかを見ていきながら、NP完全のタスクを避けるための有用なアプローチ方法を簡単にお話ししていきたいと思います。

NP完全性の検証

NP完全性を検証するためには、多様な出力のあるアルゴリズムの現代的な世界から、yesもしくはnoのどちらかを取るブーリアン出力を持つアルゴリズムである、複雑性理論の限定的な世界へと移行する必要があります。複雑性理論の世界では、VERSION問題(VERSIONは常に大文字)を定義し、有効なバージョン選択があるかどうかを要求します。ブーリアンのVERSION問題は私たちが持つ元々の問題の半分でしかなく、これがNP完全であることは証明可能です。この証明を行うには、VERSIONがNPに属していることと、そのVERSIONがNP困難であることの2つの異なる事実を証明する必要があります。

解 “yes” の全てに、検証が容易な多項式サイズの説明が含まれている場合、ある問題はNPに属することになります。

選択されたパッケージのバージョンをリストすることによって、解 “yes” のどれも説明することができるので、VERSIONはNPに属することになります。このリストは入力よりも大きくなることはなく、時間内に正確性を確認することができ、入力内の二次式よりも悪くなることはありません(計算モデルの詳細により、一次式の可能性もあります)。

ある問題に対する有効な解決策が、NPに属する全ての他の問題に対する有効な解決策に適合することができる場合、問題はNP困難となります。これは非常に難しい注文ではありますが、VERSIONにおける有効な解決策を、もう1つのNP困難の問題(HARDと呼びます)における有効な解決策に適応させることを証明するだけで十分です。そして、他の誰かが証明したHARDにおける有効な解決策が、NPに属するその他全ての問題における有効な解決策に適応できるという事実に依存すればいいのです。

NP完全(NPとNP困難)の有用な例に、充足可能性問題があります。充足可能性問題では、入力は、変数もしくはその変数の否定である、3つそれぞれのリテラルを論理和(OR)で結び、それらを論理積(AND)で結ぶように制限されたブーリアン変数のブーリアン方程式となります。充足可能性問題の入力として以下の例を挙げておきます(∧はAND、∨はOR、¬はNOT)。

(¬ x1 ∨ ¬ x2 ∨ ¬ x3) ∧ (¬ x2 ∨ ¬ x3 ∨ ¬ x4) ∧ (¬ x2 ∨ ¬ x2 ∨ x3) ∧ (x2 ∨ x2 ∨ x2)

x1 = 0、x2 = 1、x3 = 1、x4 = 0のように、変数にこのような組み合わせの数値を代入することによって充足可能になります。よって解はyesです。

以下のように、項をもう1つ追加した場合はどうでしょうか。

(¬ x1 ∨ ¬ x2 ∨ ¬ x3) ∧ (¬ x2 ∨ ¬ x3 ∨ ¬ x4) ∧ (¬ x2 ∨ ¬ x2 ∨ x3) ∧ (x2 ∨ x2 ∨ x2) ∧ (x1 ∨ ¬ x2 ∨ x4)

この場合、変数にどのような値を代入しても充足不可能なので、解はnoです。

充足可能性問題のインスタンスにおける一般的な形式は、変数V1からVm,に対する項C1からCnの論理積で、各Ciは3つのリテラル、各xjまたは、いくつかの変数xjにおける¬ xjの論理和である方程式Fとなります。項にある重複したリテラルは、上記にある(¬ x2 ∨ ¬ x2 ∨ x3)や(x2 ∨ x2 ∨ x2)のようにすることができます。

どのような充足可能性問題のインスタンスでも、同じ解となるVERSIONのインスタンスに置き換えることができます。パッケージ管理については、以下についてのみ仮定することとします。

  1. パッケージは0個以上のパッケージまたは特定のパッケージのバージョンを依存関係としてリストすることができる。
  2. パッケージをインストールするには、依存関係のあるこれら全てのパッケージがインストールされなければならない。
  3. パッケージの各バージョンは、異なる依存関係を持つことができる。
  4. 2種類の異なるバージョンのパッケージを同時にインストールすることはできない。

バージョンVのパッケージPをP:V(方程式の標準数式イタリックと区別するためにパッケージについては等幅フォントを使用しています)という形に省略します。P:Vの依存関係は、V-1やV+1ではなく、バージョンVによって完全に満たされなくてはなりません。

充足可能性問題の方程式が与えられれば、パッケージFを作成することができます。このFは、パッケージC1、C2、Cnといった全体の方程式を表しており、Cnは各項を、パッケージX1、X2、Xmなどは各変数を表しています。

各パッケージXjはXj:0とXj:1という2つのバージョンを持っています。上記のことを仮定した場合、Xj:0とXj:1は競合関係にあり、両方をインストールすることはできません。元々の方程式では、インストールされているXj:1がxj=1に対応しています。

パッケージCiは数字0、1、2という3つのバージョンを持っていて、それぞれのバージョンは対応する項のリテラルによって決まります。例えば、C5が(x1 ∨ ¬ x2x4)である場合、C5:0がX1:1に、C5:1がX2:0に、C5:2がX4:1によって決まります。元々の方程式では、インストールされているCi:kは、真であるCik番目のリテラルに対応します(結果、Ciが真となります)。

パッケージFは、C1、C2、…、Cnによって決まります。インストールされているFは、全てのCiがインストールされることを示しており、これによって真となる全てのCiに対応することになるので、結果、Fが真となります。

パッケージ管理がパッケージFをインストールする方法を見つけることができれば、元々の方程式における満足する代入は、各変数xjに対するXjのインストール状態から読み出すことができます。同様に、方程式が充足可能なのであれば、満足できる代入は、パッケージ管理がFのインストールを問題なく実行する1つの方法を与えてくれるでしょう。それ故に私たちは、同じ解法を用いることで、充足可能性問題のインスタンスを、一致するVERSIONのインスタンスに置き換えました。これにより、充足可能性問題はVERSIONを使うことで解決できると定めることができ、VERSIONはNP困難ということになります。

VERSIONがNPに属していてNP困難であることから、VERSIONはNP完全となります。

実装

上記はかなり最低限の場合を想定しています。パッケージは依存関係のリストを持っていて、パッケージの依存関係は独自のバージョンからバージョンに変更することが可能。パッケージの依存関係は特定の依存関係のバージョンを制限し、2つのパッケージのバージョンをお互いに競合関係にすることが可能。これはパッケージ管理システムを役立たせるには最低限必要なことでしょう。いくつかのパッケージ管理では、依存関係が特定のバージョンをリストすることを許可しない代わりに、範囲を必要とします。しかし、バージョンの必要条件0と1は≤ 0と≥ 1へと簡単に変更することができます。いくつかのパッケージ管理は、初期設定でパッケージの異なるバージョンの競合を想定できないかもしれませんが、最低でも次に挙げるようなことは特定することは可能かもしれません。Unixシステムに2つの/bin/bashが存在することはない、または、printfという2つの定義がCプログラムに組み込まれている。

仮定は、調べた全てのパッケージ管理システムにおいて真です。調べたシステムは、DebianのAPT、RedHatのRPM、RustのCargo、Nodeのnpmjs、JavaのMaven、HaskellのCabal、またその他複数です。どうやらパッケージ管理の実装で直面するのは、NP完全のタスクのようです。インストールの方法を決めるために長い時間を要する可能性があるのか、それともインストールできないものとしてインストール可能なパッケージのレポートするのかを、それぞれが選択しなくてはなりません(もちろん、何らかの事情により、所与の実装が両方を行うこともあります)。

KnuthはThe Art of Computer Programming Volume 4, Fascicle 6で以下のように記述しています。

充足可能性の話は、美しい数学を織り交ぜたソフトウェアエンジニアリングの勝利を語るものです。見事な新しいデータ構造やその他のテクニックのおかげです。このような問題は数年前まで不可能と考えられていましたが、現代のSATソルバは、多くの変数が絡んだ現実の問題に当たり前のように対処できるようになっています。

実際のところ、現代のパッケージ管理はSATソルバの使用へと移行し始めています。

0installはヒューリスティックから開始しましたが、SATソルバに移行することが必要だと分かりました

システム統合フレームワークであるChefは、Gecodeの制約ソルバのためのRubyバインディングのdep-selectgorを使っています。

Dartのpubには、しばしば長い時間を要するバックトラッキングのソルバが含まれています。

Debianのapt-getは、初期設定でヒューリスティックを使っていますが、SATソルバを呼び出すことができ、ユーザプリファレンスを考慮することもできます。また、Debianの品質保証チームは、リポジトリ内でインストールできないパッケージを特定するためにソルバを実行しています

Eclipseは、プラグインの実装を管理するために、sat4j SATソルバを使っています。

FedoraのDNF(または “Dandified yum” )では、実験モードでSATソルバを使っています。

FreeBSDのpkg(DragonflyBSDでも使われています)では、picosat SATソルバを使っています。

OCamlのOPAMは、ローカルまたはネットワークを介してリモートでSATソルバを呼び出すことができます。Debianのapt-getのように、OPAMのソルバはユーザプリファレンスを考慮することができ、OPAMのリポジトリはインストールできないパッケージに対してスキャンが実行されます。

Open SUSEのパッケージ管理は、 “充足可能性のアルゴリズムを使っているフリーパッケージの依存関係ソルバ” であるlibsolvを使っています。また、独自のlibzyppSATソルバを使うOpenSUSEのzypperもあります。

PythonのAnacondaは、SATソルバを使っていますが、長い時間を要します

RustのCargoでは、基本的なバックトラッキングソルバを使っています。これは、複数のバージョンが最終的なバイナリにリンクされることを許可します。

Illumosでも使用され、またIPSとしても知られるSolarisのpkgは、minisat SATソルバを使っています

Swiftのパッケージ管理では、基本的なバックトラッキングソルバを使っています。

(こちらに他のパッケージ管理を追加したいと思っているので、詳細をご存じの方(または記載されている内容に間違いがある場合)は私宛にメールしていただくかツイートを送ってください。よろしくお願いします)

代替案?

パッケージのバージョン選択がNP完全であるという事実に、私たちはどう反応すべきでしょうか? 1つの反応としては、複雑性を受け入れ、SATソルバが有能であることに感謝することでしょう。別の反応としては、これが良い方法なかどうかを問いかけてみることです。この問題を解決することを要求するようなツールをビルドすべきではないかもしれませんし、またソフトウェアを開発する過程で何か不具合が起こる可能性もあります。

パッケージのバージョン選択がNP完全問題なのであれば、それはつまり、考えられるパッケージの組み合わせの探索空間が大きく、効率の良い体系的分析が複雑だということです。効率の良い統計的テストはどうでしょうか? もし、探索で競合しない組み合わせを見つけた場合、組み合わせが機能するとなぜ信じることができるのでしょう? バージョンの競合がないということは、組み合わせがテストされていないということだけを意味します。探索が競合しない組み合わせを見つけられなかった場合、次のステップを明確にするために、開発者にその失敗をどのように説明することができるでしょう? NP完全を自らのソフトウェアのコンフィギュレーションの決定に受け入れることをせずに、ソフトウェアをきちんと理解するのは非常に難しいものです。それでは、ここまでのおさらいと、どのように回避できるかを検証していきましょう。

上に示した証明は、前述の仮定に左右されます。その仮定をもう一度、以下に示しておきます。

  1. パッケージは0個以上のパッケージまたは特定のパッケージのバージョンを依存関係として列挙できる。
  2. パッケージをインストールするには、依存関係のあるこれら全てのパッケージがインストールされなければならない。
  3. パッケージの各バージョンは異なる依存関係を持つことができる。
  4. 2種類の異なるバージョンのパッケージを同時にインストールすることはできない。

先に私が提示したように、これらは “パッケージ管理を役立つものとするための必要最低限” に相当する、と一般に通用しています。しかし、最終的にはこの仮定を削減する方法を見つけることができるかもしれません。

NP完全性を回避するための1つの方法は、仮定1に取り組むことです。もし仮に、依存関係に、特定のパッケージのバージョンをリストするのではなく、最小バージョンしか明記できないとしたらどうなるでしょう? この場合は、使用するパッケージを見つけるために、次のようなちょっとしたアルゴリズムがあります。インストールしたいものの最新バージョンから始めて、その全ての依存関係の最新バージョンを、再帰的に入手します。この記事の冒頭、最初の菱形依存問題で、AはBとCを必要とし、BとCは異なるバージョンのDを必要とします。BはD 1.5を必要とし、CはD 1.6が必要とするなら、ビルドは両方に対しD 1.6を使うことができます。もし、BがD 1.6で動作しないなら、BのバージョンあるいはD 1.6のどちらかにバグがあると考えられます。バグのあるバージョンは配布から完全に削除しなければなりません。またその後、新しくリリースしたバージョンで問題を修正する必要があります。逆に依存関係グラフに競合を加えることは、問題を修正せずにバグを添付しているようなものです。

NP完全性を回避するもう1つの方法は、仮定4に取り組むことです。もし仮に、2つの異なるバージョンのパッケージを同時にインストールすることができるとしたらどうなるでしょう。ほとんど全ての探索アルゴリズムは、プログラムをビルドするためのパッケージの組み合わせを見つけるでしょう。それは、もしかすると最小限の組み合わせではないかもしれません(それはまだNP完全です)。BがD 1.5を必要とし、CがD 2.2を必要とするなら、ビルドは、両方を最終的なバイナリに含めて、個別のパッケージとして扱うことができます。上述のように、2種類のprintfの定義をCプログラムに組み込むことはあり得ませんが、明示的モジュールシステムを有する言語は、(完全修飾が異なるという保証の下)Dの個別のバージョンをプログラムに含めることに、何の問題もありません。

NP完全性を回避する別の方法は、上で述べた2つを組み合わせることです。すでに示した例のように、もしパッケージがセマンティック バージョニングに従えば、パッケージ管理は自動的にメジャーバージョンの中から最新バージョンの依存関係を使うでしょう。しかしその一方で、異なるメジャーバージョンを別のパッケージとして扱います。

このような制限の根本原理の1つは、開発者がソフトウェアをビルドしたりテストしたりする際に、全ての考え得るパッケージの組み合わせ全体について考えていない可能性があるということです。この考えは、ソフトウェアがどのようにビルドされているかについて開発者とそのツールの整合性を保つために、重要です。これらのアプローチのいずれかが、実際に実行されるようになれば、言語のパッケージ管理の動作と理解性の簡素化に大いに効果があるでしょう。

関連著書

DebianとRedHatのパッケージのインストレーションがNP完全であるという証明は、EDOS dekuveravke WP2-D2.1、ソフトウェア依存関係の形式的管理に関する報告書(2005年)の49~50ページに掲載されています。インストレーションをパッケージ化するための充足可能性問題の削減における、困難な手順は論理和をどのように構成するかということです。EDOSの証明は、単一の依存関係に対する代替リストを特定するパッケージ管理の機能を使って、直接に(Debianの場合)、あるいは “provides” 名令(RedHatの場合)を用いて、論理和をエンコードします。例えば、これらのシステムでは、実際のパッケージ、edviacmeのいずれかがインストールされる際に、pseudo-packageのtext-editorがインストール済とみなされる、と定義することができます。

RustのCargoのような言語のパッケージ管理の、依存関係の仕様書はDebianやRedHatの仕様書よりもはるかに簡素なものです。ですから、EDOSの証明は当てはまりません。そのため、言語のパッケージ管理はより簡単な(NP完全ではない)ジョブに直面することが望まれるかもしれません。上述の新しい証明はその望みをはねのけてくれるでしょう。(この証明を確認するための1つの方法は、edviacmeのそれぞれに由来する3つのバージョンのtext-editorパッケージを定義して、最後の例で述べた “provides” 命令をシミュレートすることです。)

パッケージの異なるバージョンの依存関係を変更して論理和をエンコーディングすれば、DebianやRedHatのパッケージ管理の両方に対して、修正することなく新しい証明が機能するだけでなく、いかなる予見可能なオペレーティングシステムや言語パッケージ管理に本質的に適用できるのです。言語のパッケージ管理の作成者のほとんどは、自分たちが直面した問題をNP完全とみなしていたと想像していますが、その事実が以前に証明された書面を見つけることはできていません。

依存関係を持つ、いくつかのシステムではSATソルバの代わりに制約ソルバを使っています。しかし、根本的な問題は、やはりNP完全です。

2008年、Daniel Burrowsはdpkgを用いた数独問題の解法に関する記事をブログに投稿しました。

EDOS報告書を私に示唆してくれたSam Boyerと、彼の優れたパッケージマネージメントの概要に感謝します。

Roberto Di Cosmoは、EDOS報告書に続くものをたくさん書いています。こちらがそのリストです。特に、依存関係の解法、コンポーネントの進化するマネジメントでの個別の懸念には、最新版の証明が含まれています。その一連の研究はSATソルバに適用するだけでなく、ユーザプリファレンスを考慮に入れて動作します。

また別の関連著書には、2007年ICSEで発表されたTuckerらの
OPIUM、最適なパッケージのインストール/アンインストール管理、があります。OPIUMは0installソルバの出発点です。

Jaroslav Tulachは2009年に、上で述べたのと同じ証明を発見しました。ハンドル名edwintorokという読者のリンクに感謝します。

Webサイト、LtUでのTulachの証明に関する議論では、2005年のDaniel Burrowsの論文「ソフトウェア依存関係のモデリングとリゾルビング」に触れていますが、この論文の証明は、Tulachの証明/上述の証明よりもEDOSの証明に近いでしょう。

多くの読者が、参考文献や、SATソルバを有するパッケージ管理の追加のリンクを送ってくれました。みなさんどうもありがとうございます。