{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T05:30:39Z","timestamp":1736487039570,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_34","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"368-381","source":"Crossref","is-referenced-by-count":2,"title":["Solving Quantified Boolean Formulas with Circuit Observability Don\u2019t Cares"],"prefix":"10.1007","author":[{"given":"Daijue","family":"Tang","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research\u00a010, 323\u2013352 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmark, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 126\u2013142. Springer, Heidelberg (2000)"},{"unstructured":"Gent, I.P., Rowley, A.G.D.: Encoding connect-4 using quantified boolean formulae. In: Modelling and Reformulating CSP, pp. 78\u201393 (2003)","key":"34_CR4"},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic computational techniques for solving games. International Journal on Software Tools for Technology Transfer (STTT), 118\u2013128 (2005)","key":"34_CR5","DOI":"10.1007\/s10009-004-0179-0"},{"unstructured":"Ans\u00f3tegui, C., Gomes, C.P., Selman, B.: The achilles\u2019 heel of QBF. In: Proceedings of the 21th National (US) Conference on Artificial Intelligence (AAAI), pp. 275\u2013281 (2005)","key":"34_CR6"},{"doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of the Design Automation Conference (DAC) (2001)","key":"34_CR7","DOI":"10.1145\/378239.378471"},{"doi-asserted-by":"crossref","unstructured":"Katz, J., Hanna, Z., Dershowitz, N.: Space-efficient bounded model checking. In: Proceedings of the IEEE\/ACM Design, Automation, and Test in Europe (DATE), pp. 686\u2013687 (2005)","key":"34_CR8","DOI":"10.1109\/DATE.2005.276"},{"doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1968)","key":"34_CR9","DOI":"10.1007\/978-1-4899-5327-8_25"},{"doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: Proceedings of the Design Automation Conference (DAC), pp. 747\u2013750 (2002)","key":"34_CR10","DOI":"10.1145\/513918.514105"},{"unstructured":"Lu, F., Wang, L., Cheng, K., Huang, R.: A circuit SAT solver with signal correlation guided learning. In: Design, Automation, and Test in Europe (DATE 2003), Munich, Germany, pp. 892\u2013897 (2003)","key":"34_CR11"},{"doi-asserted-by":"crossref","unstructured":"Gupta, A., Gupta, A., Yang, Z., Ashar, P.: Dynamic detection and removal of inactive clauses in SAT with application in image computation. In: Design Automation Conference, pp. 536\u2013541 (2001)","key":"34_CR12","DOI":"10.1145\/378239.379018"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.N. Velev","year":"2005","unstructured":"Velev, M.N.: Encoding global unobservability for efficient translation to sat. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Comparison of schemes for encoding unobservability in translation to sat. In: Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 1056\u20131059 (2005)","key":"34_CR14","DOI":"10.1145\/1120725.1120823"},{"doi-asserted-by":"crossref","unstructured":"Safarpour, S., Veneris, A.G., Drechsler, R., Lee, J.: Managing don\u2019t cares in boolean satisfiability. In: Proceedings of the IEEE\/ACM Design, Automation, and Test in Europe (DATE), pp. 260\u2013265 (2004)","key":"34_CR15","DOI":"10.1109\/DATE.2004.1268858"},{"unstructured":"Fu, Z., Yu, Y., Malik, S.: Considering circuit observability don\u2019t cares in CNF satisfiability. In: Proceedings of the IEEE\/ACM Design, Automation, and Test in Europe (DATE), pp. 1108\u20131113 (2005)","key":"34_CR16"},{"key":"34_CR17","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1109\/43.3211","volume":"7","author":"K. Bartlett","year":"1988","unstructured":"Bartlett, K., Brayton, R.K., Hachtel, G.D., Jacoby, R.M., Morrison, C.R., Rudell, R.L., Sangiovanni-Vincentelli, A., Wang, A.R.: Multi-level logic minimization using implicit don\u2019t cares. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a07, 723\u2013740 (1988)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference (DAC) (2001)","key":"34_CR18","DOI":"10.1145\/378239.379017"},{"key":"34_CR19","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46027-6","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, Springer, Heidelberg (2002)"},{"key":"34_CR21","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, Springer, Heidelberg (2002)"},{"unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified Boolean logic satisfiability. In: Proceedings of the 18th National (US) Conference on Artificial Intelligence (AAAI) (2002)","key":"34_CR22"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD) (2001)","key":"34_CR23","DOI":"10.1145\/774572.774637"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD) (2002)","key":"34_CR24","DOI":"10.1145\/774572.774637"},{"unstructured":"Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: The Design Automation Conference (DAC) (submitted, 2006)","key":"34_CR25"},{"doi-asserted-by":"crossref","unstructured":"Mneimneh, M., Sakallah, K.: Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In: Sixth International Conference on Theory and Application of Satisfiability Testing (2003)","key":"34_CR26","DOI":"10.1007\/978-3-540-24605-3_31"},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11527695_23","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Tang","year":"2005","unstructured":"Tang, D., Yu, Y., Ranjan, D., Malik, S.: Analysis of DPLL Based Search Algorithms for Satisfiability of Quantified Boolean Formulas arising from Circuits. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 292\u2013305. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T23:23:34Z","timestamp":1736465014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11814948_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}