{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T06:23:36Z","timestamp":1790144616499,"version":"4.0.1"},"reference-count":38,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,3]]},"DOI":"10.23919\/date.2019.8715061","type":"proceedings-article","created":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:29:07Z","timestamp":1558042147000},"page":"468-473","source":"Crossref","is-referenced-by-count":11,"title":["Bosphorus: Bridging ANF and CNF Solvers"],"prefix":"10.23919","author":[{"given":"Davin","family":"Choo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mate","family":"Soos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kian Ming A.","family":"Chai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref38","article-title":"Bitcoin: A peer-to-peer electronic cash system","author":"nakamoto","year":"2008","journal-title":"Tech Rep"},{"key":"ref33","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability Volume 185 Frontiers in Artificial Intelligence and Applications"},{"key":"ref32","article-title":"CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017","author":"biere","year":"2017","journal-title":"SAT Competition 2017 &#x2013; Solver and Benchmark Descriptions"},{"key":"ref31","author":"balyo","year":"2017","journal-title":"SAT Competition 2017 &#x2013; Solver and Benchmark Descriptions"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/TCE.1953.6371932"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.5220\/0005064903990404"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747946"},{"key":"ref35","year":"2017","journal-title":"SageMath the Sage Mathematics Software System (Version 8 1)"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_10"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36178-2_17"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77272-9_10"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34047-5_18"},{"key":"ref13","article-title":"A new incremental algorithm for computing Gr&#x00F6;bner bases","author":"gao","year":"2010","journal-title":"Proceedings of ISSAC"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0183-4"},{"key":"ref15","first-page":"220","article-title":"GRASP - a new search algorithm for satisfiability","author":"silva","year":"1996","journal-title":"Proceedings of CAV ser ICCAD &#x2019;96"},{"key":"ref16","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"Proc SAT"},{"key":"ref17","first-page":"61","article-title":"Effective preprocessing in SAT through variable and clause elimination","author":"e\u00e9n","year":"2005","journal-title":"Proc SAT"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref19","article-title":"Constrained sampling and counting: Universal hashing meets SAT solving","author":"meel","year":"2016","journal-title":"Beyond NP AAAI Workshops"},{"key":"ref28","article-title":"The CryptoMiniSat 5 set of solvers at SAT competition 2016","author":"soos","year":"2016","journal-title":"SAT Competition 2016 &#x2013; Solver and Benchmark Descriptions"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00005-5"},{"key":"ref27","article-title":"Efficient dense Gaus-sian elimination over the finite field with two elements","author":"albrecht","year":"2011"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2005.09.007"},{"key":"ref6","article-title":"M4GB: an efficient Gr&#x00F6;bner-basis algorithm","author":"makarim","year":"2017","journal-title":"Proceedings of ISSAC"},{"key":"ref29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-2821-6","author":"brayton","year":"1984","journal-title":"Logic Minimization Algorithms for VLSI Synthesis"},{"key":"ref5","article-title":"A new efficient algorithm for computing Gr&#x00F6;bner bases without reduction to zero (F5)","author":"faug\u00e8re","year":"2002","journal-title":"Proceedings of ISSAC"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0125"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15582-6_17"},{"key":"ref2","article-title":"Secure Hash Standard (SHS)","year":"2015","journal-title":"FIPS PUB 180&#x2013;4"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45539-6_27"},{"key":"ref1","article-title":"Advanced Encryption Standard (AES)","year":"2001","journal-title":"FIPS PUB 197"},{"key":"ref20","author":"meel","year":"2017","journal-title":"Constrained Counting and Sampling Bridging the gap between Theory and Practice"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63104-6_28"},{"key":"ref24","article-title":"A Gr&#x00F6;bner basis approach to CNF-formulae preprocessing","author":"condrat","year":"2007","journal-title":"Proc of TACAS"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90074-8"},{"key":"ref26","author":"albrecht","year":"2012","journal-title":"The M4RI Library &#x2013; Version 20121224 The M4RI Team"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.02.017"}],"event":{"name":"2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)","location":"Florence, Italy","start":{"date-parts":[[2019,3,25]]},"end":{"date-parts":[[2019,3,29]]}},"container-title":["2019 Design, Automation &amp; Test in Europe Conference &amp; Exhibition (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8704855\/8714721\/08715061.pdf?arnumber=8715061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T23:50:36Z","timestamp":1559605836000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8715061\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3]]},"references-count":38,"URL":"https:\/\/doi.org\/10.23919\/date.2019.8715061","relation":{},"subject":[],"published":{"date-parts":[[2019,3]]}}}