{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T08:31:59Z","timestamp":1774341119196,"version":"3.50.1"},"reference-count":49,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2023YFB3307503"],"award-info":[{"award-number":["2023YFB3307503"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62172072"],"award-info":[{"award-number":["62172072"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62202025"],"award-info":[{"award-number":["62202025"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62302528"],"award-info":[{"award-number":["62302528"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62422203"],"award-info":[{"award-number":["62422203"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62522201"],"award-info":[{"award-number":["62522201"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Young Elite Scientist Sponsorship Program by China Association for Science and Technology","award":["YESS20230566"],"award-info":[{"award-number":["YESS20230566"]}]},{"name":"Beijing Natural Science Foundation","award":["L241050"],"award-info":[{"award-number":["L241050"]}]},{"DOI":"10.13039\/100015804","name":"China Computer Federation (CCF)-Huawei Populus Grove Fund","doi-asserted-by":"publisher","award":["CCF-HuaweiFM2024005"],"award-info":[{"award-number":["CCF-HuaweiFM2024005"]}],"id":[{"id":"10.13039\/100015804","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Fundamental Research Fund Project of Beihang University"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2026,4]]},"DOI":"10.1109\/tcad.2025.3608060","type":"journal-article","created":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T17:32:09Z","timestamp":1757439129000},"page":"1841-1851","source":"Crossref","is-referenced-by-count":0,"title":["<i>CirOPT<\/i>\n                    : Toward Effective Combinational Equivalence Checking via Compiler Optimization"],"prefix":"10.1109","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-2769-9337","authenticated-orcid":false,"given":"Shaoke","family":"Cui","sequence":"first","affiliation":[{"name":"School of Software, Beihang University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5028-1064","authenticated-orcid":false,"given":"Chuan","family":"Luo","sequence":"additional","affiliation":[{"name":"School of Software, Beihang University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1063-2025","authenticated-orcid":false,"given":"Zhenwei","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Software, Beihang University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5493-8497","authenticated-orcid":false,"given":"Jiabao","family":"Lin","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0975-4613","authenticated-orcid":false,"given":"Wei","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Central South University, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8132-2380","authenticated-orcid":false,"given":"Chanjuan","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Dalian University of Technology, Dalian, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3473-9703","authenticated-orcid":false,"given":"Chunming","family":"Hu","sequence":"additional","affiliation":[{"name":"School of Software, Beihang University, Beijing, China"}]}],"member":"263","reference":[{"key":"ref1","first-page":"1","article-title":"Clausal congruence closure, \u201cClausal congruence closure","volume-title":"Proc. SAT","volume":"305","author":"Biere"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218691"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681580"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147044"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TCSI.2024.3388256"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.882484"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/43.771175"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2023.3297069"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/5.52213"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2001.915010"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2008.4751838"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SoC54400.2022.9939646"},{"key":"ref13","first-page":"547","article-title":"SAT-based combinational equivalence checking with don\u2019t care","volume-title":"Proc. ITC-CSCC","author":"Nam"},{"key":"ref14","doi-asserted-by":"crossref","DOI":"10.1109\/DAC63849.2025.11132604","article-title":"X-SAT: An efficient circuit-based sat solver","volume-title":"Proc. 62st ACM\/IEEE Design Autom. Conf. (DAC)","author":"Qian"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.mejo.2023.106005"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586331"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643505"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD57390.2023.10323876"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref22","article-title":"Improved large-scale SAT sweeping","volume-title":"Proc. IWLS","author":"Zhang"},{"key":"ref23","article-title":"On-the-fly compression of logical circuits","author":"Ganai","year":"2000"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2017.7934583"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2017.7858312"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3287624.3287671"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"ref30","first-page":"8","article-title":"CaDiCaL, gimsatul, IsaSAT and kissat entering the SAT competition 2024","volume-title":"Proc. SAT","author":"Biere"},{"key":"ref31","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho","year":"1986"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3508362"},{"key":"ref34","volume-title":"LLVM User Guides","year":"2025"},{"key":"ref35","first-page":"1","article-title":"Collection of combinational arithmetic miters submitted to the SAT competition 2016","volume":"2016","author":"Biere","year":"2016","journal-title":"SAT Competition"},{"key":"ref36","article-title":"The EPFL combinational benchmark suite","volume-title":"Proc. 24th Int. Workshop Log. Synth. (IWLS)","author":"Amar\u00fa"},{"key":"ref37","article-title":"The AIGER and-inverter graph (AIG) format version 20070427","author":"Brummayer","year":"2007"},{"key":"ref38","first-page":"20","article-title":"Kissat MAB-DC in SAT competition 2024","volume-title":"Proc. SAT Competition, Solver, Benchmark Proof Checker Descriptions","volume":"B-2024-1","author":"Liu"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_29"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref41","first-page":"1","article-title":"Improving local search for structured SAT formulas via unit propagation based construct and cut initialization","volume-title":"Proc. CP Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik","author":"Cai"},{"key":"ref42","volume-title":"Advanced Compiler Design and Implementation","author":"Muchnick","year":"1997"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/800028.808480"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207154"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103136"},{"key":"ref47","article-title":"Witnessing control flow graph optimizations","author":"Casula","year":"2015"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2797022.2797030"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/43\/11450487\/11154022.pdf?arnumber=11154022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T05:17:02Z","timestamp":1774329422000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11154022\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4]]},"references-count":49,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2025.3608060","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4]]}}}