Identifying the shortest path in large networks using Boolean satisfiability

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 recently been used to solve many problems in Engineering and Computer Science. In this paper, we show how to formulate the shortest path problem as a SAT problem. Our approach is verified on various network topologies. The results are promising and indicate that using the proposed approach can improve on previous techniques.