Introduction to Automated Planning / Введение в автоматизированное планирование: Planning without observability by evaluation of QBF

Планирование без наблюдения по оценке QBF

Mark_Krass 05.01.14 в 21:09

В этом разделе мы расширим методы из раздела 3.5 для ненаблюдаемого планирования. Потому что

Mark_Krass 05.01.14 в 21:09

исходя из недетерминизма и нескольких начальных состояний один план может иметь несколько различных способов выполнения.

Mark_Krass 05.01.14 в 21:10

Получается, что логика высказываний не подходит для представления ненаблюдаемого планирования

Mark_Krass 05.01.14 в 21:10

а вместо него необходим язык количественных Булевых формул. Интуитивно понятно, что причина

Mark_Krass 05.01.14 в 21:11

этого в том, что нам приходится количественно оценивать нарастающее в геометрической прогрессии число вариантов выполнения плана: нам нужно выражение типа

Alex_ander 06.01.14 в 10:32

"существует план, такой что для всех вариантов его выполнения...", а [выразить это кратко средствами обычной логики суждений не предcтавляется возможным.]

Alex_ander 06.01.14 в 10:34

использование данной логики не возможно. Теоретическое обоснование, данное в разделе 4.5.4 показывает, что тестирование

Mark_Krass 05.01.14 в 21:13

существующих планов проблематично в случае отсутствия наблюдения даже когда выполнено ограничение плана

Mark_Krass 05.01.14 в 21:14

полиноминальной длины классом сложности ∑2 и он не содержится в NP как

Mark_Krass 05.01.14 в 21:15

соответствующая задача недетерминированного планирования. Это заставляет предположить,

Mark_Krass 05.01.14 в 21:15

ввиду общепринятых теоретических гипотез о сложности, что в рамках логики суждений

Alex_ander 06.01.14 в 10:47

эффективного способа постановки этой задачи не существует.

Alex_ander 06.01.14 в 10:47

В разделе 4.1.2 мы показали, как недетерминированные операторы могут быть переведены в формулы

Mark_Krass 05.01.14 в 21:16

логики высказываний. Целью этого перевода было использования формул в планировании BDD

Mark_Krass 05.01.14 в 21:16

алгоритмов для вычисления образов и прообразов множеств состояний. Для QBF

Mark_Krass 05.01.14 в 21:16

представления недетерминированных операторов мы должны иметь возможность определять количество

Mark_Krass 05.01.14 в 21:17

всех возможных успешных состояний производящих операторов, и не можем просто выразить это, используя

Mark_Krass 05.01.14 в 21:18

формулы из раздела 4.1.2, поэтому мы делаем новый перевод использующий для определения количества Булевы

Mark_Krass 05.01.14 в 21:18

формулы (смотри раздел 2.2.1)

Mark_Krass 05.01.14 в 21:18

Перевод недетерминированных операторов в логику высказываний

Mark_Krass 05.01.14 в 21:19

Для обработки недетерминизмов мы должны определить количество всех недетерминированных операторов

Mark_Krass 05.01.14 в 21:19

потому что в любом случае остальные операторы в плане должны приводить к целевому состоянию. Для достижения результата

Mark_Krass 05.01.14 в 21:19

при n недетерминированных альтернативах можно применить m = dlog2 ne
единообразно задаваемых

Alex_ander 07.01.14 в 20:07

количество вспомогательных переменных. Для оценки каждой переменной должен быть выбран один из альтернативных вариантов.

Mark_Krass 05.01.14 в 21:21

Поставим в соответствие каждому атомарному событию формулу, которая истинна тогда и только тогда, когда событие выполняется.

Mark_Krass 05.01.14 в 21:23

Это аналогично расширению понятия функции EPCl(e) в определении 3.3. Проблема расширения

Mark_Krass 05.01.14 в 21:23

недетерминизма состоит в следующем: если l принимает значение «истина», то вспомогательные переменные должны

Mark_Krass 05.01.14 в 21:24

иметь значения, соответствующие событиям, делающим l «истиной».

Mark_Krass 05.01.14 в 21:24

Условием выполнения l является выполнение события e в nEPCl(e, σ, t).

Mark_Krass 05.01.14 в 21:25

Целочисленная последовательность σ получает уникальные имена для вспомогательных переменных в nEPCl(e, σ, t), и

Mark_Krass 05.01.14 в 21:25

значение вспомогательной переменной t в формуле определяется когда будет вычислено e. Предполагается, что результат будет представлен

Mark_Krass 05.01.14 в 21:25

в нормальной форме I

Mark_Krass 05.01.14 в 21:26

nEPCl(e, _, t) = EPCl(e) ^ t если е детерминизировано

Mark_Krass 06.01.14 в 21:20

nEPCl(p1e1| • • • |pnen, _, t) = nEPCl(e1, _; 1, cn1(_) ^ t) _ • • • _ nEPCl(en, _; n, cnn(_) ^ t)

Mark_Krass 06.01.14 в 21:20

nEPCl(e1 ^ • • • ^ en, _, t) = nEPCl(e1, _; 1, t) _ • • • _ nEPCl(en, _; n, t)

Mark_Krass 06.01.14 в 21:20

Функция Cni (σ) строится по формуле для вычисления i-ого результата из n вариантов. Эта

Mark_Krass 05.01.14 в 21:26

формула обычно соединяет вспомогательные переменные
Amσ = {aσ,1, . . . , aσ, m}

Mark_Krass 05.01.14 в 21:26

соответствующих одной оценке Amσ. Здесь m= log2n. Когда n не является степенью двойки, последний

Mark_Krass 05.01.14 в 21:27

результат en соответствует более чем одной оценке Amσ. Определим:

Mark_Krass 05.01.14 в 21:27

dmi(_) =V({a_,j 2 Am_ |jth bit of i − 1 is 1}{¬a_,j |a_,j 2 Am_ , jth bit of i − 1 is 0}).

Mark_Krass 06.01.14 в 21:19

Когда i ∈ {1, . . . , n − 1} (и в этом особом случае i = n = 2m) мы определяем Cni (σ) как dm i(σ). Когда n=i мы определяем Cni (σ) как dm n(σ) ˅ • • • ˅ dm 2m(σ)

Mark_Krass 05.01.14 в 21:28

Отсюда события с e1 до en−1 соответствуют бинарной кодировке чисел от 0 до n-2 и en охватывает

Mark_Krass 05.01.14 в 23:16

все остальные оценки Amσ

Mark_Krass 05.01.14 в 23:16

Следующий фрейм аксиоматически выражает условия, при которых значение переменной а ∈ А может

Mark_Krass 05.01.14 в 23:17

может меняться от ложного к истинному и наоборот. Будем считать, что операторы O = {o1, . . . , on}

Mark_Krass 05.01.14 в 23:17

пронумерованы от 1 до n

Mark_Krass 05.01.14 в 23:17

(¬a ^ a0)!((o1 ^ nEPCa(e1, 1,>)) _ • • • _ (on ^ nEPCa(en, n,>)))

Mark_Krass 06.01.14 в 21:19

(a ^ ¬a0)!((o1 ^ nEPC¬a(e1, 1,>)) _ • • • _ (on ^ nEPC¬a(en, n,>)))

Mark_Krass 06.01.14 в 21:19

Для каждого оператора o = <z, e> ∈ O мы имеем формулы для описания значений переменных состояния

Mark_Krass 05.01.14 в 23:18