{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T04:35:16Z","timestamp":1772339716502,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"The Chinese University of Hong Kong"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,10,27]]},"DOI":"10.1145\/3676536.3676748","type":"proceedings-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:21:20Z","timestamp":1744204880000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["DiffSAT: Differential MaxSAT Layer for SAT Solving"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7835-3024","authenticated-orcid":false,"given":"Yu","family":"Zhang","sequence":"first","affiliation":[{"name":"CSE, The Chinese University of Hong Kong, Shatin, Hong Kong"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3195-9348","authenticated-orcid":false,"given":"Hui-Ling","family":"Zhen","sequence":"additional","affiliation":[{"name":"Noah's Ark Lab, Huawei, Shatin, Hong Kong"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2236-8784","authenticated-orcid":false,"given":"Mingxuan","family":"Yuan","sequence":"additional","affiliation":[{"name":"Noah's Ark Lab, Huawei, Shatin, Hong Kong"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6406-4810","authenticated-orcid":false,"given":"Bei","family":"Yu","sequence":"additional","affiliation":[{"name":"CSE, The Chinese University of Hong Kong, Shatin, Hong Kong"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions.","author":"Balyo Tomas","year":"2023","unstructured":"Tomas Balyo, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda. 2023. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. (2023)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/DTIS.2014.6850674"},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. of SAT Competition","author":"Biere Armin","year":"2022","unstructured":"Armin Biere, Mathias Fleury, T Balyo, M Heule, M Iser, M J\u00e4rvisalo, and M Suda. 2022. Gimsatul, IsaSAT and Kissat entering the SAT competition 2022. Proc. of SAT Competition (2022), 10--11."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i4.25505"},{"key":"e_1_3_2_1_5_1","unstructured":"Stephen A Cook. 2023. The complexity of theorem-proving procedures. In Logic Automata and Computational Complexity: The Works of Stephen A. Cook. 143--152."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISTCS.1995.377033"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895480192243516"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/227683.227684"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/227683.227684"},{"key":"e_1_3_2_1_10_1","volume-title":"SBVA-CADICAL and SBVA-KISSAT: Structured Bounded Variable Addition. SAT COMPETITION 2023 ([n. d.]), 18","author":"Haberlandt Andrew","unstructured":"Andrew Haberlandt and Harrison Green. [n. d.]. SBVA-CADICAL and SBVA-KISSAT: Structured Bounded Variable Addition. SAT COMPETITION 2023 ([n. d.]), 18."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/795663.796364"},{"key":"e_1_3_2_1_12_1","volume-title":"Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980","author":"Kingma Diederik P","year":"2014","unstructured":"Diederik P Kingma and Jimmy Ba. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)."},{"key":"e_1_3_2_1_13_1","volume-title":"Pytorch: An imperative style, high-performance deep learning library. Advances in neural information processing systems 32","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. 2019. Pytorch: An imperative style, high-performance deep learning library. Advances in neural information processing systems 32 (2019)."},{"key":"e_1_3_2_1_14_1","volume-title":"On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues. Mathematics of operations research 23, 2","author":"Pataki G\u00e1bor","year":"1998","unstructured":"G\u00e1bor Pataki. 1998. On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues. Mathematics of operations research 23, 2 (1998), 339--358."},{"key":"e_1_3_2_1_15_1","volume-title":"SAT 2019, Lisbon, Portugal, July 9--12, 2019, Proceedings 22","author":"Selsam Daniel","year":"2019","unstructured":"Daniel Selsam and Nikolaj Bj\u00f8rner. 2019. Guiding high-performance SAT solvers with unsat-core predictions. In Theory and Applications of Satisfiability Testing-SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9--12, 2019, Proceedings 22. Springer, 336--353."},{"key":"e_1_3_2_1_16_1","volume-title":"Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685","author":"Selsam Daniel","year":"2018","unstructured":"Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, and David L Dill. 2018. Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685 (2018)."},{"key":"e_1_3_2_1_17_1","volume-title":"SATformer: Transformer-Based UNSAT Core Learning. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD)","author":"Shi Zhengyuan","year":"2022","unstructured":"Zhengyuan Shi, Min Li, Sadaf Khan, Hui-Ling Zhen, Mingxuan Yuan, and Qiang Xu. 2022. SATformer: Transformer-Based UNSAT Core Learning. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD) (2022)."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD57390.2023.10323798"},{"key":"e_1_3_2_1_19_1","volume-title":"The mixing method: low-rank coordinate descent for semidefinite programming with diagonal constraints. arXiv preprint arXiv:1706.00476","author":"Wang Po-Wei","year":"2017","unstructured":"Po-Wei Wang, Wei-Cheng Chang, and J Zico Kolter. 2017. The mixing method: low-rank coordinate descent for semidefinite programming with diagonal constraints. arXiv preprint arXiv:1706.00476 (2017)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011641"},{"key":"e_1_3_2_1_21_1","volume-title":"The Twelfth International Conference on Learning Representations.","author":"Wang Wenxi","year":"2023","unstructured":"Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikkulainen. 2023. NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. In The Twelfth International Conference on Learning Representations."}],"event":{"name":"ICCAD '24: 43rd IEEE\/ACM International Conference on Computer-Aided Design","location":"Newark Liberty International Airport Marriott New York NY USA","acronym":"ICCAD '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA","IEEE EDS"]},"container-title":["Proceedings of the 43rd IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676748","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676536.3676748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:43:58Z","timestamp":1750290238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676748"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"references-count":21,"alternative-id":["10.1145\/3676536.3676748","10.1145\/3676536"],"URL":"https:\/\/doi.org\/10.1145\/3676536.3676748","relation":{},"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}