{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T16:20:32Z","timestamp":1779294032621,"version":"3.51.4"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Emerg. Technol. Comput. Syst."],"published-print":{"date-parts":[[2025,4,30]]},"abstract":"<jats:p>The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime in several instances. In this work, we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover\u2019s algorithm. The Exclusive-Sum-of-Product (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover\u2019s iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open source Qiskit platform and IBM quantum computer.<\/jats:p>","DOI":"10.1145\/3729229","type":"journal-article","created":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T10:42:51Z","timestamp":1744281771000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2300-267X","authenticated-orcid":false,"given":"Abhoy","family":"Kole","sequence":"first","affiliation":[{"name":"Cyber-Physical Systems, German Research Center for Artificial Intelligence, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3556-8785","authenticated-orcid":false,"given":"Mohammed Elkacem","family":"Djeridane","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, University of Bremen, Bremen, Germany and Siemens EDA GmbH, Hamburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6316-9780","authenticated-orcid":false,"given":"Lennart","family":"Weingarten","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1191-998X","authenticated-orcid":false,"given":"Kamalika","family":"Datta","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, University of Bremen, German Research Centre for Artificial Intelligence, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9872-1740","authenticated-orcid":false,"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, University of Bremen, German Research Centre for Artificial Intelligence, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,7,11]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2244643"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.52.3457"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_9"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055105"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11467-022-1249-z"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_4"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1063\/1.4981999"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-012-9121-3"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.93.022311"},{"key":"e_1_3_1_13_2","volume-title":"Quantum Computation and Quantum Information","author":"Nielsen M.","year":"2000","unstructured":"M. Nielsen and I. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20323-8_8"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2019.0161"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48513-9_33"}],"container-title":["ACM Journal on Emerging Technologies in Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T13:16:54Z","timestamp":1752671814000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,30]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4,30]]}},"alternative-id":["10.1145\/3729229"],"URL":"https:\/\/doi.org\/10.1145\/3729229","relation":{},"ISSN":["1550-4832","1550-4840"],"issn-type":[{"value":"1550-4832","type":"print"},{"value":"1550-4840","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,30]]},"assertion":[{"value":"2024-10-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-26","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}