OSGi NP中的解决问题

分辨率问题在OSGi R4内核规范的模块化章节中有描述。 这是一个约束满足问题,当然也是一个有效解决的具有挑战性的问题,即不是通过暴力。 主要的复杂情况是使用约束,它具有非局部效应,并且可以自由放弃可选导入以获得成功的解决方案。

NP-Completeness在StackOverflow的其他地方处理。

关于这个问题的答案已经有很多猜测,所以请避免猜测。 好的答案将包括一个证明,否则就是一个引人注目的非正式论点。

对于那些构建OSGi解析器的项目,包括Eclipse Equinox和Apache Felix开源项目以及更广泛的OSGi社区,这个问题的答案将非常有价值。


是。

所引用的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,3)和每个L(i,j)是A的成员

解决一个特定的3-SAT实例需要找到一组值,对于A中的每一个(i)来说都是true或false,这样S的计算结果为true。

现在让我们定义我们将用来构造等效分辨率问题的包。 以下所有软件包和软件包版本均为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)的使用指令

    BC(ⅰ)
    - 出口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)导出

    BS
    - 不出口
    - 对于每个条款C(i)进口PC(i)
    对于A进口PA(j)中的每个原子a(j)[1,2]

    几句解释:

    条款之间的AND关系通过从每个BC导入BS(i)仅由该捆绑包导出的PC(i)包来实现。

    因为BC(i)导入只由代表其成员的包导出的包(PM)(i),所以它们中的至少一个必须存在,并且因为它可选地从每个包中导入一些PA(j)版本x代表成员的捆绑包,该捆绑包唯一的包。

    BA(j)版本1和BA(j)版本2之间的非关系由使用约束强制执行。 BS在没有版本限制的情况下导入每个软件包PA(j),因此它必须为每个j导入PA(j)版本1或PA(j)版本2。 另外,使用约束确保由子句包BC(i)导入的任何PA(j)作为BS的类空间的隐含约束,因此如果PA(j)的两个版本都出现在它的隐含中,则不能解决BS限制。 所以只有一个版本的BA(j)可以在解决方案中。

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

    其他评论:

    减少3-SAT也不可能使用可选的进口,尽管这个时间更长。 它基本上涉及一个额外的捆绑层来模拟使用版本的可选性。 减少1比3的SAT相当于减少到3-SAT,并且看起来更简单,虽然我还没有经过它。

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

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


    本文提供了一个演示:http://www.cse.ucsd.edu/~rjhala/papers/opium.html


    从记忆中我认为这篇论文包含了演示,对不起之前没有检查过。 这里是我想复制的其他链接,我确定在第48页上提供了一个演示:http://www.edos-project.org/bin/download/Main/Deliverables/edos%2Dwp2d1.pdf

    链接地址: http://www.djcxy.com/p/39977.html

    上一篇: Is the resolution problem in OSGi NP

    下一篇: Polynomial time algorithm for a NP