{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T15:22:44Z","timestamp":1725463364903},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1109\/date.2011.5763033","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T22:45:16Z","timestamp":1361313916000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["Clause simplification through dominator analysis"],"prefix":"10.1109","author":[{"family":"Hyojung Han","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Hoonsang Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2049135"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref14","first-page":"1481","article-title":"A new clause learning scheme for efficient unsatisfiability proofs","author":"pipatsrisawat","year":"2008","journal-title":"AAAI'08 Proceedings of the 23rd National Conference on Artificial Intelligence"},{"year":"0","key":"ref15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1460299.1460314"},{"year":"0","key":"ref17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_23"},{"journal-title":"MiniSat v1 13 - a SAT solver with conflict-clause minimization SAT Competition 2005 - Solver Description","year":"2005","author":"s\u00f6rensson","key":"ref19"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","article-title":"Effective preprocessing in SAT through variable and clause elimination","author":"e\u00e9n","year":"2005","journal-title":"Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005)"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"ref6","first-page":"502","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278628"},{"key":"ref7","article-title":"CirCUs 2.0 - SAT competition 2009 edition","author":"han","year":"2009","journal-title":"Solver Description SAT Competition 2009"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref1","article-title":"P{re, i}coSAT@sc'09. SAT Competition 2009","author":"biere","year":"2009","journal-title":"GAMS Solver Description"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_21"},{"year":"0","key":"ref20"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2006.229206"}],"event":{"name":"2011 Design, Automation & Test in Europe","start":{"date-parts":[[2011,3,14]]},"location":"Grenoble","end":{"date-parts":[[2011,3,18]]}},"container-title":["2011 Design, Automation & Test in Europe"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5754459\/5762992\/05763033.pdf?arnumber=5763033","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,9]],"date-time":"2019-07-09T22:43:56Z","timestamp":1562712236000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5763033\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/date.2011.5763033","relation":{},"subject":[],"published":{"date-parts":[[2011,3]]}}}