-1 
              SAT BASED MOTION PLANNING ALGORITHM

一个简单的运动规划问题可以改造成一个SAT 求解问题。谁能解释这怎么可能？

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

4

1 回答 1

0

最简单的示例可能如下所示。

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

网格

为了达到目标，智能体应该执行几个步骤 - 向左、向右、向上或向下移动。我们不知道它需要多少步，所以我们必须自己限制这个数字。假设我们正在寻找一个包含 K 个步骤的计划。在这种情况下，我们应该添加 N*M*K 布尔变量：N 和 M 代表坐标，K - 时间。如果变量为True，则代理当前在时间k位于节点 ( x , y ) 。

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

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

我不会在这里讨论约束的详细实现，这并不难。类似的方法可以用于多智能体规划。

这个例子只是一个例子。人们在现实生活中使用satplan和STRIPS 。

EDIT1 在无碰撞路径的情况下，您应该添加额外的约束：

  1. 如果节点包含障碍物，则代理无法访问它。例如，相应的布尔变量在任何时间步都不能为真，例如它总是假
  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)
于 2017-05-30T05:42:12.867 回答