OSGi NP-Complete 中的解析问题是否存在？
解决问题在 OSGi R4 核心规范的模块化章节中进行了描述。这是一个约束满足问题，当然也是一个需要有效解决的具有挑战性的问题，即不能通过蛮力解决。主要的复杂性是使用限制，它具有非局部影响，以及放弃可选导入以获得成功解决方案的自由。
NP 完整性在 StackOverflow 上的其他地方进行了处理。
关于这个问题的答案已经有很多猜测，所以请避免猜测。好的答案将包括一个证明，或者，如果失败的话，一个令人信服的非正式论证。
这个问题的答案对于那些为 OSGi 构建解析器的项目（包括 Eclipse Equinox 和 Apache Felix 开源项目）以及更广泛的 OSGi 社区来说很有价值。
The resolution problem is described in the modularity chapter of the OSGi R4 core specification. It's a constraint satisfaction problem and certainly a challenging problem to solve efficiently, i.e. not by brute force. The main complications are the uses constraint, which has non-local effects, and the freedom to drop optional imports to obtain a successful resolution.
NP-Completeness is dealt with elsewhere on StackOverflow.
There has already been plenty of speculation about the answer to this question, so please avoid speculation. Good answers will include a proof or, failing that, a compelling informal argument.
The answer to this question will be valuable to those projects building resolvers for OSGi, including the Eclipse Equinox and Apache Felix open source projects, as well as to the wider OSGi community.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
是的。
edos 论文 Pascal 引用的方法可以与 OSGi 一起使用。下面我将展示如何将任何 3-SAT 实例减少为 OSGi 捆绑包解析问题。该网站似乎不支持数学符号，因此我将使用程序员熟悉的符号来代替。
这是我们试图简化的 3-SAT 问题的定义：
首先将 A 定义为一组命题原子及其否定 A = {a(1), … ,a(k),na(1), … ,na(k)}。用更简单的语言来说，每个 a(i) 都是一个布尔值，我们定义 na(i)=!a(i)
那么 3-SAT 实例 S 的形式为： S = C(1) & ……& C(n)
其中 C(i) = L(i,1) | L(i,2) | L(i,2) | L(i,3) 且每个 L(i,j) 都是 A 的成员
解决特定的 3-SAT 实例涉及为 A 中的每个 a(i) 找到一组值（真或假），使得 S 计算为真的。
现在让我们定义将用于构建等效解决问题的捆绑包。以下所有捆绑包和包版本均为 0，并且导入版本范围不受限制，除非另有说明。
现在从原子开始进行约束：
BA(j) 版本 1
-导出包 PA(j) 版本 1
-对于包含原子 a(j) 的每个子句 C(i)，导出 PM(i) 并将 PA(j) 添加到 PM(i) 的使用指令
BA(j) 版本 2
-导出包 PA(j) 版本 2
-对于包含否定原子 na(j) 的每个子句 C(i)，导出 PM(i) 并将 PA(j) 添加到 PM(i) 的使用指令
BC(i)
-导出PC(i)
-导入PM(i)并将其添加到PC(i)的uses指令中
-对于子句 C(i) 中的每个原子 a(j) 可选择导入 PA(j) 版本 [1,1] 并将 PA(j) 添加到 PC(i) 导出的使用指令
-对于子句 C(i) 中的每个原子 na(j) 可选择导入 PA(j) 版本 [2,2] 并将 PA(j) 添加到 PC(i) 导出
BS
-无出口
-对于每个子句 C(i) 导入 PC(i)
-对于 A 中的每个原子 a(j) import PA(j) [1,2]
几句话解释：
子句之间的 AND 关系是通过让 BS 从每个 BC(i) 导入一个包 PC(i) 来实现的仅由该捆绑包导出。
OR 关系之所以有效，是因为 BC(i) 导入包 PM(i)，该包仅由代表其成员的包导出，因此必须至少存在其中一个，并且因为它可以选择从每个包导入一些 PA(j) 版本 x代表一个成员的包，该包唯一的包。
BA(j) 版本 1 和 BA(j) 版本 2 之间的 NOT 关系由使用约束强制执行。 BS 导入每个包 PA(j) 时没有版本限制，因此它必须为每个 j 导入 PA(j) 版本 1 或 PA(j) 版本 2。此外，uses 约束确保子句包 BC(i) 导入的任何 PA(j) 充当 BS 类空间的隐含约束，因此如果 PA(j) 的两个版本都出现在其隐含中，则 BS 无法解析限制。因此解中只能存在 BA(j) 的一个版本。
顺便说一句，有一种更简单的方法来实现 NOT 关系 - 只需将 singleton:=true 指令添加到每个 BA(j) 中即可。我没有这样做，因为单例指令很少使用，所以这看起来像是作弊。我只是提到它，因为在实践中，我所知道的 OSGi 框架在面对可选导入时没有正确实现使用基于包的约束，因此，如果您要实际使用此方法创建包，然后测试它们可能是一次令人沮丧的经历。
其他备注：
不使用可选导入的 3-SAT 的减少也是可能的，尽管这更长。它基本上涉及一个额外的捆绑层来模拟使用版本的可选性。减少 1-in-3 SAT 相当于减少 3-SAT，看起来更简单，尽管我还没有经历过。
除了使用 singleton:=true 的证明之外，我所知道的所有证明都取决于使用约束的传递性。请注意，singleton:=true 和传递使用都是非局部约束。
上面的证明实际上表明 OSGi 解析问题是 NP 完全或更糟的。为了证明情况并不更糟，我们需要证明问题的任何解决方案都可以在多项式时间内得到验证。大多数需要检查的事情都是本地的，例如查看每个非可选导入并检查它是否连接到兼容的导出。验证这些是 O(num-local-constraints)。基于 singleton:=true 的约束需要查看所有单例包并检查没有两个具有相同的包符号名称。检查数量小于 num-bundlesnum-bundles。最复杂的部分是检查是否满足使用约束。对于每个捆绑包，这涉及遍历使用图来收集所有约束，然后检查这些约束是否与捆绑包的导入相冲突。任何合理的行走算法只要遇到一条电线或使用之前见过的关系就会返回，因此行走的最大步数是（框架中的线数 + 框架中的使用数）。检查一条线路或使用关系之前是否未被走过的最大成本小于此日志。一旦收集到受约束的包，每个包的一致性检查成本就小于 num-imports-in-bundlenum-exports-in-framework。这里的一切都是多项式或更好的多项式。
Yes.
The approach taken by the edos paper Pascal quoted can be made to work with OSGi. Below I’ll show how to reduce any 3-SAT instance to an OSGi bundle resolution problem. This site doesn’t seem to support mathematical notation, so I’ll use the kind of notation that’s familiar to programmers instead.
Here’s a definition of the 3-SAT problem we’re trying to reduce:
First define A to be a set of propositional atoms and their negations A = {a(1), … ,a(k),na(1), … ,na(k)}. In simpler language, each a(i) is a boolean and we define na(i)=!a(i)
Then 3-SAT instances S have the form: S = C(1) & … & C(n)
where C(i) = L(i,1) | L(i,2) | L(i,3) and each L(i,j) is a member of A
Solving a particular 3-SAT instance involves finding a set of values, true or false for each a(i) in A, such that S evaluates to true.
Now let’s define the bundles we’ll be use to construct an equivalent resolution problem. In the following all bundle and package versions are 0 and import version ranges unrestricted except where specified.
Now for the constraints, starting with the atoms:
BA(j) version 1
-export package PA(j) version 1
-for each clause C(i) containing atom a(j) export PM(i) and add PA(j) to PM(i)’s uses directive
BA(j) version 2
-export package PA(j) version 2
-for each clause C(i) containing negated atom na(j) export PM(i) and add PA(j) to PM(i)’s uses directive
BC(i)
-export PC(i)
-import PM(i) and add it to the uses directive of PC(i)
-for each atom a(j) in clause C(i) optionally import PA(j) version [1,1] and add PA(j) to the uses directive of the PC(i) export
-for each atom na(j) in clause C(i) optionally import PA(j) version [2,2] and add PA(j) to the uses directive of the PC(i) export
BS
-no exports
-for each clause C(i) import PC(i)
-for each atom a(j) in A import PA(j) [1,2]
A few words of explanation:
The AND relationships between the clauses is implemented by having BS import from each BC(i) a package PC(i) that is only exported by this bundle.
The OR relationship works because BC(i) imports package PM(i) which is only exported by the bundles representing its members, so at least one of them must be present, and because it optionally imports some PA(j) version x from each bundle representing a member, a package unique to that bundle.
The NOT relationship between BA(j) version 1 and BA(j) version 2 is enforced by uses constraints. BS imports each package PA(j) without version constraints, so it must import either PA(j) version 1 or PA(j) version 2 for each j. Also, the uses constraints ensure that any PA(j) imported by a clause bundle BC(i) acts as an implied constraint on the class space of BS, so BS cannot be resolved if both versions of PA(j) appear in its implied constraints. So only one version of BA(j) can be in the solution.
Incidentally, there is a much easier way to implement the NOT relationship - just add the singleton:=true directive to each BA(j). I haven’t done it this way because the singleton directive is rarely used, so this seems like cheating. I’m only mentioning it because in practice, no OSGi framework I know of implements uses based package constraints properly in the face of optional imports, so if you were to actually create bundles using this method then testing them could be a frustrating experience.
Other remarks:
A reduction of 3-SAT that doesn't use optional imports in also possible, although this is longer. It basically involves an extra layer of bundles to simulate the optionality using versions. A reduction of 1-in-3 SAT is equivalent to a reduction to 3-SAT and looks simpler, although I haven't stepped through it.
Apart from proofs that use singleton:=true, all of the proofs I know about depend on the transitivity of uses constraints. Note that both singleton:=true and transitive uses are non-local constraints.
The proof above actually shows that the OSGi resolution problem is NP-Complete or worse. To demonstrate that it’s not worse we need to show that any solution to the problem can be verified in polynomial time. Most of the things that need to be checked are local, e.g. looking at each non-optional import and checking that it is wired to a compatible export. Verifying these is O(num-local-constraints). Constraints based on singleton:=true need to look at all singleton bundles and check that no two have the same bundle symbolic name. The number of checks is less than num-bundlesnum-bundles. The most complicated part is checking that the uses constraints are satisfied. For each bundle this involves walking the uses graph to gather all of the constraints and then checking that none of these conflict with the bundle’s imports. Any reasonable walking algorithm would turn back whenever it encountered a wire or uses relationship it had seen before, so the maximum number of steps in the walk is (num-wires-in-framework + num-uses-in framework). The maximum cost of checking that a wire or uses relationship hasn't been walked before is less than the log of this. Once the constrained packages have been gathered the cost of the consistency check for each bundle is less than num-imports-in-bundlenum-exports-in-framework. Everything here is a polynomial or better.
本文提供了一个演示：http://www.cse.ucsd.edu /~rjhala/papers/opium.html
This paper provides a demonstration: http://www.cse.ucsd.edu/~rjhala/papers/opium.html
根据记忆，我认为这篇论文包含了演示，很抱歉之前没有检查过。这是我打算复制的另一个链接，我确信它在第 48 页上提供了演示：http://www.edos-project.org/bin/download/Main/Deliverables/edos%2Dwp2d1.pdf
From memory I thought this paper contained the demonstration, sorry for not checking that out before. Here is other link that I meant to copy that I'm sure provides a demonstration on page 48: http://www.edos-project.org/bin/download/Main/Deliverables/edos%2Dwp2d1.pdf