{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T06:47:07Z","timestamp":1785912427204,"version":"3.56.0"},"reference-count":71,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"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":[[2026,6]]},"DOI":"10.1109\/isca66397.2026.00165","type":"proceedings-article","created":{"date-parts":[[2026,8,4]],"date-time":"2026-08-04T19:08:48Z","timestamp":1785870528000},"page":"2349-2363","source":"Crossref","is-referenced-by-count":0,"title":["SATIC: An Optimizing Ising Compiler for SAT(isfiability)"],"prefix":"10.1109","author":[{"given":"Ahmet","family":"Efe","sequence":"first","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"H\u00fcsrev","family":"C\u0131lasun","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abhimanyu","family":"Kumar","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nafisa S.","family":"Prova","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ziqing","family":"Zeng","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tahmida","family":"Islam","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruihong","family":"Yin","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chaohui","family":"Li","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Kreye","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chris H.","family":"Kim","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sachin S.","family":"Sapatnekar","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ulya R.","family":"Karpuzcu","sequence":"additional","affiliation":[{"name":"University of Minnesota","place":["Twin Cities, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_5"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1103\/physrevresearch.4.023062"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1103\/physreve.103.062130"},{"key":"ref5","first-page":"359","article-title":"Planning as Satisfiability","volume-title":"Proc. Eur. Conf. Artif. Intell. (ECAI)","volume":"1992","author":"Kautz","year":"1992"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref11","volume-title":"Handbook of Satisfiability","volume":"185","author":"Biere","year":"2009"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_16"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-88757-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77272-9_10"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23178-0_43"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.12205"},{"key":"ref17","first-page":"1782","article-title":"Efficient Exact Verification of Binarized Neural Networks","volume":"33","author":"Jia","year":"2020","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/811"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1038\/s41928-025-01393-3"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TASC.2014.2318294"},{"key":"ref22","article-title":"dwave-tabu","volume-title":"GitHub repository, 2022, version 0.5.0, commit 3b64cff","year":"2025"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-025-00037-y"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"ref25","volume-title":"Introduction to Algorithms","author":"Cormen","year":"2022"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006303512524"},{"key":"ref27","first-page":"331","article-title":"Where the Really Hard Problems Are","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI)","volume":"1","author":"Cheeseman","year":"1991"},{"key":"ref28","first-page":"283","article-title":"SATLIB: An Online Resource for Research on SAT","volume-title":"SAT 2000: Theory and Applications of Satisfiability Testing","author":"Hoos","year":"2000"},{"key":"ref29","first-page":"613","article-title":"Beitr\u00e4ge zum Verst\u00e4ndnis der magnetischen Eigenschaften in festen K\u00f6rpern","volume":"21","author":"Lenz","year":"1920","journal-title":"Physikalische Zeitschrift"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/BF02980577"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1103\/revmodphys.39.883"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1038\/nature10012"},{"key":"ref33","article-title":"Next-Generation Topology of D-Wave Quantum Processors","author":"Boothby","year":"2020","journal-title":"arXiv preprint"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-021-03582-4"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-021-03585-1"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.2015.2498601"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1038\/s41928-022-00749-3"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1038\/s41928-023-01021-y"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.3389\/fphy.2014.00005"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-014-9734-0"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1811.11538"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3583133.3596330"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-36030-5_3"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1038\/srep37107"},{"key":"ref45","volume-title":"Algorithms","author":"Dasgupta","year":"2006"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-024-60316-y"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190022"},{"key":"ref49","first-page":"203","article-title":"Using CSP Look-Back Techniques to Solve Real-World SAT Instances","volume-title":"Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI)","author":"Bayardo","year":"1997"},{"key":"ref50","volume-title":"Partitioning Optimization Problems for Hybrid Classical\/Quantum Execution","author":"Boost","year":"2017"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527414"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s42484-021-00039-9"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"ref55","first-page":"105","article-title":"The SAT Phase Transition","volume-title":"Proc. 11th European Conference on Artificial Intelligence (ECAI)","author":"Gent","year":"1994"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_19"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9074-1"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_6"},{"key":"ref59","article-title":"Quantum Annealing with More Than One Hundred Qubits","author":"Boixo","year":"2013","journal-title":"arXiv preprint"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1126\/science.1252319"},{"key":"ref61","article-title":"SAT Benchmarks to Assess Quantum-Inspired Solvers","volume-title":"GitHub repository","author":"Regli","year":"2025"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-018-38388-4"},{"key":"ref63","doi-asserted-by":"crossref","DOI":"10.3233\/FAIA336","volume-title":"Handbook of Satisfiability: Second Edition","author":"Biere","year":"2021"},{"key":"ref64","year":"2024","journal-title":"dwave-hybrid: A Python Framework for Hybrid Quantum-classical Computing"},{"key":"ref65","year":"2024","journal-title":"Energy Impact Decomposer Documentation"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2021.3138629"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.3389\/fict.2016.00014"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/3425607"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/3520304.3533986"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/HPEC58863.2023.10363584"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA56546.2023.10071022"}],"event":{"name":"2026 ACM\/IEEE 53rd Annual International Symposium on Computer Architecture (ISCA)","location":"Raleigh, NC, USA","start":{"date-parts":[[2026,6,27]]},"end":{"date-parts":[[2026,7,1]]}},"container-title":["2026 ACM\/IEEE 53rd Annual International Symposium on Computer Architecture (ISCA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11617393\/11617394\/11617414.pdf?arnumber=11617414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T06:01:36Z","timestamp":1785909696000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11617414\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":71,"URL":"https:\/\/doi.org\/10.1109\/isca66397.2026.00165","relation":{},"subject":[],"published":{"date-parts":[[2026,6]]}}}