{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T14:18:12Z","timestamp":1765808292676,"version":"3.28.0"},"reference-count":42,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T00:00:00Z","timestamp":1698451200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T00:00:00Z","timestamp":1698451200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,10,28]]},"DOI":"10.1109\/iccad57390.2023.10323731","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T18:58:45Z","timestamp":1701370725000},"page":"1-4","source":"Crossref","is-referenced-by-count":6,"title":["SATformer: Transformer-Based UNSAT Core Learning"],"prefix":"10.1109","author":[{"given":"Zhengyuan","family":"Shi","sequence":"first","affiliation":[{"name":"The Chinese University of Hong Kong"}]},{"given":"Min","family":"Li","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong"}]},{"given":"Yi","family":"Liu","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong"}]},{"given":"Sadaf","family":"Khan","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong"}]},{"given":"Junhua","family":"Huang","sequence":"additional","affiliation":[{"name":"Noah's Ark Lab, Huawei"}]},{"given":"Hui-Ling","family":"Zhen","sequence":"additional","affiliation":[{"name":"Noah's Ark Lab, Huawei"}]},{"given":"Mingxuan","family":"Yuan","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong"}]},{"given":"Qiang","family":"Xu","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2001.915010"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337546"},{"issue":"53","key":"ref4","first-page":"1","article-title":"Minisat v 1, 13-a sat solver with conflictclause minimization","volume":"2005","author":"Sorensson","year":"2005","journal-title":"SAT"},{"key":"ref5","first-page":"51","article-title":"CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020","volume":"B-2020\u20131","author":"Biere","year":"2020","journal-title":"Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, ser. Department of Computer Science Report Series B"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/026\/25"},{"key":"ref7","article-title":"Parafrost at the sat race 2021","volume":"32","author":"Osama","year":"2021","journal-title":"SAT COMPE-TITION 2021"},{"key":"ref8","first-page":"8","article-title":"Cadical at the sat race 2019","author":"QUEUE","year":"2019","journal-title":"SAT RACE 2019"},{"key":"ref9","first-page":"50","article-title":"Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020","volume":"2020","author":"Fleury","year":"2020","journal-title":"SAT COMPETITION"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213018400018"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253719"},{"key":"ref12","first-page":"7","article-title":"Glucose: a solver that predicts learnt clauses quality","author":"Audemard","year":"2009","journal-title":"SAT Competition"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ITC50671.2022.00010"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13800-3_7"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253718"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.1995.466367"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1997.643606"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s11633-022-1396-2"},{"key":"ref22","article-title":"Learning a sat solver from single-bit supervision","author":"Selsam","year":"2018","journal-title":"arXiv preprint"},{"key":"ref23","article-title":"Learning to solve circuit-sat: An unsupervised differentiable approach","volume-title":"International Conference on Learning Representations","author":"Amizadeh","year":"2018"},{"key":"ref24","article-title":"Deepsat: An eda-driven learning framework for sat","author":"Li","year":"2022","journal-title":"arXiv preprint"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/164"},{"key":"ref26","first-page":"9608","article-title":"Can q-learning with graph networks learn a generalizable branching heuristic for a sat solver?","volume":"33","author":"Kurin","year":"2020","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref27","first-page":"arXiv-2110","article-title":"Neurocomb: Improving sat solving with graph neural networks","author":"Wang","year":"2021","journal-title":"arXiv e-prints"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1706.03762"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45439-5_3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/P19-1176"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2010.11929"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV48922.2021.00986"},{"key":"ref33","article-title":"Transformer-based machine learning for fast sat solvers and logic synthesis","volume-title":"arXiv preprint","author":"Shi","year":"2021"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007379606734"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177729694"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2017.106"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200987"},{"key":"ref39","article-title":"Adam: A method for stochastic optimization","author":"Kingma","year":"2014","journal-title":"arXiv preprint"},{"key":"ref40","article-title":"Goal-aware neural sat solver","author":"Ozolins","year":"2021","journal-title":"arXiv preprint"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"ref42","first-page":"221","article-title":"Boosting minimal unsatisfiable core extraction","author":"Nadel","year":"2010","journal-title":"Formal Methods in Computer Aided Design"}],"event":{"name":"2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD)","start":{"date-parts":[[2023,10,28]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2023,11,2]]}},"container-title":["2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10323590\/10323543\/10323731.pdf?arnumber=10323731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T22:06:23Z","timestamp":1709417183000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10323731\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,28]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/iccad57390.2023.10323731","relation":{},"subject":[],"published":{"date-parts":[[2023,10,28]]}}}