SMT-Based Aircraft Conflict Detection and Resolution

The integration of Unmanned Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) operations will create the need to develop robust, efficient, and verifiable tools and techniques for UAS Traffic Management (UTM). In this paper, we present a novel approach for strategic detection and resolution of airborne conflicts using Satisfiability Modulo Theories (SMT) solvers. Our approach takes a flight plan for an ownship, a set of immutable flight plans for traffic aircraft, and a set of constraints, and then returns a flight plan for the ownship that satisfies all constraints and is also conflict free with respect to the traffic aircraft. The constraints can relate to operational, business, or other aspects which must be considered while setting up the conflict resolution task as a constraint satisfaction problem. We present simulations of our approach using a prototype implementation based on \(\textsf {dReal}\) , an SMT solver that is specialized for solving non-linear real function problems, showing promising results.