寻找路径：SAT求解

Question

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

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

Answer 1

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

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

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

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

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