| CPC G08G 5/0034 (2013.01) [G08G 5/0043 (2013.01); G08G 5/006 (2013.01); G08G 5/0069 (2013.01); G08G 5/045 (2013.01)] | 18 Claims |

|
1. A method for generating verifiable conflict-free flight plans for aircraft comprising: receiving, by a server computer from a user device, a set of air traffic flight plans for
an airspace comprising elements and at least two of aerodynamic constraint data, business constraint data and operational constraint data for an aircraft;
generating, by the server computer utilizing a first constraint satisfaction solver, a plurality of candidate flight plans for the aircraft based on the at least two of the aerodynamic constraint data, the business constraint data and the operational constraint data;
checking, by the server computer utilizing a second constraint satisfaction solver as each candidate flight plan is generated, for conflicts with the elements of the air traffic flight plans for the airspace, the second constraint satisfaction solver comprises a Satisfiability Modulo Theories (SMT) solver, the SMT solver being capable of solving a non-boolean constraint; and
providing, by the server computer using the second constraint satisfaction solver, at least one verifiable conflict-free flight plan for the aircraft from the plurality of candidate flight plans when a candidate flight plan is conflict-free from all of the elements of the set of air traffic flight plans.
|