Towards optimal path encoding using SAT solver
Authors: 
Dong Guo, Ying ZhangAuthors Info & Claims
Pages 52 - 54
Abstract
A Software-Defined Networking with programmable data-plane allows applications to realize policies by generating both datapath layouts and rules on switches. However, computing optimized datapath layouts and populating the compact rules for such datapaths can be overwhelmingly complex. This paper introduces a generic approach to realize network-wide policies in network, then derive optimal encoding for paths and forwarding rules for switches by modeling the process as a SAT problem. Finally, the evaluations on real ISP topologies show that our solution achieves about a 50% reduction of the path encoding length in average compare with the state of the art.
References
[1]
A. Hari et al. 2015. Path Switching : Reduced-state flow handling in SDNusing path information. In Proc. of CoNEXT. IEEE, 1--7.
[2]
A. Hari, U. Niesen, and Wilfong. 2017. On the Problem of Optimal Path Encoding for Software-Defined Networks. IEEE/ACM Transactions on Networking 25 (2017), 189--198.
[3]
Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113--126.
[4]
Simon Knight, Hung X. Nguyen, Nick Falkner, Rhys Bowden, and Matthew Roughan. 2011. The Internet Topology Zoo. IEEE Journal on Selected Areas in Communications 29(9) (2011), 1765--1775.
[5]
L. D. Moura and N. Bjørner. 2008. An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340.
[6]
N. Spring, R. Mahajan, and D. Wetherall. Aug. 2002. Measuring ISP topologies with rocketfuel. In Proc. ACM SIGCOMM. 133--145.
[7]
C. A. Sunshine. 1977. Source routing in computer networks. ACM SIGCOMM Comput. Commun 7, 1 (1977), 29--33.
[8]
Andreas Voellmy, Junchang Wang, Y Richard Yang, Bryan Ford, and Paul Hudak. 2013. Maple: Simplifying SDN Programming Using Algorithmic Policies. In Proceedings of the ACM SIGCOMM. 87--98.
Recommendations
Natural Max-SAT Encoding of Min-SAT
LION 6: Revised Selected Papers of the 6th International Conference on Learning and Intelligent Optimization - Volume 7219We show that there exists a natural encoding which transforms Min-SAT instances into Max-SAT instances. Unlike previous encodings, this natural encoding keeps the same variables, and the optimal assignment for the Min-SAT instance is identical to the ...
A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system designThe state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2020
96 pages
ISBN:9781450380485
DOI:10.1145/3405837
Copyright © 2020 Owner/Author.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 14 September 2021
Check for updates
Qualifiers
- Poster
Conference
SIGCOMM '20
Sponsor:
Acceptance Rates
Overall Acceptance Rate 92 of 158 submissions, 58%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 51Total Downloads
- Downloads (Last 12 months)13
- Downloads (Last 6 weeks)2
Reflects downloads up to 29 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in