sat - 寻找路径：SAT求解

Question

我们给定一个 n*m 网格，它在各个点都有障碍物，即机器人的起始和结束位置。任务是找到一条从头到尾的无碰撞路径。这个问题将被建模为 SAT 问题。

请指导我在这种情况下应该做什么以获得最佳解决方案。

Answer 1

我会假设最优意味着最短。使用我在这里描述的方法，您可以执行第一步：

1. 定义一个网格
2. 制定可满足性任务

在这个阶段，求解器会返回满足所有约束的随机路径。要记住的重要一点 - 您可以定义达到目标所需的步骤数 k ！因此，您只需从k = 0开始。是否有可能通过 0 个动作达到目标？可能不会，直到代理已经达到目标。然后只增加k = 1。现在有可能吗？如果没有，增加更多！如何实施？只需将高于某个限制的所有k设置为 False 并在每次迭代时增加此限制。

如果您知道上限，则可以使用二进制搜索来找到可能的最短路径，这可能会更有效。

如果您关心路径的其他属性，则可以使用伪布尔约束。通过利用这种方法，您可以最大限度地减少例如右转的次数。为所有可能的右转创建一个布尔计数器，并通过假设限制可用转数。