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

Question

              SAT BASED MOTION PLANNING ALGORITHM

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

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

Answer 1

Простейший пример может выглядеть следующим образом.

Давайте введем 2D сетку из 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 в реальной жизни.

РЕДАКТИРОВАТЬ1 В случае пути без столкновений вы должны добавить дополнительные ограничения:

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

AND (agent1_x_y_t, agent2_x_y_t) <=> False

EDIT2

Как построить формулу, которая будет удовлетворена. Выполните итерацию по всем узлам и всем временным меткам, например, по каждой логической переменной. Для каждой логической переменной добавьте ограничения (я буду использовать 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)