基于SAT的运动计划 [英] SAT based motion planning

问题描述

              SAT BASED MOTION PLANNING ALGORITHM

一个简单的运动计划问题可以重构为 SAT解决问题.谁能解释这怎么可能?

在这个问题中，我们必须找到从起点到终点的无碰撞路径.

解决方案

最简单的示例如下所示.

让我们介绍N行和M列的2D网格，移动代理A从节点(x，y)开始.他的目标T的坐标为(x_i，y_j):

要达到目标，座席应执行几个步骤-因此向左，向右，向上或向下移动.我们不知道它需要多少步骤，因此我们必须自己限制此数目.假设我们正在寻找一个由K个步骤组成的计划.在这种情况下，我们应该添加N * M * K个布尔变量:N和M代表坐标，K-时间.如果变量为 True ，则代理当前位于时间 k 处的节点( x ， y )./p>

接下来，我们添加各种约束:

1. 座席必须在每个步骤中更改其位置(实际上这是可选的)
2. 如果机器人在步骤 k 处的位置(x，y)，则在步骤 k + 1 处，它必须位于四个相邻节点之一
当且仅当步骤 k 中的代理位于目标节点时，
3. SAT公式满足

在这里我将不讨论约束的详细实现，这并不困难.类似的方法可以用于多主体规划.

此示例仅是一个示例.人们使用 satplan 和 解决方案

The simplest example could look like this.

Let's introduce 2D grid of N rows and M columns, a moving agent A starts at a node (x,y). His target T has coordinates (x_i, y_j):

To reach a target the agent should perform several steps - move left, right, up or down consequently. We don't know how many steps it needs, so we have to limit this number ourselves. Let's say, we are searching for a plan that consists of K steps. In this case, we should add N*M*K boolean variables: N and M represent coordinates, K - time. If a variable is True then the agent currently at a node (x,y) at time k.

Next, we add various constraints:

1. The agent must change his position at each step (this is optional, actually)
2. If robot at step k is at a position (x,y), then at step k+1 it must be at one of four adjacent nodes
3. SAT formula is satisfied if and only if the agent at step k is at the target node

I'll not discuss a detailed implementation of the constraints here, it's not that difficult. The similar approach could be used for multiagent planning.

This example is just an illustration. People use satplan and STRIPS in real life.

EDIT1 In the case of a collision-free path you should add additional constraints:

1. If a node contains an obstacle, an agent can't visit it. E.g. corresponding boolean variables can't be True at any timestep e.g. it's always False
2. If we are talking about a multiagent system, then two boolean variables, corresponding to two agents being at same timestep at the same node, can't be True simultaneously:

AND (agent1_x_y_t, agent2_x_y_t) <=> False

EDIT2

How to build a formula that would be satisfied. Iterate over all nodes and all timestamps, e.g. over each Boolean variable. For each Boolean variable add constraints (I'll use Python-like pseudocode):

 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)

这篇关于基于SAT的运动计划的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！