satmotion-planning

Finding a path: SAT solving


We are given an n*m grid, which has obstacles at various points,the starting and ending location of the bot. The task is to find a collision free path from start to end. This problem is to be modelled as a SAT problem.

Please guide me on what should be done in this case to get an optimal solution.


Solution

  • I would assume that optimal means the shortest. Using the approach that I've described here you can do first steps:

    1. define a grid
    2. formulate a satisfiability task

    At this stage, a solver returns to you random path that satisfies all constraints. An important thing to remember - you can define number of steps k which are required to reach a goal! So you just start with k = 0. Is it possible to reach the goal with 0 actions? Probably, not, until an agent is at the goal already. Then just increment k = 1. Is it possible now? If not, increment more! How to implement it? Just set all k's above a certain limit to False and increment this limit each iteration.

    If you know upper limits, you can use binary search to find the shortest possible path, which could be more efficient.

    If you care for other properties of a path, you can use pseudo-boolean constraints. By leveraging this approach, you can minimize, for example, a number of right turns. Create a Boolean counter for all possible right turns and limit number of available turns via assumptions.