{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:40:21Z","timestamp":1729676421453,"version":"3.28.0"},"reference-count":26,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1109\/date.2010.5457088","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T18:16:33Z","timestamp":1361297793000},"page":"1695-1700","source":"Crossref","is-referenced-by-count":0,"title":["Leveraging dominators for preprocessing QBF"],"prefix":"10.1109","author":[{"given":"H","family":"Mangassarian","sequence":"first","affiliation":[]},{"family":"Bao Le","sequence":"additional","affiliation":[]},{"given":"A","family":"Goultiaeva","sequence":"additional","affiliation":[]},{"given":"A","family":"Veneris","sequence":"additional","affiliation":[]},{"given":"F","family":"Bacchus","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_22"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_34"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_38"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2004.1268858"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2006.229206"},{"key":"ref15","article-title":"Solving QBF with combined conjunctive and disjunctive normal forms","author":"zhang","year":"2006","journal-title":"National Conference on Artificial Intelligence (AAAI)"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_35"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_19"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9055-y"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1145\/37888.37963","article-title":"a topological search algorithm for atpg","author":"kirkland","year":"1987","journal-title":"24th ACM\/IEEE Design Automation Conference"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_32"},{"key":"ref3","first-page":"239","article-title":"On the complexity of power estimation problems","author":"freitas","year":"2000","journal-title":"Int'l Workshop on Logic and Synthesis"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397272"},{"key":"ref5","first-page":"1","article-title":"Compressing BMC encodings with QBF","author":"jussila","year":"2006","journal-title":"Proc Int'l Workshop Bounded Model Checking"},{"key":"ref8","first-page":"238","article-title":"Resolve and expand","author":"biere","year":"2004","journal-title":"Int'l Conf on Theory and Applications of Satisfiability Testing"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","article-title":"sKizzo: a suite to evaluate and certify QBFs","author":"benedetti","year":"2005","journal-title":"Int'l Conf on Automated Deduction"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","article-title":"Qube: A system for deciding quantified boolean formulas satisfiability","author":"giunchiglia","year":"2001","journal-title":"Proceedings of the First International Joint Conference on Automated Reasoning"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/43.273754"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.888264"},{"key":"ref21","first-page":"514","article-title":"Preprocessing QBF","author":"samulowitz","year":"2006","journal-title":"3 Internat Conf on Principles and Practice of Constraint Programming"},{"key":"ref24","first-page":"115","article-title":"On the complexity of derivations in the propositional calculus","author":"tseitin","year":"1968"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An opensource tool for symbolic model checking","author":"cimatti","year":"2002","journal-title":"Computer Aided Verification"},{"key":"ref26","first-page":"869","article-title":"Finding dominators revisited: extended abstract","author":"georgiadis","year":"2004","journal-title":"SODA"},{"key":"ref25","article-title":"Graph-theoretic constructs for program flow analysis","volume":"3923","author":"allen","year":"1972","journal-title":"Technical Report RC"}],"event":{"name":"2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)","start":{"date-parts":[[2010,3,8]]},"location":"Dresden","end":{"date-parts":[[2010,3,12]]}},"container-title":["2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5450668\/5456897\/05457088.pdf?arnumber=5457088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,9]],"date-time":"2019-07-09T22:18:41Z","timestamp":1562710721000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5457088\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/date.2010.5457088","relation":{},"subject":[],"published":{"date-parts":[[2010,3]]}}}