{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T09:43:54Z","timestamp":1763977434818,"version":"3.45.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T00:00:00Z","timestamp":1763942400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T00:00:00Z","timestamp":1763942400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cybersecurity"],"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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\n                    <jats:italic>SPPsolver<\/jats:italic>\n                    , 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\n                    <jats:italic>SPPsolver<\/jats:italic>\n                    . We use real-world datasets to perform experiments and compare with state-of-the-art algorithms, the results demonstrate the superiority and efficiency of\n                    <jats:italic>SPPsolver<\/jats:italic>\n                    .\n                  <\/jats:p>","DOI":"10.1186\/s42400-025-00421-1","type":"journal-article","created":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T09:39:12Z","timestamp":1763977152000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SPPsolver: a SAT-based algorithm for solving any stable paths problem correctly"],"prefix":"10.1186","volume":"8","author":[{"given":"Wenwu","family":"Yan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9317-1384","authenticated-orcid":false,"given":"Bo","family":"Hu","sequence":"additional","affiliation":[]},{"given":"Weiqing","family":"Huang","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Ma","sequence":"additional","affiliation":[]},{"given":"Xiaobin","family":"Tian","sequence":"additional","affiliation":[]},{"given":"Min","family":"Yu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,24]]},"reference":[{"key":"421_CR1","doi-asserted-by":"crossref","unstructured":"Beckett R, Gupta A, Mahajan R, Walker D (2018) Control plane compression. In: Proceedings of the 2018 conference of the ACM special interest group on data communication, pp 476\u2013489","DOI":"10.1145\/3230543.3230583"},{"key":"421_CR2","unstructured":"CAIDA (2024) As relationships and internet traffic dataset. https:\/\/www.caida.org\/catalog\/datasets\/as-relationships\/"},{"key":"421_CR3","doi-asserted-by":"crossref","unstructured":"Cheng Y, Luo N, Zhang J, Antonopoulos T, Piskac R, Xiang Q (2021) Looking for the maximum independent set: a new perspective on the stable path problem. In: INFOCOM 2021. IEEE, pp 1\u201310","DOI":"10.1109\/INFOCOM42981.2021.9488682"},{"issue":"4","key":"421_CR4","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/TNSM.2011.110311.100109","volume":"8","author":"L Cittadini","year":"2011","unstructured":"Cittadini L, Rimondini M, Vissicchio S, Corea M, Di Battista G (2011) From theory to practice: efficiently checking BGP configurations for guaranteed convergence. IEEE Trans Netw Serv Manag 8(4):387\u2013400","journal-title":"IEEE Trans Netw Serv Manag"},{"key":"421_CR5","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"421_CR6","first-page":"351","volume":"34","author":"X Fang","year":"2021","unstructured":"Fang X, Hu B, Ma C, Huang W (2021) Survey on network verification. J Softw 34(1):351\u2013380","journal-title":"J Softw"},{"key":"421_CR7","doi-asserted-by":"crossref","unstructured":"Fang X, Ding F, Huang B, Wang Z, Han G, Yang R, You L, Xiang Q, Kong L, Liu Y, Shu J (in press) Network can help check itself: accelerating SMT-based network configuration verification using network domain knowledge. In: INFOCOM 2024","DOI":"10.1109\/INFOCOM52122.2024.10621215"},{"key":"421_CR8","doi-asserted-by":"crossref","unstructured":"Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C (2004) DPLL (T): fast decision procedures. In: Computer aided verification: 16th international conference, CAV 2004, Boston, MA, USA, July 13\u201317, 2004. Proceedings, vol 16. Springer, pp 175\u2013188","DOI":"10.1007\/978-3-540-27813-9_14"},{"issue":"6","key":"421_CR9","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1109\/90.974523","volume":"9","author":"L Gao","year":"2001","unstructured":"Gao L, Rexford J (2001) Stable internet routing without global coordination. IEEE\/ACM Trans Netw 9(6):681\u2013692","journal-title":"IEEE\/ACM Trans Netw"},{"key":"421_CR10","doi-asserted-by":"crossref","unstructured":"Garcia-Luna-Aceves J (2022) Stable, loop-free, multi-path inter-domain routing using BGP. In: ICC 2022-IEEE international conference on communications. IEEE, pp 322\u2013328","DOI":"10.1109\/ICC45855.2022.9839159"},{"issue":"2","key":"421_CR11","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/90.993304","volume":"10","author":"TG Griffin","year":"2002","unstructured":"Griffin TG, Shepherd FB, Wilfong G (2002) The stable paths problem and interdomain routing. IEEE\/ACM Trans Netw 10(2):232\u2013243","journal-title":"IEEE\/ACM Trans Netw"},{"key":"421_CR12","volume-title":"Centurylink selects nuage networks SDN technology","author":"L Hedges","year":"2015","unstructured":"Hedges L (2015) Centurylink selects nuage networks SDN technology. Capacity Magazine"},{"key":"421_CR13","unstructured":"Hurricane (2025) Hurricane electric internet services. https:\/\/bgp.he.net\/"},{"key":"421_CR14","unstructured":"Pouryousef S, Gao L, Venkataramani A (2020) Towards logically centralized interdomain routing. In: 17th USENIX symposium on networked systems design and implementation (NSDI 20), pp 739\u2013757"},{"key":"421_CR15","doi-asserted-by":"crossref","unstructured":"Rekhter Y, Li T, Hares S (2006) RFC 4271: a border gateway protocol 4 (BGP-4)","DOI":"10.17487\/rfc4271"},{"key":"421_CR16","volume-title":"Discrete mathematics and its applications","author":"KH Rosen","year":"1999","unstructured":"Rosen KH, Krithivasan K (1999) Discrete mathematics and its applications, vol 6. McGraw-Hill, New York"},{"key":"421_CR17","doi-asserted-by":"crossref","unstructured":"Scheder D (2024) PPSZ is better than you think. TheoretiCS 3","DOI":"10.46298\/theoretics.24.5"},{"key":"421_CR18","doi-asserted-by":"crossref","unstructured":"Shao X, Gao L (2020) Verifying policy-based routing at internet scale. In: IEEE INFOCOM 2020-IEEE conference on computer communications. IEEE, pp 2293\u20132302","DOI":"10.1109\/INFOCOM41043.2020.9155235"},{"key":"421_CR19","doi-asserted-by":"crossref","unstructured":"Tang A, Beckett R, Benaloh S, Jayaraman K, Patil T, Millstein T, Varghese G (2023) Lightyear: using modularity to scale BGP control plane verification. In: Proceedings of the ACM SIGCOMM 2023 conference, pp 94\u2013107","DOI":"10.1145\/3603269.3604842"},{"key":"421_CR20","doi-asserted-by":"crossref","unstructured":"Thijm TA, Beckett R, Gupta A, Walker D (2022) Kirigami, the verifiable art of network cutting. In: 2022 IEEE 30th international conference on network protocols (ICNP). IEEE, pp 1\u201312","DOI":"10.1109\/ICNP55882.2022.9940333"},{"key":"421_CR21","unstructured":"Vahidi A (2003) JDD, a pure java BDD and Z-BDD library. https:\/\/bitbucket.org\/vahidi\/jdd\/"}],"container-title":["Cybersecurity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s42400-025-00421-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s42400-025-00421-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s42400-025-00421-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T09:39:15Z","timestamp":1763977155000},"score":1,"resource":{"primary":{"URL":"https:\/\/cybersecurity.springeropen.com\/articles\/10.1186\/s42400-025-00421-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,24]]},"references-count":21,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12]]}},"alternative-id":["421"],"URL":"https:\/\/doi.org\/10.1186\/s42400-025-00421-1","relation":{},"ISSN":["2523-3246"],"issn-type":[{"value":"2523-3246","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,24]]},"assertion":[{"value":"18 September 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 June 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"103"}}