找到一条路径：SAT求解

Question

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

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

Answer 1

我会假设最佳意味着最短。使用我所描述的方法here你可以做第一个步骤：

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

在这个阶段，求解器返回到您随机路径满足所有限制。一个重要的事情要记住 - 你可以定义步数k这是达到目标所必需的！所以你只需从开始k = 0。有0个动作可以达到目标吗？可能不是，直到一个经纪人已经到达目标。然后仅增加k = 1。现在可能吗？如果没有，增加更多！如何实现它？只需将所有k的值设置为False的一定限制以上，并且每次迭代都会增加此限制。

如果您知道上限，可以使用二分查找找到最短路径，这可能会更有效。

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