Page 447 - AWSAR 2.0

the number of charging stations along with their locations. This approach is guaranteed to give a solution. However, as it needs to check the original huge set of constraints every time, it is not at all scalable.
This is important that when the constraint solver is unable to satisfy all the constraints, that is, the set of constraints is unsatisfiable; it gives an unsatisfiable-core (in short, unsat core). An unsat core is a smaller subset of constraints that actually could not be satisfied (other constraints are satisfiable). In our algorithms, we use this unsat core to find a more specific and precise subset of constraints towards the cause of unsatisfiability. Please note that a unsat core is much smaller in size compared with the original set of constraints.
In our novel approach, whenever the original set of constraints is unsatisfiable, we extract the unsat core and then check the satisfiability of the unsat core (and not the original huge set of constraints)
for the next higher test value.
If it still does not satisfy, check
with the next higher test value
and so on. Thus, when the
unsat core becomes satisfiable,
it means the previously
unsatisfiable set of constraints
is satisfiable now, and we get a
model. Now, we need to verify if
this model satisfies the original
set of constraints. It may or
may not satisfy. If the model
satisfies the original set, we are
done. Otherwise, it implies that
the model does not fit well with
the original set of constraints.
Therefore, we go for the next
higher value and do similar
checking again with the original set. It goes on iteratively until we get a model satisfying the original set of constraints.
In every iteration, instead of checking
Mr. Tanmoy Kundu || 423
with the original mammoth state space, we find a much smaller state space (unsat core) and check its satisfiability. Then, it intelligently checks the usability of the solution in the perspective of the original problem. This approach guarantees the scalability of our methods. Our approach also guarantees an optimal solution to the problem.
In our experiments, we used Z3 SMT
solver from Microsoft research as the backend constraint solver. We did our experiments with three different types of robots – Turtlebot, Quadcopter and Dubins car; in three different types of workspaces such as warehouse, artificial floor and maze; and two different dimensions of the workspace. In almost all the cases, our algorithms found optimal solutions. Most importantly, our approach turns out to be much more scalable compared with the naive solution. The experiment shows that both our algorithms run 30%–85% faster compared with their naive counterparts. The Fig. shows an example of charging station placement using our algorithm. We applied problem variant-1 to find out the minimum number of charging stations for different types of robots.
Two variants of the charging station placement problem are proposed. The first variant assumes a power threshold to be given; we find out a minimum number of charging stations and their locations. The second variant considers the number of charging stations to be given, and we find out the value of the minimum power threshold and charging station locations.