Scholarlink

<p>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 <i>SPPsolver</i>, 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 <i>SPPsolver</i>. We use real-world datasets to perform experiments and compare with state-of-the-art algorithms, the results demonstrate the superiority and efficiency of <i>SPPsolver</i>.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年11月24日

查看全文
  • Wenwu Yan,
  • Bo Hu,
  • Weiqing Huang,
  • Chao Ma,
  • Xiaobin Tian,
  • Min Yu

摘要

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.