{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T06:10:14Z","timestamp":1747894214393,"version":"3.41.0"},"reference-count":51,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"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,3,31]]},"DOI":"10.23919\/date64628.2025.10993248","type":"proceedings-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T17:36:35Z","timestamp":1747848995000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["High-Throughput SAT Sampling"],"prefix":"10.23919","author":[{"given":"Arash","family":"Ardakani","sequence":"first","affiliation":[{"name":"University of California,Berkeley"}]},{"given":"Minwoo","family":"Kang","sequence":"additional","affiliation":[{"name":"University of California,Berkeley"}]},{"given":"Kevin","family":"He","sequence":"additional","affiliation":[{"name":"University of California,Berkeley"}]},{"given":"Qijing","family":"Huang","sequence":"additional","affiliation":[{"name":"NVIDIA"}]},{"given":"John","family":"Wawrzynek","sequence":"additional","affiliation":[{"name":"University of California,Berkeley"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100071"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390662"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"ref9","first-page":"209","article-title":"Klee: unassisted and automatic generation of high-coverage tests for complex systems programs","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, ser. OSDI\u201908. USA: USENIX","author":"Cadar","year":"2008"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref12","article-title":"jfuzz: A concolic whitebox fuzzer for java","author":"Jayaraman","year":"2009","journal-title":"NASA Formal Methods"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.3571576"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CSCWD.2009.4968035"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_60"},{"key":"ref21","first-page":"1720","article-title":"Constraint-based random stimuli generation for hardware verification","volume-title":"Proceedings of the 18th Conference on Innovative Applications of Artificial Intelligence - Volume 2, ser. IAAI\u2019 06","author":"Naveh","year":"2006"},{"volume":"185","volume-title":"Handbook of Satisfiability, ser. Frontiers in Artificial Intelligence and Applications","year":"2009","key":"ref22"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213018400018"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.3233\/faia200987"},{"volume-title":"Model counting and uniform sampling instances","year":"2020","author":"Meel","key":"ref28"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9295-4"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/026\/25"},{"key":"ref33","first-page":"1","article-title":"Does Looking Inside a Circuit Help?","volume-title":"42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)","volume":"83","author":"Impagliazzo","year":"2017"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_34"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_22"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_31"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3649329.3663505"},{"key":"ref38","first-page":"663","article-title":"Restoring circuit structure from sat instances","volume-title":"proceedings of international workshop on Logic and synthesis. Citeseer","author":"Roy","year":"2004"},{"key":"ref39","first-page":"e103","article-title":"Sympy: symbolic computing in python","volume-title":"Peer J Computer Science,","volume":"3","author":"Meurer","year":"2017"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2068716.2068720"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2017.2654298"},{"key":"ref44","article-title":"The synthesis of xnor recurrent neural networks with stochastic logic","volume-title":"Advances in Neural Information Processing Systems","volume":"32","author":"Ardakani","year":"2019"},{"key":"ref45","article-title":"On scalable testing of samplers","volume-title":"Advances in Neural Information Processing Systems (NeurIPS)","author":"Pote","year":"2022"},{"key":"ref46","article-title":"Parallelization of sat algorithms on gpus","author":"Costa","year":"2013","journal-title":"Technical report, INESC-ID, Technical University of Lisbon, Tech. Rep."},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_8"},{"volume-title":"Matsat: a matrix-based differentiable sat solver","year":"2021","author":"Sato","key":"ref48"},{"key":"ref49","article-title":"Learning to solve circuit-sat: An unsupervised differentiable approach","volume-title":"International Conference on Learning Representations","author":"Amizadeh","year":"2018"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/3658617.3697760"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2007.81"}],"event":{"name":"2025 Design, Automation & Test in Europe Conference (DATE)","start":{"date-parts":[[2025,3,31]]},"location":"Lyon, France","end":{"date-parts":[[2025,4,2]]}},"container-title":["2025 Design, Automation & Test in Europe Conference (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10992638\/10992588\/10993248.pdf?arnumber=10993248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T05:33:37Z","timestamp":1747892017000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10993248\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":51,"URL":"https:\/\/doi.org\/10.23919\/date64628.2025.10993248","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]}}}