{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:00:09Z","timestamp":1725796809687},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_18","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:43:21Z","timestamp":1404279801000},"page":"227-242","source":"Crossref","is-referenced-by-count":5,"title":["Dominant Controllability Check Using QBF-Solver and Netlist Optimizer"],"prefix":"10.1007","author":[{"given":"Tamir","family":"Heyman","sequence":"first","affiliation":[]},{"given":"Dan","family":"Smith","sequence":"additional","affiliation":[]},{"given":"Yogesh","family":"Mahajan","sequence":"additional","affiliation":[]},{"given":"Lance","family":"Leong","sequence":"additional","affiliation":[]},{"given":"Husam","family":"Abu-Haimed","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"QDIMACS Standard Version 1.1 (released on December 21, 2005)"},{"key":"18_CR2","unstructured":"Abramovici, M., Breuer, M.A., Friedman, A.D.: Digital Systems Testing and Testable Design. Computer Science Press (1990)"},{"key":"18_CR3","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked Clause Elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R. Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated Testing and Debugging of SAT and QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 44\u201357. Springer, Heidelberg (2010)"},{"issue":"4","key":"18_CR5","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1147\/rd.254.0272","volume":"25","author":"J.A. Darringer","year":"1981","unstructured":"Darringer, J.A., Joyner Jr., W.H., Berman, C.L., Trevillyan, L.: Logic Synthesis Through Local Transformations. IBM Journal of Research and Development\u00a025(4), 272\u2013280 (1981)","journal-title":"IBM Journal of Research and Development"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-14186-7_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"E. Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An Effective Preprocessor for QBFs based on Equivalence Reasoning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 85\u201398. Springer, Heidelberg (2010)"},{"key":"18_CR7","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI 2011, vol.\u00a01, pp. 546\u2013553. AAAI Press (2011)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: On QBF Proofs and Preprocessing. CoRR abs\/1310.2491 (2013)","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-14186-7_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing Solutions After Blocked Clause Elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 340\u2013345. Springer, Heidelberg (2010)"},{"key":"18_CR10","unstructured":"Kuehlmann, A.: Dynamic Transition Relation Simplification for Bounded Property Checking. In: ICCAD, pp. 50\u201357. IEEE Computer Society \/ ACM (2004)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-based QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 158\u2013171. Springer, Heidelberg (2010)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Marin, P., Miller, C., Lewis, M., Becker, B.: Verification of Partial Designs Using Incremental QBF Solving. In: Design, Automation Test in Europe Conference Exhibition DATE 2012, pp. 623\u2013628 (March 2012)","DOI":"10.1109\/DATE.2012.6176547"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to Combinational Equivalence Checking. In: ICCAD, pp. 836\u2013843 (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based Certificate Extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 430\u2013435. Springer, Heidelberg (2012)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/11889205_37","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 514\u2013529. Springer, Heidelberg (2006)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Validating the Result of a Quantified Boolean Formula (QBF) Solver: Theory and Practice. In: Tang, T. (ed.) ASP-DAC, pp. 1047\u20131051. ACM Press (2005)","DOI":"10.1145\/1120725.1120821"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:49:17Z","timestamp":1558306157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}