Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks

We propose a novel method for combined Routing and Wave-length Assignment (RWA) in optical networks by reformulation to an equivalent Pseudo-Boolean Satisfiability (PB-SAT) problem. We introduce edge observability variables to represent whether an edge is on the optimal route, combined with either a simple or a hierarchical SAT encoding to select a wavelength for that edge only when the edge is on the route. This translation exponentially reduces the size of the solution space, making it independent of the number of wavelengths per link. We present experimental results for routing instances with up to 3,000 nodes, 15,000 edges, and 2,048 wavelengths per edge, and achieve at least 8 orders of magnitude speedup relative to a previous PB-SAT encoding by Aloul et al., such that the speedup is increasing with the number of nodes and edges in the network, and the number of wavelengths per edge. A portfolio of 4 parallel strategies, each based on the new approach and a different hierarchical encoding, resulted in additional speedup of up to 6 times, and reduced the variability of the run times for large networks.