{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:09:20Z","timestamp":1761620960988},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441205"},{"type":"electronic","value":"9783540461357"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46135-3_14","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T01:59:47Z","timestamp":1179194387000},"page":"200-215","source":"Crossref","is-referenced-by-count":60,"title":["Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation"],"prefix":"10.1007","author":[{"given":"Lintao","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"J. Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323\u2013352, 1999","journal-title":"Journal of Artificial Intelligence Research"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"M. Sheeran, S. Singh, G. St\u00e4lmark, Checking Safety Properties Using Induction and a SAT-Solver, in Proceedings of FMCAD, 2000","DOI":"10.1007\/3-540-40922-X_8"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs, In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 1999","DOI":"10.21236\/ADA360973"},{"issue":"1","key":"14_CR4","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"H. Kleine-B\u00fcning, M. Karpinski and A. Fl\u00f6gel. Resolution for quantified Boolean formulas. In Information and Computation, 117(1):12\u201318, 1995","journal-title":"In Information and Computation"},{"key":"14_CR5","unstructured":"D. A. Plaisted, A. Biere and Y. Zhu. A Satisfiability Procedure for Quantified Boolean Formulae, To appear in, Discrete Applied Mathematics"},{"key":"14_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. In Communications of the ACM, 5:394\u2013397, 1962","journal-title":"Communications of the ACM"},{"key":"14_CR7","unstructured":"M. Cadoli, M. Schaerf, A. Giovanardi and M. Giovanardi. An algorithm to evaluate quantified Boolean formulae and its experimental evaluation, in Highlights of Satisfiability Research in the Year 2000, IOS Press, 2000"},{"key":"14_CR8","unstructured":"J. Rintanen, Improvements to the Evaluation of Quantified Boolean Formulae, in Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 1999"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"J. Rintanen, Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae, in International Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2001","DOI":"10.1007\/3-540-45653-8_25"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano and A. Tacchella,. Qube: a system for Deciding Quantified Boolean Formulas Satisfiability,. In Proc. of International Joint Conf. on Automated Reasoning (IJCAR), 2001","DOI":"10.1007\/3-540-45744-5_27"},{"key":"14_CR11","unstructured":"E. Giunchiglia, M. Narizzano and A. Tacchella. Backjumping for Quantified Boolean Logic Satisfiability. In Proc. of International Joint Conf. on Artificial Intelligence (IJCAI), 2001"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"Jo\u00e3o P. Marques-Silva and Karem A. Sakallah, \u201cGRASP: A Search Algorithm for Prepositional Satisfiability, In IEEE Transactions on Computers, vol. 48, 506\u2013521, 1999","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"R. Bayard and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances, in Proc. of the 14th Nat. (US) Conf. on Artificial Intelligence (AAAI), 1997","DOI":"10.1007\/3-540-61551-2_65"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover, In Proc. of the International Conference on Automated Deduction, 1997","DOI":"10.1007\/3-540-63104-6_28"},{"key":"14_CR15","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering an efficient SAT Solver, In Proceedings of the Design Automation Conference, 2001"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"L. Zhang, C. Madigan, M. Moskewicz, S. Malik, Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, in Proc. of International Conference on Computer Aided Design (ICCAD), 2001","DOI":"10.1145\/774572.774637"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"L. Zhang and S. Malik, Conflict Driven Learning in a Quantified Boolean Satisfiability Solver, Accepted for publication, International Conference on Computer Aided Design (ICCAD), 2002","DOI":"10.1145\/774572.774637"},{"key":"14_CR18","unstructured":"G. Hachtel and F. Somenzi, Logic Sysntheiss and Verification Algorithms: Kluwer Academic Publishers, 1996"},{"key":"14_CR19","unstructured":"J. Rintanen\u2019s benchmarks are at http:\/\/ww.informatik.uni-freiburg.de\/~rintanen\/qbfhtml"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"R. Letz, Lemma, Model Caching in Decision Procedures for Quantified Boolean Formulas, in Proc. International Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, 2002","DOI":"10.1007\/3-540-45616-3_12"},{"key":"14_CR21","unstructured":"E. Giunchiglia, M. Narizzano and A. Tacchella, Learning for Quantified Boolean Logic Satisfiability, in Proc. of the 18th Nat. (US) Conf. on Artificial Intelligence (AAAI), 2002"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46135-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:25:37Z","timestamp":1556396737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46135-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441205","9783540461357"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46135-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}