SPPsolver: a SAT-based algorithm for solving any stable paths problem correctly

Abstract The Stable Paths Problem (SPP) is a widely adopted model for analyzing the convergence of Border Gateway Protocol (BGP). Solving SPP correctly is of great significance for determining BGP convergence. Existing studies have proposed some SPP solving algorithms that can only solve a part of SPP instances and have limited capabilities. To fill this gap, in this paper we transform SPP into Boolean Satisfiability Problem (SAT) and propose a new SPP solving algorithm called SPPsolver , which can support the solution of any SPP instance. We use Binary Decision Diagrams (BDD) to encode and calculate the SAT formula and apply two optimization methods to accelerate SPPsolver . We use real-world datasets to perform experiments and compare with state-of-the-art algorithms, the results demonstrate the superiority and efficiency of SPPsolver .