{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T04:24:01Z","timestamp":1743049441006,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642296994"},{"type":"electronic","value":"9783642297007"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29700-7_24","type":"book-chapter","created":{"date-parts":[[2012,4,28]],"date-time":"2012-04-28T12:25:56Z","timestamp":1335615956000},"page":"259-268","source":"Crossref","is-referenced-by-count":0,"title":["Solving Difficult SAT Problems by Using OBDDs and Greedy Clique Decomposition"],"prefix":"10.1007","author":[{"given":"Yanyan","family":"Xu","sequence":"first","affiliation":[]},{"given":"Wei","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Kaile","family":"Su","sequence":"additional","affiliation":[]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Stephen, A.: Cook. The Complexity of Theorem-Proving Procedures. In: STOC, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"issue":"2","key":"24_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M.N. Velev","year":"2003","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput.\u00a035(2), 73\u2013106 (2003)","journal-title":"J. Symb. Comput."},{"issue":"6","key":"24_CR3","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1109\/TCAD.2002.1004311","volume":"21","author":"G.-J. Nam","year":"2002","unstructured":"Nam, G.-J., Sakallah, K.A., Rutenbar, R.A.: A new FPGA detailed routing approach via search-based Boolean satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a021(6), 674\u2013684 (2002)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"24_CR4","unstructured":"Kautz, H.A., Selman, B.: Planning as Satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-24605-3_30","volume-title":"Theory and Applications of Satisfiability Testing","author":"J. Franco","year":"2004","unstructured":"Franco, J., Kouril, M., Schlipf, J., Ward, J., Weaver, S., Dransfield, M., Vanfleet, W.M.: SBSAT: a State-Based, BDD-Based Satisfiability Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 398\u2013410. Springer, Heidelberg (2004)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: DAC, pp. 818\u2013823. ACM (2003)","DOI":"10.1145\/776038.776039"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11527695_19","volume-title":"Theory and Applications of Satisfiability Testing","author":"G. Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Search vs. Symbolic Techniques in Satisfiability Solving. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 235\u2013250. Springer, Heidelberg (2005)"},{"issue":"1\/2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1006303512524","volume":"24","author":"I. Rish","year":"2000","unstructured":"Rish, I., Dechter, R.: Resolution versus Search: Two Strategies for SAT. J. Autom. Reasoning\u00a024(1\/2), 225\u2013275 (2000)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"24_CR9","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0166-218X(02)00403-1","volume":"130","author":"J.F. Groote","year":"2003","unstructured":"Groote, J.F., Zantema, H.: Resolution and binary decision diagrams cannot simulate each other polynomially. Discrete Applied Mathematics\u00a0130(2), 157\u2013171 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"24_CR10","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, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"10","key":"24_CR11","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1016\/j.ipl.2009.01.006","volume":"109","author":"W. Chen","year":"2009","unstructured":"Chen, W., Zhang, W.: A direct construction of polynomial-size OBDD proof of pigeon hole problem. Inf. Process. Lett.\u00a0109(10), 472\u2013477 (2009)","journal-title":"Inf. Process. Lett."},{"key":"24_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-73580-9_28","volume-title":"Abstraction, Reformulation, and Approximation","author":"P. Surynek","year":"2007","unstructured":"Surynek, P.: Solving Difficult SAT Instances Using Greedy Clique Decomposition. In: Miguel, I., Ruml, W. (eds.) SARA 2007. LNCS (LNAI), vol.\u00a04612, pp. 359\u2013374. Springer, Heidelberg (2007)"},{"issue":"8","key":"24_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers ACM (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"24_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/11941439_67","volume-title":"AI 2006: Advances in Artificial Intelligence","author":"W. Yue","year":"2006","unstructured":"Yue, W., Xu, Y., Su, K.: BDDRPA*: An Efficient BDD-Based Incremental Heuristic Search Algorithm for Replanning. In: Sattar, A., Kang, B.H. (eds.) AI 2006. LNCS (LNAI), vol.\u00a04304, pp. 627\u2013636. Springer, Heidelberg (2006)"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Xu, Y., Yue, W.: A Generalized Framework for BDD-based Replanning A* Search. In: Kim, H.-K., Lee, R.Y. (eds.) SNPD, pp. 133\u2013139. IEEE Computer Society (2009)","DOI":"10.1109\/SNPD.2009.9"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-02270-8_28","volume-title":"Frontiers in Algorithmics","author":"Y. Xu","year":"2009","unstructured":"Xu, Y., Yue, W., Su, K.: The BDD-Based Dynamic A* Algorithm for Real-Time Replanning. In: Deng, X., Hopcroft, J.E., Xue, J. (eds.) FAW 2009. LNCS, vol.\u00a05598, pp. 271\u2013282. Springer, Heidelberg (2009)"},{"issue":"1-3","key":"24_CR18","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10817-005-9009-7","volume":"35","author":"G. Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Symbolic Techniques in Satisfiability Solving. J. Autom. Reasoning\u00a035(1-3), 25\u201350 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T. Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended Resolution Proofs for Symbolic SAT Solving with Quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 54\u201360. Springer, Heidelberg (2006)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C. Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended Resolution Proofs for Conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 600\u2013611. Springer, Heidelberg (2006)"},{"key":"24_CR21","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package, Release 2.4.1. Technical report, University of Colorado at Boulder (2005)"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1145\/513918.514102","volume-title":"DAC 2002: Proceedings of the 39th Conference on Design Automation","author":"F.A. Aloul","year":"2002","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: DAC 2002: Proceedings of the 39th Conference on Design Automation, pp. 731\u2013736. ACM, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Frontiers in Algorithmics and Algorithmic Aspects in Information and Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29700-7_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:54:15Z","timestamp":1743026055000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29700-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642296994","9783642297007"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29700-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}