{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T04:09:03Z","timestamp":1746590943891,"version":"3.40.5"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319133379"},{"type":"electronic","value":"9783319133386"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13338-6_12","type":"book-chapter","created":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T03:35:45Z","timestamp":1414985745000},"page":"148-164","source":"Crossref","is-referenced-by-count":4,"title":["Partial Quantifier Elimination"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","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, vol.\u00a06803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"issue":"8","key":"12_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-44798-9_24","volume-title":"Correct Hardware Design and Verification Methods","author":"P. Chauhan","year":"2001","unstructured":"Chauhan, P., Clarke, E., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 293\u2013309. Springer, Heidelberg (2001)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","first-page":"93","volume-title":"HVC 2010","author":"E. Goldberg","year":"2010","unstructured":"Goldberg, E., Manolios, P.: SAT-solving based on boundary point elimination. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol.\u00a06504, pp. 93\u2013111. Springer, Heidelberg (2010)"},{"key":"12_CR6","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: FMCAD 2012, pp. 34\u201344 (2012)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: FMCAD 2013, pp. 85\u201392 (2013)","DOI":"10.1109\/FMCAD.2013.6679395"},{"key":"12_CR8","unstructured":"Goldberg, E., Manolios, P.: Bug hunting by computing range reduction. Technical Report arXiv:1408.7039 [cs.LO] (2014)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Partial quantifier elimination. Technical Report arXiv:1407.4835 [cs.LO] (2014)","DOI":"10.1007\/978-3-319-13338-6_12"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-662-44199-2_45","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"E. Goldberg","year":"2014","unstructured":"Goldberg, E., Manolios, P.: Software for quantifier elimination in propositional logic. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol.\u00a08592, pp. 291\u2013294. Springer, Heidelberg (2014)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: DAC 2005, pp. 750\u2013753 (2005)","DOI":"10.1145\/1065579.1065775"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-02658-4_30","volume-title":"Computer Aided Verification","author":"J.-H.R. Jiang","year":"2009","unstructured":"Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 383\u2013397. Springer, Heidelberg (2009)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-40627-0_33","volume-title":"Principles and Practice of Constraint Programming","author":"W. Klieber","year":"2013","unstructured":"Klieber, W., Janota, M., Marques-Silva, J., Clarke, E.: Solving QBF with free variables. In: Schulte, C. (ed.) CP 2013. LNCS, vol.\u00a08124, pp. 415\u2013431. Springer, Heidelberg (2013)"},{"issue":"1-2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-sat decision and worst-case analysis. Theor. Comput. Sci.\u00a0223(1-2), 1\u201372 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A., Ashar, P.: Efficient sat-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD 2004, pp. 510\u2013517 (2004)","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"12_CR18","unstructured":"HWMCC-2010 benchmarks, http:\/\/fmv.jku.at\/hwmcc10\/benchmarks.html"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13338-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T04:21:20Z","timestamp":1746505280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13338-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319133379","9783319133386"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13338-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}