Да.
Подход, использованный в edos paper Указанный Паскаль, может быть использован для работы с 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) в Aтакой, что S оценивается как true.
Теперь давайте определим пакеты, которые мы будем использовать для построения задачи эквивалентного разрешения.В дальнейшем все версии комплекта и пакета равны 0, а диапазоны версий импорта не ограничены, кроме случаев, где это указано.
- Все выражение S будет представлено Пакетом 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)
-экспорт PC (i))
-импортировать PM (i) и добавить его в директиву использования ПК (i)
-для каждого атома a (j) в пункте C (i) дополнительно импортировать версию PA (j) [1,1] и добавить PA (j) к директиве использования ПК (i) export
- для каждого атома na (j) в пункте C (i) opимпортировать PA (j) версию [2,2] и добавить PA (j) в директиву использования ПК (i) export
BS
- no export
- для каждого пункта C(i) импортировать ПК (i)
- для каждого атома a (j) в A импортировать PA (j) [1,2]
Несколько слов объяснения:
Отношения И между предложениями реализуются путем импорта БС из каждого BC (i) пакета ПК (i), который экспортируется только этим комплектом.
Отношение ИЛИ работает, потому что BC (i) импортирует пакет PM (i) который экспортируется только пакетами, представляющими его участников, поэтому должен присутствовать хотя бы один из них, и поскольку он может импортировать некоторую версию x PA (j) из каждого пакета, представляющего элемент, пакет, уникальный для этого пакета.
Отношение NOT между BA (j) версии 1 и BA (j) версии 2 обеспечивается с использованием ограничений .BS импортирует каждый пакет PA (j) без ограничений версии, поэтому она должна импортировать либо PA (j) версию 1, либо PA (j) версию 2 для каждого j.Кроме того, ограничения использования гарантируют, что любой PA (j), импортированный пакетом предложений BC (i), действует как подразумеваемое ограничение на пространство классов BS, поэтому BS не может быть разрешена, если обе версии PA (j) появляются в ее подразумеваемомограничения.Таким образом, в решении может быть только одна версия BA (j).
Между прочим, существует гораздо более простой способ реализации отношения NOT - просто добавьте директиву singleton: = true вкаждый BA (J).Я не делал это таким образом, потому что директива синглтона используется редко, так что это похоже на обман.Я упоминаю об этом только потому, что на практике ни одна из известных мне OSGi-сред, реализующих , правильно не использует ограничения пакетов на основе перед лицом необязательного импорта, поэтому, если вы действительно создадите пакеты с помощью этого метода, то их тестирование можетбыть разочаровывающим опытом.
Другие замечания:
Сокращение 3-SAT, которое не использует дополнительный импорт, также возможно, хотя это и дольше. В основном это включает в себя дополнительный слой пакетов для имитации опциональности с использованием версий. Сокращение 1-в-3 SAT эквивалентно сокращению до 3-SAT и выглядит проще, хотя я не прошел через него.
Помимо доказательств, которые используют singleton: = true, все известные мне доказательства зависят от транзитивности ограничений использования. Обратите внимание, что как singleton: = true, так и переходное использование являются нелокальными ограничениями.
Приведенное выше доказательство фактически показывает, что проблема разрешения OSGi является NP-Complete или хуже. Чтобы продемонстрировать, что это не хуже, мы должны показать, что любое решение проблемы может быть проверено за полиномиальное время. Большинство вещей, которые необходимо проверить, являются локальными, например, просматривая каждый необязательный импорт и проверяя, связан ли он с совместимым экспортом. Проверка это O (Num-локальные ограничения). Ограничения, основанные на singleton: = true, должны просмотреть все одноэлементные пакеты и убедиться, что никакие два не имеют одинаковое символическое имя пакета. Количество проверок меньше чем num-bundles num-bundles. Самая сложная часть - проверка выполнения ограничений использования. Для каждого пакета это включает в себя обход графика использования для сбора всех ограничений и проверку того, что ни один из них не конфликтует с импортом пакета. Любой разумный алгоритм ходьбы будет возвращаться назад всякий раз, когда он сталкивается с проводом или использует отношения, которые он видел ранее, поэтому максимальное количество шагов в прогулке равно (num-wire-in-framework + num-использовании-in framework). Максимальная стоимость проверки того, что отношение проводов или использования не было пройдено ранее, меньше, чем лог этого. Как только ограниченные пакеты собраны, стоимость проверки согласованности для каждого пакета становится меньше, чем num-import-in-bundle num-exports-in-framework. Здесь все многочлен или лучше.