2010-01-18 13 views
24

El problema de resolución se describe en el capítulo de modularidad de OSGi R4 core specification. Es un problema de satisfacción de restricciones y ciertamente un problema difícil de resolver de manera eficiente, es decir, no mediante la fuerza bruta. Las principales complicaciones son la restricción de uso, que tiene efectos no locales, y la libertad de eliminar importaciones opcionales para obtener una resolución exitosa.¿El problema de resolución está en OSGi NP-Complete?

NP-Integridad se trata con elsewhere en StackOverflow.

Ya ha habido mucha especulación sobre la respuesta a esta pregunta, así que evite las especulaciones. Las buenas respuestas incluirán una prueba o, en su defecto, un argumento informal convincente.

La respuesta a esta pregunta será valiosa para aquellos proyectos que crean resolvedores para OSGi, incluidos los proyectos de código abierto Eclipse Equinox y Apache Felix, así como para la comunidad OSGi más amplia.

+0

¡Derecho! Creo que alguien con los antecedentes adecuados podría responder la pregunta sin demasiado dolor. El problema principal es encontrar a esa persona. –

+0

Consulte también [prueba] (http://wiki.apidesign.org/wiki/LibraryReExportIsNPComplete) que un problema de resolución similar es NP-Complete. –

Respuesta

26

Sí.

El enfoque adoptado por edos paper Pascal citado se puede hacer para que funcione con OSGi. A continuación, mostraré cómo reducir cualquier instancia 3-SAT a un problema de resolución de paquete OSGi. Este sitio no parece ser compatible con la notación matemática, por lo que usaré el tipo de notación que es familiar para los programadores.

Aquí es una definición del problema 3-SAT que estamos tratando de reducir:

En primer lugar definir un ser un conjunto de átomos de proposiciones y sus negaciones A = {a (1), ..., (k), na (1), ..., na (k)}. En un lenguaje más sencillo, cada una (i) es un valor lógico y definimos na (i) = a (i)

Luego 3-SAT instancias S tienen la forma: S = C (1) & ... & C (n)

donde C (i) = L (i, 1) | L (i, 2) | L (i, 3) y cada L (i, j) es miembro de A

Resolver una instancia particular de 3-SAT implica encontrar un conjunto de valores, verdadero o falso para cada a (i) en A, tal que S evalúa como verdadero

Ahora definamos los paquetes que se usarán para construir un problema de resolución equivalente. A continuación, todas las versiones de paquetes y paquetes son 0 e importan rangos de versiones sin restricciones, excepto donde se especifique.

  • Toda la expresión S estarán representados por Bundle BS
  • Cada cláusula C (i) estará representada por un BC haz (i)
  • Cada átomo a (j) será representado por un haz BA (j) versión 1
  • Cada átomo negada na (j) será representada por un BA haz (j) versión 2

ya por las restricciones, a partir de los átomos:

BA (j) versión 1
-paquete de exportación PA (j) versión 1
-para cada cláusula C (i) que contiene átomo a (j) exportación PM (i) y agregue PA (j) a PM (i) 's usos Directiva sobre

BA (j) versión 2
paquete -export PA (j) versión 2
-para cada cláusula C (i) que contiene un átomo negada na (j) PM exportación (i) y añadir usos PA (j) de PM (i) 's Directiva sobre

aC (i)
-export PC (i)
-import PM (i) y añadirlo a los usos d irective de PC (i)
-para cada átomo a (j) en la cláusula C (i) opcionalmente importe la versión PA (j) [1,1] y agregue PA (j) a la directiva de usos de la PC (i) exportación
-para cada átomo na (j) en la cláusula C (i) opcionalmente de importación PA (j) versión [2,2] y añadir PA (j) a la directiva usos de la PC (i) la exportación

BS
exportaciones -no
-para cada cláusula C (i) PC ​​de la importación (i)
-para cada átomo a (j) en una importación de PA (j) [1,2]

Unas pocas palabras de explicación:

Las relaciones AND entre las cláusulas se implementan al importar BS de cada BC (i) un paquete PC (i) que solo se exporta mediante este paquete.

La relación OR funciona porque BC (i) importa el paquete PM (i) que solo se exporta mediante los paquetes que representan a sus miembros, por lo que debe estar presente al menos uno de ellos y porque opcionalmente importa algunos PA (j) la versión x de cada paquete que representa un miembro, un paquete exclusivo para ese paquete.

La relación NOT entre BA (j) versión 1 y BA (j) versión 2 es impuesta por utiliza restricciones. BS importa cada paquete PA (j) sin restricciones de versión, por lo que debe importar PA (j) versión 1 o PA (j) versión 2 para cada j. Además, las restricciones de uso aseguran que cualquier PA (j) importado por un paquete de cláusulas BC (i) actúa como una restricción implícita en el espacio de clase de BS, por lo que BS no puede resolverse si ambas versiones de PA (j) aparecen en su implícita restricciones Entonces, solo una versión de BA (j) puede estar en la solución.

Por cierto, hay una manera mucho más fácil de implementar la relación NOT: simplemente agregue la directiva singleton: = true a cada BA (j). No lo he hecho así porque rara vez se usa la directiva singleton, así que parece una trampa.Solo lo menciono porque, en la práctica, ningún framework OSGi que conozca implementa usa según las restricciones del paquete de forma adecuada frente a las importaciones opcionales, por lo que si realmente crease paquetes usando este método, probarlos podría ser una experiencia frustrante .

Otras observaciones:

Una reducción de 3-SAT que no utiliza las importaciones opcionales en también es posible, aunque esto es más largo. Básicamente, implica una capa adicional de paquetes para simular la opción de usar versiones. Una reducción de 1-en-3 SAT es equivalente a una reducción a 3-SAT y parece más simple, aunque no lo he superado.

Además de las pruebas que usan singleton: = verdadero, todas las pruebas que conozco dependen de la transitividad de las restricciones de uso. Tenga en cuenta que los usos singleton: = true y transitive son restricciones no locales.

La prueba anterior muestra que el problema de resolución de OSGi es NP-Complete o peor. Para demostrar que no es peor, tenemos que demostrar que cualquier solución al problema se puede verificar en tiempo polinomial. La mayoría de las cosas que deben verificarse son locales, p. mirando cada importación no opcional y comprobando que está conectada a una exportación compatible. Verificando esto es O (num-local-constraints). Restricciones basadas en singleton: = verdadera necesidad de mirar todos los paquetes simples y comprobar que no hay dos que tengan el mismo nombre simbólico de paquete. El número de comprobaciones es menor que num-bundles num-bundles. La parte más complicada es verificar que las restricciones de uso estén satisfechas. Para cada paquete esto implica recorrer el gráfico de usos para reunir todas las restricciones y luego verificar que ninguno de estos entre en conflicto con las importaciones del paquete. Cualquier algoritmo de caminata razonable retrocedería cada vez que encontrara una relación de cable o de uso que haya visto antes, por lo que el número máximo de pasos en la caminata es (marco num-hilos-en-marco + num-usos-en). El costo máximo de verificar que un cable o una relación de uso no se haya andado antes es menor que el registro de esto. Una vez que se han reunido los paquetes restringidos, el costo de la verificación de coherencia para cada paquete es menor que num-imports-in-bundle num-exports-in-framework. Todo aquí es un polinomio o mejor.

+0

cosas geniales. Tenemos que demostrar que una solución de resolución se puede verificar en tiempo polinomial; de lo contrario, el problema de resolución podría ser> peor

+0

Steve Powell y yo pasamos por esta prueba y nos parece correcto (suponiendo que el problema de resolución no sea peor que NP). ¡Bien hecho! Sin embargo, tenga en cuenta que la prueba se basa en que el resolver descarta las restricciones de uso para los paquetes importados opcionalmente que no están cableados. Es cuestionable si el resolvedor debería hacer esto, pero es ciertamente lo que hace actualmente el resolutor Equinox. –

+0

Steve - Punto justo.Estaba tomando la verificación de tiempo polinomial como un hecho, pero en realidad no lo compré. Creo que la única parte no obvia es la verificación de las restricciones de uso para cada paquete al recorrer el árbol de importación-> exportación-> usos-> importación, etc. A primera vista, parece que podría ser exponencial, pero el número finito de cables de importación y exportación y el uso de relaciones limita la duración de la caminata, lo que hace que la comprobación sea polinómica. Cuando tenga algo de tiempo, agregaré una explicación más detallada de esto a mi respuesta. –

2

Este documento proporciona una demostración: http://www.cse.ucsd.edu/~rjhala/papers/opium.html

+0

Sí, se ha hablado de utilizar un solucionador de SAT para implementar una resolución de OSGi, pero eso no ayuda a responder la pregunta de NP-Completitud. Por ejemplo, es posible resolver problemas triviales de restricción usando un solucionador SAT, pero eso no implica que esos problemas sean NP-completos. También sabemos que algunos problemas NP-Complete pueden ser resueltos por un solucionador SAT, por lo que la existencia de un solucionador OSGi SAT no implicaría que el problema de resolución OSGi no sea NP-Complete. Buen intento sin embargo. ;-) –

0

De memoria pensé que este documento contenía la demostración, lo siento por no comprobar que antes. Aquí hay otro enlace que quería copiar que estoy seguro proporciona una demostración en la página 48: http://www.edos-project.org/bin/download/Main/Deliverables/edos%2Dwp2d1.pdf

+0

Ok. Ese documento demuestra que la instalación del paquete Debian es NP-hard y, por lo tanto, NP-complete. Desafortunadamente, la demostración depende del hecho de que cualquier instancia 3SAT se puede reducir en tiempo polinomial a un problema de instalación del paquete Debian. Esto se muestra esencialmente codificando las operaciones booleanas AND, OR y NOT en términos de restricciones de instalación del paquete. Intenté este enfoque en el pasado, pero no pude codificar O o NO como restricciones de resolución OSGi. Entonces, a menos que podamos reducir la resolución OSGi a la instalación del paquete Debian en tiempo polinomial, no tenemos una demostración. –