{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T10:03:47Z","timestamp":1766484227384,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T00:00:00Z","timestamp":1661126400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Zhejiang Lab","award":["2022QA0AB05"],"award-info":[{"award-number":["2022QA0AB05"]}]},{"DOI":"10.13039\/100017489","name":"Alibaba DAMO Academy","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100017489","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ministry of Education, China","award":["2021FNA02008"],"award-info":[{"award-number":["2021FNA02008"]}]},{"name":"NSFC","award":["62172345,"],"award-info":[{"award-number":["62172345,"]}]},{"name":"Tan Kah Kee Innovation Laboratory","award":["HRTP-2022-34"],"award-info":[{"award-number":["HRTP-2022-34"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,22]]},"DOI":"10.1145\/3528082.3544835","type":"proceedings-article","created":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T18:19:17Z","timestamp":1660587557000},"page":"24-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["P4-DPLL"],"prefix":"10.1145","author":[{"given":"Jinghui","family":"Jiang","sequence":"first","affiliation":[{"name":"Xiamen University and Tan Kah Kee Innovation Laboratory"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenpei","family":"Huang","sequence":"additional","affiliation":[{"name":"Xiamen University and Tan Kah Kee Innovation Laboratory"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiao","family":"Xiang","sequence":"additional","affiliation":[{"name":"Xiamen University and Tan Kah Kee Innovation Laboratory"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu","family":"Tang","sequence":"additional","affiliation":[{"name":"Xiamen University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiwu","family":"Shu","sequence":"additional","affiliation":[{"name":"Xiamen University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,22]]},"reference":[{"unstructured":"2000. SATLIB - Benchmark Problems. https:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html.  2000. SATLIB - Benchmark Problems. https:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html.","key":"e_1_3_2_1_1_1"},{"unstructured":"2022. The International SAT Competition. http:\/\/www.satcompetition.org.  2022. The International SAT Competition. http:\/\/www.satcompetition.org.","key":"e_1_3_2_1_2_1"},{"unstructured":"2022. P4-DPLL. https:\/\/p4-dpll.github.io\/.  2022. P4-DPLL. https:\/\/p4-dpll.github.io\/.","key":"e_1_3_2_1_3_1"},{"unstructured":"Barefoot 2019. Barefoot S9180-32X Switch. https:\/\/www.ufispace.com\/uploads\/able\/files\/productfilemanager\/000045467d1fc648d792c404372956a0.pdf.  Barefoot 2019. Barefoot S9180-32X Switch. https:\/\/www.ufispace.com\/uploads\/able\/files\/productfilemanager\/000045467d1fc648d792c404372956a0.pdf.","key":"e_1_3_2_1_4_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1145\/3229591.3229596"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1007\/978-3-642-36742-7_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/368273.368557"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/321033.321034"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1145\/3230543.3230555"},{"volume-title":"Handbook of Parallel Constraint Reasoning","author":"Hamadi Youssef","unstructured":"Youssef Hamadi and Lakhdar Sais . 2018. Handbook of Parallel Constraint Reasoning . Springer . Youssef Hamadi and Lakhdar Sais. 2018. Handbook of Parallel Constraint Reasoning. Springer.","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/3359989.3365433"},{"key":"e_1_3_2_1_12_1","volume-title":"NetChain: Scale-Free Sub-RTT Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Jin Xin","year":"2018","unstructured":"Xin Jin , Xiaozhou Li , Haoyu Zhang , Nate Foster , Jeongkeun Lee , Robert Soul\u00e9 , Changhoon Kim , and Ion Stoica . 2018 . NetChain: Scale-Free Sub-RTT Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18) . 35--49. Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soul\u00e9, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). 35--49."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1145\/3132747.3132764"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1145\/1857927.1857937"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/2890955.2890968"},{"key":"e_1_3_2_1_17_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Li Jialin","year":"2020","unstructured":"Jialin Li , Jacob Nelson , Ellis Michael , Xin Jin , and Dan RK Ports . 2020 . Pegasus: Tolerating Skewed Workloads in Distributed Storage with {In-Network} Coherence Directories . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . 387--406. Jialin Li, Jacob Nelson, Ellis Michael, Xin Jin, and Dan RK Ports. 2020. Pegasus: Tolerating Skewed Workloads in Distributed Storage with {In-Network} Coherence Directories. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 387--406."},{"key":"e_1_3_2_1_18_1","volume-title":"13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16)","author":"Li Xiaozhou","year":"2016","unstructured":"Xiaozhou Li , Raghav Sethi , Michael Kaminsky , David G Andersen , and Michael J Freedman . 2016 . Be Fast, Cheap and in Control with {SwitchKV} . In 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16) . 31--44. Xiaozhou Li, Raghav Sethi, Michael Kaminsky, David G Andersen, and Michael J Freedman. 2016. Be Fast, Cheap and in Control with {SwitchKV}. In 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16). 31--44."},{"key":"e_1_3_2_1_19_1","volume-title":"Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, et al.","author":"Li Yuliang","year":"2019","unstructured":"Yuliang Li , Rui Miao , Hongqiang Harry Liu , Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, et al. 2019 . HPCC : High precision congestion control. In Proceedings of the ACM Special Interest Group on Data Communication. 44--58. Yuliang Li, Rui Miao, Hongqiang Harry Liu, Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, et al. 2019. HPCC: High precision congestion control. In Proceedings of the ACM Special Interest Group on Data Communication. 44--58."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1145\/3037697.3037731"},{"key":"e_1_3_2_1_21_1","volume-title":"DistCache: Provable Load Balancing for Large-Scale Storage Systems with Distributed Caching. In 17th USENIX Conference on File and Storage Technologies (FAST 19)","author":"Liu Zaoxing","year":"2019","unstructured":"Zaoxing Liu , Zhihao Bai , Zhenming Liu , Xiaozhou Li , Changhoon Kim , Vladimir Braverman , Xin Jin , and Ion Stoica . 2019 . DistCache: Provable Load Balancing for Large-Scale Storage Systems with Distributed Caching. In 17th USENIX Conference on File and Storage Technologies (FAST 19) . 143--157. Zaoxing Liu, Zhihao Bai, Zhenming Liu, Xiaozhou Li, Changhoon Kim, Vladimir Braverman, Xin Jin, and Ion Stoica. 2019. DistCache: Provable Load Balancing for Large-Scale Storage Systems with Distributed Caching. In 17th USENIX Conference on File and Storage Technologies (FAST 19). 143--157."},{"volume-title":"GRASP---a new search algorithm for satisfiability","author":"Marques Silva Jo\u00e3o P","unstructured":"Jo\u00e3o P Marques Silva and Karem A Sakallah . 2003. GRASP---a new search algorithm for satisfiability . In The Best of ICCAD. Springer , 73--89. Jo\u00e3o P Marques Silva and Karem A Sakallah. 2003. GRASP---a new search algorithm for satisfiability. In The Best of ICCAD. Springer, 73--89.","key":"e_1_3_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1109\/ACCESS.2020.2980008"},{"key":"e_1_3_2_1_25_1","volume-title":"Dan RK Ports, and Peter Richt\u00e1rik","author":"Sapio Amedeo","year":"2019","unstructured":"Amedeo Sapio , Marco Canini , Chen-Yu Ho , Jacob Nelson , Panos Kalnis , Changhoon Kim , Arvind Krishnamurthy , Masoud Moshref , Dan RK Ports, and Peter Richt\u00e1rik . 2019 . Scaling distributed machine learning with in-network aggregation. arXiv preprint arXiv:1903.06701 (2019). Amedeo Sapio, Marco Canini, Chen-Yu Ho, Jacob Nelson, Panos Kalnis, Changhoon Kim, Arvind Krishnamurthy, Masoud Moshref, Dan RK Ports, and Peter Richt\u00e1rik. 2019. Scaling distributed machine learning with in-network aggregation. arXiv preprint arXiv:1903.06701 (2019)."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1145\/3452296.3472887"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1145\/3387514.3405857"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1145\/3123878.3131998"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.1049\/ip-cdt:20000482"},{"key":"e_1_3_2_1_30_1","volume-title":"Harmonia: Near-linear scalability for replicated storage with in-network conflict detection. arXiv preprint arXiv:1904.08964","author":"Zhu Hang","year":"2019","unstructured":"Hang Zhu , Zhihao Bai , Jialin Li , Ellis Michael , Dan Ports , Ion Stoica , and Xin Jin . 2019 . Harmonia: Near-linear scalability for replicated storage with in-network conflict detection. arXiv preprint arXiv:1904.08964 (2019). Hang Zhu, Zhihao Bai, Jialin Li, Ellis Michael, Dan Ports, Ion Stoica, and Xin Jin. 2019. Harmonia: Near-linear scalability for replicated storage with in-network conflict detection. arXiv preprint arXiv:1904.08964 (2019)."},{"key":"e_1_3_2_1_31_1","volume-title":"RackSched: A Microsecond-Scale Scheduler for Rack-Scale Computers. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Zhu Hang","year":"2020","unstructured":"Hang Zhu , Kostis Kaffes , Zixu Chen , Zhenming Liu , Christos Kozyrakis , Ion Stoica , and Xin Jin . 2020 . RackSched: A Microsecond-Scale Scheduler for Rack-Scale Computers. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . 1225--1240. Hang Zhu, Kostis Kaffes, Zixu Chen, Zhenming Liu, Christos Kozyrakis, Ion Stoica, and Xin Jin. 2020. RackSched: A Microsecond-Scale Scheduler for Rack-Scale Computers. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 1225--1240."}],"event":{"sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"acronym":"SIGCOMM '22","name":"SIGCOMM '22: ACM SIGCOMM 2022 Conference","location":"Amsterdam Netherlands"},"container-title":["Proceedings of the ACM SIGCOMM Workshop on Formal Foundations and Security of Programmable Network Infrastructures"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3528082.3544835","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3528082.3544835","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:25Z","timestamp":1750186945000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3528082.3544835"}},"subtitle":["accelerating SAT solving using switching ASICs"],"short-title":[],"issued":{"date-parts":[[2022,8,22]]},"references-count":30,"alternative-id":["10.1145\/3528082.3544835","10.1145\/3528082"],"URL":"https:\/\/doi.org\/10.1145\/3528082.3544835","relation":{},"subject":[],"published":{"date-parts":[[2022,8,22]]},"assertion":[{"value":"2022-08-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}