openSUSE:Libzypp SAT ソルバー
依存関係の解決
依存関係の処理は、 Linux における ソフトウエア管理アプリケーション における中枢機能とも呼べるものです。
依存関係 とは、複数のソフトウエア要素に機能を分割したり、その分割した機能をパッケージ間で共有したりするための仕組みです。
Linux (および Unix) では 分割統治法 を実装するための 2 つの基本的な考え方、具体的には巨大な問題を小さく分割し、管理しやすくするための考え方に従っています。
それぞれのソフトウエアパッケージには、他のパッケージに提供する機能が記されていて、依存関係の処理では、その情報をもとに必要なものを洗い出します。
依存関係解決器 は、ソフトウエアの管理にあたってこれらの関係性をチェックしたり、充足させたりするために使用します。
解決の基本的な流れ
依存関係解決器は、下記の 2 つの基本的なルールをベースにして、ユーザの操作なく依存関係を解決しようとします。
- 起動時に指定されたインストールや削除の要件を満たすこと。
- インストール済みのシステムの一貫性を維持すること。
解決器はそれぞれのパッケージを同じように扱うことから、これらのルールには暗黙の仕組みが含まれています。暗黙の仕組みには大きいものから予期しないものまでありますが、いずれにしても、依存関係が壊れてしまうと多数のパッケージを削除するように動作してしまうことに注意してください。そのような場合、処理後のシステムは一貫性が保たれているものの、ほぼ利用できないシステムになってしまいます。
機能
パッケージの依存関係を計算するにあたっては、 充足可能性解決器 と呼ばれる仕組みを使用します。これは パッケージ管理#パッケージの依存関係 を 充足可能性問題 として解決する仕組みをベースにしています。
背景と情報
openSUSE 11.0 における SAT ソルバーの実装は、 2 つのメジャーかつ独立したブロックをベースにしています:
- パッケージや依存関係の情報を保存したり取り出したりする際には、辞書型のアプローチを使用する。
- 充足可能性と呼ばれる、既知のよく調査される方法を利用して、パッケージの依存関係を計算する。
充足可能性解決器をパッケージの依存関係の解決に使用する際の基本は、 SAT ソルバーの基本 および SAT ソルバーの内部 で詳しく説明しています。
開発者向けドキュメンテーション
さらに詳しく
SAT ソルバーを利用するツールやライブラリです。