{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T14:52:17Z","timestamp":1761663137040},"reference-count":18,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1109\/date.2009.5090918","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T18:16:39Z","timestamp":1361297799000},"page":"1590-1595","source":"Crossref","is-referenced-by-count":12,"title":["Faster SAT solving with better CNF generation"],"prefix":"10.1109","author":[{"given":"B.","family":"Chambers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Manolios","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Vroon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"17","article-title":"on the complexity of derivation in propositional calculus","author":"tseitin","year":"1968","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337587"},{"article-title":"rsat 2.0: sat solver description","year":"0","author":"pipatsrisawat","key":"15"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_35"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_3"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"12","doi-asserted-by":"crossref","DOI":"10.1109\/DAC.1997.597155","article-title":"equivalence checking using cuts and heaps","author":"kuehlmann","year":"1997","journal-title":"Design Automation Conference"},{"journal-title":"ABC A System for Sequential Synthesis and Verification http","year":"0","key":"3"},{"key":"2","article-title":"symbolic reachability analysis based on sat-solvers","author":"abdulla","year":"2000","journal-title":"TACAS"},{"year":"2008","author":"sat-race","key":"1"},{"year":"0","key":"10"},{"key":"7","article-title":"an optimality result for clause form translation","author":"de la tour","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"6","article-title":"local two-level and-inverter graph minimization without blowup","author":"brummayer","year":"2006","journal-title":"MEMICS"},{"journal-title":"Hardware Model Checking Competition 2008","year":"0","author":"biere","key":"5"},{"journal-title":"AIGER Format and Toolbox","year":"0","author":"biere","key":"4"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"8","article-title":"a fast linear-arithmetic solver for dpll(t)","author":"dutertre","year":"0","journal-title":"Proc CAV 2006"}],"event":{"name":"2009 Design, Automation & Test in Europe Conference & Exhibition (DATE'09)","start":{"date-parts":[[2009,4,20]]},"location":"Nice","end":{"date-parts":[[2009,4,24]]}},"container-title":["2009 Design, Automation & Test in Europe Conference & Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4926138\/5090609\/05090918.pdf?arnumber=5090918","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T15:12:13Z","timestamp":1602688333000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/5090918"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1109\/date.2009.5090918","relation":{},"subject":[],"published":{"date-parts":[[2009,4]]}}}