OSGi NP-Complete中的分辨率问题是什么？

Question

解决问题的方法在OSGi R4 核心规范的模块化章节中有所描述.这是一个约束满足问题,当然也是一个有效解决的挑战性问题,即不是蛮力.主要的复杂因素是使用约束,它具有非局部效应,并且可以自由地删除可选导入以获得成功的解决方案.

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

关于这个问题的答案已经有很多猜测,所以请避免猜测.好的答案将包括一个证据,或者,如果没有这个,那就是一个引人注目的非正式论

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

Answer 1

是.

引用的Edos文件所采用的方法可以与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中的每个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
- 每个条款C(i)包含原子a(j)导出PM(i)并将PA(j)添加到PM(i)的使用指令

BA(j)第2
版
- 出口包PA(j)第2版- 每个条款C(i)包含否定原子na(j)输出PM(i)并将PA(j)添加到PM(i)的使用指令

BC(i)
-export 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
-no
export -for each clause C(i)import PC(i)
-for each atom a(j)in a import PA(j)[1,2]

几句解释:

子句之间的AND关系是通过从每个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.此外,使用约束确保由子句束BC(i)导入的任何PA(j)充当BS的类空间的隐含约束,因此如果PA(j)的两个版本出现在其隐含中,则BS无法被解析.限制.因此,解决方案中只能有一个版本的BA(j).

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

其他评论:

减少不使用可选进口的3-SAT也是可能的,尽管这会更长.它基本上涉及额外的一层bundle来模拟使用版本的可选性.减少1-in-3 SAT相当于减少到3-SAT并且看起来更简单,尽管我还没有逐步完成它.

除了使用singleton:= true的证明之外,我所知道的所有证明都取决于使用约束的传递性.请注意,singleton:= true和transitive使用都是非本地约束.

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