SAT解決策の統合
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/10/11 14:21 UTC 版)
Libzyppが改善を必要とした部分は、依存解決策の速度であった。libsolvは修正BSDライセンスの下で書かれてリリースされている。 Optimal Package Install/Uninstall Manager (OPIUM) やMANCOOSIなどのプロジェクトは、SAT解決策で依存関係の問題を解決しようとしていた。Advanced Packaging Tool (APT) などの伝統的な解決策では、時に容認できない欠陥が明らかになる。ZYppスタックにSATアルゴリズムと統合することが決定した。使われる解決アルゴリズムは有名なMinisatの解決策を基本にしたものであった。openSUSE 11.0で見えたSAT解決の実装は2つのメジャーではあるが独立したブロックを基本としている: パッケージや依存情報を保存して取り出すためにデータ辞書アプローチを使う。新しいsolv形式が作成され、これはリポジトリを文字列辞書、関係辞書、そして全てのパッケージ依存物として貯蔵する。複数のsolvリポジトリを読み込んでマージするための所要時間はわずか数ミリ秒である。 パッケージ依存の算出に充足可能性を利用する。充足可能性問題はよく研究された問題であり利用可能な多くの模範解決策がある。パッケージ解決策の複雑さは、SAT解決策を利用する他の領域よりもはるかに単純であるため、模範パッケージ解決策はとても高速である。さらにそれは複雑なアルゴリズムを必要としないため、問題解決が不可能な理由の証明を導いて理解可能な提案を提供できる。 数ヶ月の作業の後、SAT解決策と統合されたこの4代目ZYppバージョンのベンチマーク結果は期待以上のものであり、YaSTやZypperは他のRPMベースのパッケージマネージャよりもスピードやサイズが勝った状態で動作する。
※この「SAT解決策の統合」の解説は、「ZYpp」の解説の一部です。
「SAT解決策の統合」を含む「ZYpp」の記事については、「ZYpp」の概要を参照ください。
- SAT解決策の統合のページへのリンク
