本文介绍了基于SAT的运动计划的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

              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 处,它必须位于四个相邻节点之一
  3. 当且仅当步骤 k 中的代理位于目标节点时,
  4. SAT公式满足

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

此示例仅是一个示例.人们使用 satplan STRIPS 在现实生活中.

EDIT1对于无冲突的路径,您应该添加其他约束:

  1. 如果节点包含障碍物,则业务代表将无法访问它.例如.相应的布尔变量在任何时候都不能为 True ,例如总是 False
  2. 如果我们谈论的是多主体系统,则两个布尔变量(分别对应于同一节点上同一时间步长的两个主体)不能同时 True :

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)
              SAT BASED MOTION PLANNING ALGORITHM

A simple motion planning problem can be remodelled as a SAT solving problem. Can anyone explain how is this possible?

In this problem, we have to find a collision free path from start to end location.

解决方案

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.

EDIT1In 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的运动计划的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

08-04 04:27
查看更多