—Today, most routing problems are solved using Dijkstra’s shortest path algorithm. Many efficient implementations of Dijkstra’s algorithm exist and can handle large networks in short runtimes. Despite these advances, it is difficult to incorporate user-specific conditions on the solution when using Dijkstra’s algorithm. Such conditions can include forcing the path to go through a specific node, forcing the path to avoid a specific node, using any combination of inclusion/exclusion of nodes in the path, etc. In this paper, we propose a new approach to solving the shortest path problem using advanced Boolean satisfiability (SAT) techniques. SAT has been heavily researched in the last few years. Significant advances have been proposed and has lead to the development of powerful SAT solvers that can handle very large problems. SAT solvers use intelligent search algorithms that can traverse the search space and efficiently prune parts that contain no solutions. These solvers have re...
Fadi A. Aloul, Bashar Al Rawi, Mokhtar Aboelaze