{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:33:07Z","timestamp":1763724787936,"version":"3.44.0"},"reference-count":39,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"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":[[2025,6,22]]},"DOI":"10.1109\/dac63849.2025.11133310","type":"proceedings-article","created":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T17:35:41Z","timestamp":1757957741000},"page":"1-7","source":"Crossref","is-referenced-by-count":1,"title":["Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving"],"prefix":"10.1109","author":[{"given":"Zhengyuan","family":"Shi","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":"Tiebing","family":"Tang","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":"Jiaying","family":"Zhu","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":"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":"Hui-Ling","family":"Zhen","sequence":"additional","affiliation":[{"name":"Noah’s Ark Lab, Huawei,Hong Kong,S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingxuan","family":"Yuan","sequence":"additional","affiliation":[{"name":"Noah’s Ark Lab, Huawei,Hong Kong,S.A.R"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhufei","family":"Chu","sequence":"additional","affiliation":[{"name":"Ningbo University,Faculty of Electrical Engineering and Computer Science,Ningbo,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":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"issue":"53","key":"ref2","first-page":"1","article-title":"Minisat v1. 13-a sat solver with conflictclause minimization","volume-title":"Theory and Applications of Satisfiability Testing-SAT 2005","volume":"2005","author":"Sorensson"},{"key":"ref3","first-page":"50","article-title":"Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020","volume":"2020","author":"Biere","year":"2020","journal-title":"SAT COMPETITION"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46135-3_13"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_22"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_48"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ASP-DAC47756.2020.9045559"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3380446.3430622"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD57390.2023.10323798"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114927"},{"key":"ref13","article-title":"The epfl logic synthesis libraries","author":"Soeken","year":"2018","journal-title":"arXiv preprint arXiv:1805.05121"},{"key":"ref14","first-page":"133","article-title":"Conflict-driven clause learning sat solvers","volume-title":"Handbook of satisfiability","author":"Marques-Silva"},{"key":"ref15","first-page":"399","article-title":"Predicting learnt clauses quality in modern sat solvers","volume-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence","author":"Audemard"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/iccad57390.2023.10323731"},{"key":"ref18","first-page":"262","article-title":"Solving the round robin problem using propositional logic","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"17","author":"B\u00e9jar"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364479"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643505"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/DAC56929.2023.10248001"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/iccad.1988.122551"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-024-4155-7"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530497"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3676536.3676791"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ITC50671.2022.00027"},{"article-title":"Aiger (aiger is a format, library and set of utilities for andinverter graphs (aigs))","year":"2006","author":"Biere","key":"ref27"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"ref29","first-page":"49","article-title":"The decomposition and factorization of boolean expressions","volume-title":"International Symposium on Computer Architecture (ISCA 1982)","author":"Brayton"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.811447"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114868"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1038\/nature14236"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190015"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/84"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065693"},{"key":"ref37","article-title":"Abc: A system for sequential synthesis and verification","volume":"17","author":"Mishchenko","year":"2007"},{"author":"Heule","key":"ref38","article-title":"Proceedings of sat competition 2024: Solver, benchmark and proof checker descriptions"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"}],"event":{"name":"2025 62nd ACM\/IEEE Design Automation Conference (DAC)","start":{"date-parts":[[2025,6,22]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2025,6,25]]}},"container-title":["2025 62nd ACM\/IEEE Design Automation Conference (DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11132383\/11132091\/11133310.pdf?arnumber=11133310","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T05:25:15Z","timestamp":1758000315000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11133310\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/dac63849.2025.11133310","relation":{},"subject":[],"published":{"date-parts":[[2025,6,22]]}}}