版の制約と依存の解決

次の組を依存の解決問題の入力という。

• パッケージの有限集合 $P$ と、各 $a \in P$ の版の有限集合 $V_a \subseteq \mathbb{N}$。
• 各パッケージ $a$ の各版 $v \in V_a$ がもつ制約の有限集合 $\mathrm{Req}(a, v)$。制約は組 $(b, S)$（$b \in P$、$S \subseteq V_b$）で、「$b$ が必要で、その版は $S$ に属すること」を表す。
• 作ろうとしているプログラム自身の制約の有限集合 $\mathrm{Req}_0$（根の制約）。

部分写像 $\rho : P \rightharpoonup \mathbb{N}$ で、$\rho(a) \in V_a$ であり、

• (R1) $(b, S) \in \mathrm{Req}_0$ ならば、$b$ は $\rho$ の定義域に属し $\rho(b) \in S$、
• (R2) $a$ が $\rho$ の定義域に属し $(b, S) \in \mathrm{Req}(a, \rho(a))$ ならば、$b$ は $\rho$ の定義域に属し $\rho(b) \in S$、

を満たすものを解決という。$\rho$ は各パッケージに高々 1 つの版を選ぶ。入力（$S$ は元を列挙して表す）が与えられたとき、解決が存在するかを問う判定問題を $\mathrm{RESOLVE}$ と書く。