Планирование движения на основе SAT

              SAT BASED MOTION PLANNING ALGORITHM

Простую задачу планирования движения можно преобразовать в задачу решения SAT. Кто-нибудь может объяснить, как это возможно?

В этой задаче мы должны найти путь без столкновений от начального до конечного местоположения.


motion-planning sat
person Jaskirat Singh    schedule 30.05.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Самый простой пример может выглядеть так.

Давайте представим двумерную сетку из N строк и M столбцов, движущийся агент A начинается в узле (x, y). Его цель T имеет координаты (x_i, y_j):

сетка

Чтобы добраться до цели, агент должен совершить несколько шагов - двигаться влево, вправо, вверх или вниз последовательно. Мы не знаем, сколько шагов ему нужно, поэтому мы должны сами ограничить это число. Допустим, мы ищем план, состоящий из K шагов. В этом случае мы должны добавить N*M*K логических переменных: N и M представляют собой координаты, K - время. Если переменная имеет значение True, то агент в настоящий момент находится в узле (x,y) в момент времени k.

Далее мы добавляем различные ограничения:

  1. Агент должен менять свою позицию на каждом шаге (на самом деле это необязательно)
  2. Если робот на шаге k находится в позиции (x,y), то на шаге k+1 он должен быть в одном из четырех соседних узлов
  3. Формула SAT выполняется тогда и только тогда, когда агент на шаге k находится в целевом узле.

Я не буду подробно обсуждать здесь реализацию ограничений, это не так сложно. Аналогичный подход можно использовать для многоагентного планирования.

Этот пример является просто иллюстрацией. Люди используют satplan и STRIPS в реальной жизни.

EDIT1 В случае пути без столкновений вы должны добавить дополнительные ограничения:

  1. Если узел содержит препятствие, агент не может его посетить. Например. соответствующие логические переменные не могут быть True на любом временном шаге, например. это всегда False
  2. Если мы говорим о многоагентной системе, то две логические переменные, соответствующие двум агентам, находящимся на одном и том же временном шаге в одном и том же узле, не могут быть True одновременно:

AND (agent1_x_y_t, agent2_x_y_t) <=> False

РЕДАКТИРОВАТЬ2

Как построить формулу, которая бы удовлетворяла. Перебрать все узлы и все временные метки, например. над каждой булевой переменной. Для каждой логической переменной добавьте ограничения (я буду использовать Python-подобный псевдокод):

 formula = []
 for x in range(N):
     for y in range(M):
         for t in range (K):
             current_var = all_vars[x][y][t]
             # obstacle
             if obstacle:
                 formula = AND (formula, NOT (current_var))

             # an agent should change his location each step
             prev_step = get_prev_step (x,y,t)
             change = NOT (AND (current_var, prev_step))
             formula = AND (formula, change)

             adjacent_nodes = get_adj (x,y, k+1)

             constr = AND (current_var, only_one_is_true (adjacent_nodes))
             formula = AND (formula, constr)
 satisfy (formula)
person CaptainTrunky    schedule 30.05.2017
comment
Я сожалею, что должен был явно упомянуть о проблеме. Можно ли каким-либо образом изменить ваше решение, чтобы удовлетворить ограничения? - person Jaskirat Singh; 30.05.2017
comment
@JaskiratSingh Вы можете добавить к этой задаче любые ограничения, которые хотите, я попытался представить основные ограничения и способ решения этой проблемы. - person CaptainTrunky; 30.05.2017
comment
Да, понял. Спасибо :) - person Jaskirat Singh; 30.05.2017