Abstract—Today, most routing problems are solved usingDijkstra’s shortest path algorithm. Many efficient implementationsof Dijkstra’s algorithm exist and can handle large networksin short runtimes. Despite these advances, it is difficult toincorporate user-specific conditions on the solution when usingDijkstra’s algorithm. Such conditions can include forcing thepath to go through a specific node, forcing the path to avoid aspecific node, using any combination of inclusion/exclusion ofnodes in the path, etc. In this paper, we propose a new approachto solving the shortest path problem using advanced Booleansatisfiability (SAT) techniques. SAT has been heavily researchedin the last few years. Significant advances have beenproposed and has lead to the development of powerful SATsolvers that can handle very large problems. SAT solvers use intelligentsearch algorithms that can traverse the search spaceand efficiently prune parts that contain no solutions. Thesesolvers have recently been used to solve many problems in Engineeringand Computer Science. In this paper, we show how toformulate the shortest path problem in non-optical networks asa SAT problem. We also show how to use SAT in finding routingand wavelength assignments in optical networks. Our approachis verified on various network topologies. The resultsare promising and indicate that using the proposed approachcan improve on previous techniques.

Index Terms—Networks, Boolean Satisfiability, BacktrackSearch, Optimization, Routing and Wavelength Assignments.

Cite: Fadi A. Aloul, Bashar Al Rawi, and Mokhtar Aboelaze, "Routing in Optical and Non-Optical Networks using Boolean Satisfiability," Journal of Communications, vol. 2, no. 4, pp. 49-56, 2007.