Solve the following exercise by means of a reduction to
SAT:
- Determine if two planes can fly simultaneously through a cave
filled with obstacles without crashing and, furthermore, crossing
at some point of the flight, i.e., such that the plane that started higher
ends lower than the other. The cave is a two-dimensional space discretized
in squares. It has height h and length l. Each square can either
be free or an obstacle. For instance, the cave
##########################·········
·······###·········#########·······
········#···············#########··
········#······###···········######
······#········#·#····###··········
·····###·······###····########·····
···######··························
###################################
has height 8 and length 35, obstacles being indicated with a #.
A plane occupies a square. At each unit of time, planes move forward
(one square to the right). At the same time, they can ascend (increasing
their height by one square), keep the same height, or descend (decreasing
their height by one square). We start with two planes, A and B, at the
beginning of the cave (in the first column of squares),
the plane A starting somewhere above plane B.
We want to
find how can they fly safely to the end of the cave (the last column), without
crashing against obstacles or against each other. Moreover, we want to
find a route in which the planes cross, i.e., such that the plane A
reaches the end of the cave somewhere below the plane B. For instance, given
the starting positions A and B, the paths marked with
a and b are a valid solution for the previous cave:
##########################
Aaa ### #########
aaaa # aaaaaaaa #########
bbba# a ### aaaaaaa ######
bb #baa # # ### aaaaa bb
Bb ###bbbbb ### ######## ab
###### bbbbbbbbbbbbbbbbbbbaaa
###################################
The input of the exercise and the output with the solution (when the input is
solvable) are as follows:
Note: this problem can be solved in asymptotic polynomial time without reducing to SAT.