{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:29:09Z","timestamp":1725586149040},"reference-count":18,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,11]]},"DOI":"10.1109\/iccad.2010.5654209","type":"proceedings-article","created":{"date-parts":[[2010,12,10]],"date-time":"2010-12-10T22:29:13Z","timestamp":1292020153000},"page":"602-609","source":"Crossref","is-referenced-by-count":5,"title":["Reduction of interpolants for logic synthesis"],"prefix":"10.1109","author":[{"given":"John D.","family":"Backes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc D.","family":"Riedel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"year":"1968","author":"tseitin","journal-title":"On the Complexity of Derivations in Prepositional Calculus","key":"17"},{"key":"18","first-page":"10880","article-title":"Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications","author":"zhang","year":"2003","journal-title":"Design Automation and Test in Europe"},{"doi-asserted-by":"publisher","key":"15","DOI":"10.2307\/2275583"},{"year":"0","author":"so?rensson","journal-title":"Minisat V1 13 - A SAT Solver with Conflict-clause Minimization","key":"16"},{"year":"2007","author":"mishchenko","journal-title":"ABC A System for Sequential Synthesis and Verification","key":"13"},{"doi-asserted-by":"publisher","key":"14","DOI":"10.1109\/DAC.2001.156196"},{"key":"11","first-page":"1","article-title":"Interpolation and. SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"International Conference on Computer Aided Verification"},{"doi-asserted-by":"publisher","key":"12","DOI":"10.1145\/1146909.1147048"},{"doi-asserted-by":"publisher","key":"3","DOI":"10.1109\/FMCAD.2008.ECP.6"},{"key":"2","first-page":"24","article-title":"Riedel. The synthesis of cyclic dependencies with Craig interpolation","author":"backes","year":"2009","journal-title":"International Workshop on Logic and Synthesis"},{"key":"1","first-page":"143","article-title":"Riedel. The analysis of cyclic circuits with Boolean satisfiability","author":"backes","year":"2008","journal-title":"International Conference on Computer-Aided Design"},{"key":"10","first-page":"227","article-title":"Scalable exploration of functional dependency by interpolation and incremental SAT solving","author":"lee","year":"2007","journal-title":"International Conference on Computer-Aided Design"},{"year":"0","journal-title":"Benchmarks from the 1993 Int'l Workshop on Logic Synthesis","key":"7"},{"key":"6","first-page":"502","article-title":"An extensible sat-solver","author":"ee?n","year":"2003","journal-title":"SAT Volume 2919 of Lecture Notes in Computer Science"},{"key":"5","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/11499107_4","article-title":"A clause-based heuristic for SAT solvers. In","author":"dershowitz","year":"2005","journal-title":"Proc Int'l Conf Theory and Applications of Satisfiability Testing (SAT)"},{"doi-asserted-by":"publisher","key":"4","DOI":"10.2307\/2963593"},{"doi-asserted-by":"publisher","key":"9","DOI":"10.1109\/43.108614"},{"doi-asserted-by":"publisher","key":"8","DOI":"10.1007\/s10703-008-0051-z"}],"event":{"name":"2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)","start":{"date-parts":[[2010,11,7]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2010,11,11]]}},"container-title":["2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5638200\/5648785\/05654209.pdf?arnumber=5654209","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T13:08:11Z","timestamp":1497877691000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5654209\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1109\/iccad.2010.5654209","relation":{},"subject":[],"published":{"date-parts":[[2010,11]]}}}