osgi - OSGi NP-Complete 中的分辨率问题吗？

Question

OSGi R4 core specification的模块化章节中描述了解析问题。 .这是一个约束满足问题，当然也是一个要有效解决的具有挑战性的问题，即不是通过蛮力解决。主要的并发症是使用约束，它具有非本地效应，以及放弃可选导入以获得成功解决方案的自由。

NP-Completeness 处理 elsewhere在 StackOverflow 上。

关于这个问题的答案已经有很多猜测，所以请避免猜测。好的答案将包括一个证明，或者，如果没有，则包括一个令人信服的非正式论点。

这个问题的答案对那些为 OSGi 构建解析器的项目很有值(value)，包括 Eclipse Equinox 和 Apache Felix 开源项目，以及更广泛的 OSGi 社区。

Answer 1

是的。

edos paper采用的方法可以使引用的 Pascal 与 OSGi 一起使用。下面我将展示如何将任何 3-SAT 实例简化为 OSGi 包解析问题。该站点似乎不支持数学符号，因此我将使用程序员熟悉的符号代替。

这是我们试图减少的 3-SAT 问题的定义:

首先将 A 定义为一组命题原子及其否定 A = {a(1), … ,a(k),na(1), … ,na(k)}。在更简单的语言中，每个 a(i) 都是一个 bool 值，我们定义 na(i)=!a(i)

然后 3-SAT 实例 S 具有以下形式:S = C(1) & ... & C(n)

其中 C(i) = L(i,1) | L(i,2) | L(i,3) 并且每个 L(i,j) 都是 A 的成员

解决特定的 3-SAT 实例涉及为 A 中的每个 a(i) 找到一组值，真或假，以便 S 评估为真。

现在让我们定义将用于构建等效解析问题的包。在下文中，所有包和包版本均为 0，导入版本范围不受限制，除非另有说明。

整个表达式 S 将由 Bundle BS

表示

每个子句 C(i) 将由一个包 BC(i)

表示

每个原子 a(j) 将由束 BA(j) 版本 1

表示

每个否定原子 na(j) 将由束 BA(j) 版本 2

表示

现在是约束，从原子开始:

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) 的使用指令

公元前(一)
- 导出 PC(i)
-import PM(i) 并将其添加到 PC(i) 的使用指令中
-对于子句 C(i) 中的每个原子 a(j) 可选择导入 PA(j) 版本 [1,1] 并将 PA(j) 添加到 PC(i) 导出的使用指令
-对于子句 C(i) 中的每个原子 na(j) 可选择导入 PA(j) 版本 [2,2] 并将 PA(j) 添加到 PC(i) 导出的使用指令

学士
- 没有导出
-对于每个条款 C(i) 导入 PC(i)
-对于 A 中的每个原子 a(j) 导入 PA(j) [1,2]

几句话解释:

子句之间的 AND 关系是通过让 BS 从每个 BC(i) 导入一个包 PC(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。此外，使用约束确保子句束 BC(i) 导入的任何 PA(j) 作为对 BS 类空间的隐含约束，因此如果 PA(j) 的两个版本都出现在其隐含的约束。所以只有一个版本的 BA(j) 可以出现在解决方案中。

顺便说一下，有一种更简单的方法来实现 NOT 关系 - 只需将 singleton:=true 指令添加到每个 BA(j)。我没有这样做，因为单例指令很少使用，所以这看起来像是作弊。我只是提到它，因为在实践中，我所知道的任何 OSGi 框架都没有在面对可选导入时正确使用基于包的约束，所以如果您要使用这种方法实际创建包，那么测试它们可能会令人沮丧。

其他备注:

也可以减少不使用可选导入的 3-SAT，尽管这会更长。它基本上涉及一个额外的包层来模拟使用版本的可选性。减少1-in-3 SAT就相当于减少到3-SAT，看起来更简单，虽然我还没有通过。

除了使用 singleton:=true 的证明之外，我所知道的所有证明都依赖于使用约束的传递性。请注意， singleton:=true 和传递使用都是非局部约束。

上面的证明实际上表明 OSGi 解析问题是 NP-Complete 或更糟的。为了证明它并没有更糟，我们需要证明该问题的任何解决方案都可以在多项式时间内得到验证。大多数需要检查的东西都是本地的，例如查看每个非可选导入并检查它是否连接到兼容的导出。验证这些是 O(num-local-constraints)。基于 singleton:=true 的约束需要查看所有单例包并检查没有两个包具有相同的包符号名称。检查次数小于 num-bundlesnum-bundles。最复杂的部分是检查是否满足使用约束。对于每个包，这涉及遍历使用图以收集所有约束，然后检查这些约束是否与包的导入没有冲突。任何合理的步行算法都会在遇到之前见过的连线或使用关系时返回，因此步行的最大步数为(num-wires-in-framework + num-uses-in framework)。检查导线或使用关系之前没有走过的最大成本小于此日志。一旦收集了受约束的包，每个包的一致性检查的成本就会低于 num-imports-in-bundlenum-exports-in-framework。这里的一切都是多项式或更好的。