{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:20:15Z","timestamp":1725747615250},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642406263"},{"type":"electronic","value":"9783642406270"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40627-0_33","type":"book-chapter","created":{"date-parts":[[2013,9,7]],"date-time":"2013-09-07T07:11:01Z","timestamp":1378537861000},"page":"415-431","source":"Crossref","is-referenced-by-count":4,"title":["Solving QBF with Free Variables"],"prefix":"10.1007","author":[{"given":"William","family":"Klieber","sequence":"first","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Ans\u00f3tegui, C., Gomes, C.P., Selman, B.: The Achilles\u2019 Heel of QBF. In: AAAI 2005 (2005)"},{"issue":"1","key":"33_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V. Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.-H.R.: Unified QBF certification and its applications. Formal Methods in System Design\u00a041(1), 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-33386-6_29","volume-title":"Automated Technology for Verification and Analysis","author":"B. Becker","year":"2012","unstructured":"Becker, B., Ehlers, R., Lewis, M., Marin, P.: ALLQBF Solving by Computational Learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 370\u2013384. Springer, Heidelberg (2012)"},{"key":"33_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Benedetti, M., Mangassarian, H.: QBF-Based Formal Verification: Experience and Perspectives. In: JSAT (2008)","DOI":"10.3233\/SAT190055"},{"key":"33_CR6","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)"},{"issue":"8","key":"33_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a0100(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"33_CR8","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A. Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A Knowledge Compilation Map. J. Artif. Intell. Res (JAIR)\u00a017, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-24605-3_3","volume-title":"Theory and Applications of Satisfiability Testing","author":"I.P. Gent","year":"2004","unstructured":"Gent, I.P., Giunchiglia, E., Narizzano, M., Rowley, A.G.D., Tacchella, A.: Watched Data Structures for QBF Solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 25\u201336. Springer, Heidelberg (2004)"},{"key":"33_CR11","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by Dependency Sequents. In: FMCAD, pp. 34\u201343. IEEE (2012)"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting QBF Duality on a Circuit Representation. In: AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7548"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11527695_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"J. Huang","year":"2005","unstructured":"Huang, J., Darwiche, A.: Using DPLL for Efficient OBDD Construction. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 157\u2013172. Springer, Heidelberg (2005)"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W. Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A Non-prenex, Non-clausal QBF Solver with Game-State Learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"33_CR15","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":"33_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"33_CR17","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1002\/j.1538-7305.1949.tb03624.x","volume":"28","author":"C.E. Shannon","year":"1949","unstructured":"Shannon, C.E.: The Synthesis of Two Terminal Switching Circuits. Bell System Technical Journal\u00a028, 59\u201398 (1949)","journal-title":"Bell System Technical Journal"},{"key":"33_CR18","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227 (1996)"},{"issue":"2","key":"33_CR19","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. Stallman","year":"1977","unstructured":"Stallman, R.M., Sussman, G.J.: Forward Reasoning and Dependency-Directed Backtracking in a System for Computer-Aided Circuit Analysis. Artif. Intell.\u00a09(2), 135\u2013196 (1977)","journal-title":"Artif. Intell."},{"issue":"115-125","key":"33_CR20","first-page":"10","volume":"2","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Wille, R., Fey, G., Drechsler, R.: Building free binary decision diagrams using SAT solvers. Facta Universitatis-series: Electronics and Energetics (2007)","DOI":"10.2298\/FUEE0703381W"},{"key":"33_CR22","unstructured":"Zhang, L.: Solving QBF by Combining Conjunctive and Disjunctive Normal Forms. In: AAAI 2006 (2006)"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean Satisfiability Solver. In: ICCAD 2002 (2002)","DOI":"10.1145\/774572.774637"},{"key":"33_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40627-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,4]],"date-time":"2023-07-04T11:09:09Z","timestamp":1688468949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40627-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406263","9783642406270"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40627-0_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}