基于 SAT 的运动规划

Question

              SAT BASED MOTION PLANNING ALGORITHM

一个简单的运动规划问题 可以重新建模为SAT 求解问题。谁能解释这怎么可能？

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

Answer 1

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

让我们介绍一下N行M列的二维网格，一个移动代理A从一个节点(x,y)开始。他的目标T坐标为(x_i,y_j):

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

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

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

我不会在这里讨论约束的详细实现，它并不难。类似的方法可用于 multiagent planning.

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

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

如果节点包含障碍物，则代理无法访问它。例如。相应的布尔变量在任何时间步都不能是 True，例如它总是 False
如果我们谈论的是多智能体系统，那么两个布尔变量，对应于在同一节点的同一时间步长的两个智能体，不能同时为 True：

AND (agent1_x_y_t, agent2_x_y_t) <=> False

编辑2

如何建立一个令人满意的公式。遍历所有节点和所有时间戳，例如在每个布尔变量上。为每个布尔变量添加约束（我将使用 Python-like 伪代码）：

 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 的运动规划

SAT based motion planning

sat

motion-planning