{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T08:02:31Z","timestamp":1791964951028,"version":"4.3.4"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987602","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"107-114","source":"Crossref","is-referenced-by-count":27,"title":["Efficient extraction of Skolem functions from QRAT proofs"],"prefix":"10.1109","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"22","first-page":"2013","article-title":"Lingeling, plingeling and treengeling entering the sat competition 2013","author":"biere","year":"2013","journal-title":"Sat competition"},{"key":"17","article-title":"Solving qbf with counterexample guided refinement","volume":"7317","author":"janota","year":"2012","journal-title":"SATNAC 2012"},{"key":"23","first-page":"41","article-title":"Covered clause elimination","volume":"13","author":"heule","year":"2013","journal-title":"LPAR-17-short Ser EPiC Series"},{"key":"18","first-page":"1","article-title":"Partial witnesses from preprocessed quantified boolean formulas","author":"k\ufffdnighofer","year":"2014","journal-title":"DATE IEEE"},{"key":"24","year":"0","journal-title":"ABC A System for Sequential Synthesis and Verification"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_8"},{"key":"13","first-page":"357","article-title":"Clause elimination procedures for cnf formulas","volume":"6397","author":"heule","year":"2010","journal-title":"LPAR-16 Ser LNCS"},{"key":"14","first-page":"369","article-title":"Skizzo: A suite to evaluate and certify qbfs","volume":"3632","author":"benedetti","year":"2005","journal-title":"CADE-20 Ser LNCS"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_7"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"3","article-title":"Theory of quantified boolean formulas","author":"kleine b\ufffdning","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"20","first-page":"355","article-title":"Inprocessing rules","volume":"7364","author":"j\ufffdrvisalo","year":"2012","journal-title":"IJCAR"},{"key":"2","first-page":"133","article-title":"Qbf-based formal verification: Experience and perspectives","volume":"5","author":"benedetti","year":"2008","journal-title":"JSAT"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_12"},{"key":"6","first-page":"761","article-title":"Reasoning with quantified boolean formulas","volume":"185","author":"giunchiglia","year":"2009","journal-title":"Handbook of Satisfiability IOS Press"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9067-0"},{"key":"4","first-page":"275","article-title":"The achilles' heel of qbf","author":"ans\ufffdtegui","year":"2005","journal-title":"AAAI"},{"key":"9","first-page":"59","article-title":"Resolve and expand","volume":"3542","author":"biere","year":"2004","journal-title":"SAT (Selected Papers) Ser LNCS"},{"key":"8","first-page":"546","article-title":"A uniform approach for generating proofs and strategies for both true and false qbf formulas","author":"goultiaeva","year":"2011","journal-title":"IJCAI IJCAI"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,21]]},"end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987602.pdf?arnumber=6987602","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:51:12Z","timestamp":1490316672000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987602\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987602","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}