{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T15:25:37Z","timestamp":1758122737445,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,7,9]],"date-time":"2023-07-09T00:00:00Z","timestamp":1688860800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,7,9]],"date-time":"2023-07-09T00:00:00Z","timestamp":1688860800000},"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,7,9]]},"DOI":"10.1109\/dac56929.2023.10248001","type":"proceedings-article","created":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T17:31:31Z","timestamp":1694799091000},"page":"1-6","source":"Crossref","is-referenced-by-count":3,"title":["On EDA-Driven Learning for SAT Solving"],"prefix":"10.1109","author":[{"given":"Min","family":"Li","sequence":"first","affiliation":[{"name":"The Chinese University of Hong Kong,Department of Computer Science and Engineering,Hong Kong S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengyuan","family":"Shi","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong,Department of Computer Science and Engineering,Hong Kong S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiuxia","family":"Lai","sequence":"additional","affiliation":[{"name":"Communication University of China,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sadaf","family":"Khan","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong,Department of Computer Science and Engineering,Hong Kong S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,State Key Laboratory of Computer Science,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiang","family":"Xu","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong,Department of Computer Science and Engineering,Hong Kong S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364479"},{"key":"ref15","first-page":"4797","article-title":"Conditional image generation with pixelcnn decoders","author":"oord","year":"2016","journal-title":"Proceedings of the 30th International Conference on Neural Information Processing Systems"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1145\/1146909.1147048","article-title":"Dag-aware aig rewriting: A fresh look at combinational logic synthesis","author":"mishchenko","year":"2006","journal-title":"2006 43rd ACM\/IEEE Design Automation Conference"},{"key":"ref11","first-page":"5627","article-title":"Augment with care: Contrastive learning for combinatorial problems","author":"duan","year":"2022","journal-title":"ICML"},{"key":"ref10","article-title":"Learning to solve circuit-SAT: An unsupervised differentiable approach","author":"amizadeh","year":"2019","journal-title":"International Conference on Learning Representations"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10479-010-0693-2"},{"key":"ref1","first-page":"292","article-title":"Satisfiability planning with constraints on the number of actions","author":"b\u00fcttner","year":"2005","journal-title":"International Conference on Automated Planning and Scheduling"},{"key":"ref17","article-title":"Graph neural network guided local search for the traveling salesperson problem","author":"hudson","year":"2022","journal-title":"International Conference on Learning Representations"},{"key":"ref16","article-title":"Learning combinatorial optimization algorithms over graphs","volume":"30","author":"khalil","year":"2017","journal-title":"Advances in neural information processing systems"},{"key":"ref19","article-title":"Directed acyclic graph neural networks","author":"thost","year":"2021","journal-title":"International Conference on Learning Representations"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2020.2978386"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2975585"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/19.4.322"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_24"},{"key":"ref25","first-page":"4080","article-title":"Prototypical networks for few-shot learning","author":"snell","year":"2017","journal-title":"Proceedings of the 31st International Conference on Neural Information Processing Systems"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530497"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"Abc: An academic industrial-strength verification tool","author":"brayton","year":"2010","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.811447"},{"key":"ref28","article-title":"Fast graph representation learning with PyTorch Geometric","author":"fey","year":"2019","journal-title":"ICLR Workshop on Representation Learning on Graphs and Manifolds"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643505"},{"key":"ref8","first-page":"1177","article-title":"Nlocalsat: boosting local search with solution prediction","author":"zhang","year":"2021","journal-title":"Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence"},{"key":"ref7","article-title":"Learning local search heuristics for Boolean satisfiability","volume":"32","author":"yolcu","year":"2019","journal-title":"NeurIPS"},{"key":"ref9","article-title":"Learning a SAT solver from single-bit supervision","author":"selsam","year":"2019","journal-title":"International Conference on Learning Representations"},{"key":"ref4","first-page":"1","article-title":"Minisat v1. 13-a sat solver with conflict-clause minimization","volume":"2005","author":"sorensson","year":"2005","journal-title":"SAT"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"ref6","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":"NeurIPS"},{"key":"ref5","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"}],"event":{"name":"2023 60th ACM\/IEEE Design Automation Conference (DAC)","start":{"date-parts":[[2023,7,9]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2023,7,13]]}},"container-title":["2023 60th ACM\/IEEE Design Automation Conference (DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10247654\/10247655\/10248001.pdf?arnumber=10248001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,2]],"date-time":"2023-10-02T17:41:32Z","timestamp":1696268492000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10248001\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,9]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/dac56929.2023.10248001","relation":{},"subject":[],"published":{"date-parts":[[2023,7,9]]}}}