.png){kind=icon}
.png){kind=icon}
Return
SPPsolver: a SAT-based algorithm for solving any stable paths problem correctly
.png){kind=icon}
OA
AI
DOI：10.1186/s42400-025-00421-1.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
SPP
BGP
SAT
Formal methods
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
C
IF:
3.7
Papers:
570
Citations:
1.0K