{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T23:35:51Z","timestamp":1790811351637,"version":"4.1.0"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,10,9]],"date-time":"2008-10-09T00:00:00Z","timestamp":1223510400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10601-008-9060-1","type":"journal-article","created":{"date-parts":[[2008,10,8]],"date-time":"2008-10-08T14:13:15Z","timestamp":1223475195000},"page":"478-505","source":"Crossref","is-referenced-by-count":17,"title":["SymChaff: exploiting symmetry in a structure-aware satisfiability solver"],"prefix":"10.1007","volume":"14","author":[{"given":"Ashish","family":"Sabharwal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2008,10,9]]},"reference":[{"key":"9060_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F. A., Markov, I. L., & Sakallah, K. A. (2003a). Shatter: Efficient symmetry-breaking for Boolean satisfiability. In Proceedings of DAC-03: 40th design automation conference (pp. 836\u2013839). Anahein, CA, June 2003.","DOI":"10.1145\/775832.776042"},{"key":"9060_CR2","unstructured":"Aloul, F. A., Ramani, A., Markov, I. L., & Sakallah, K. A. (2002). PBS: A backtrack-search pseudo-Boolean solver and optimizer. In Proceedings of SAT-02: 5th international conference on theory and applications of satisfiability testing (pp. 346\u2013353). Cincinnati, OH, May 2002."},{"issue":"9","key":"9060_CR3","doi-asserted-by":"crossref","first-page":"1117","DOI":"10.1109\/TCAD.2003.816218","volume":"22","author":"F. A. Aloul","year":"2003","unstructured":"Aloul, F. A., Ramani, A., Markov, I. L., & Sakallah, K. A. (2003b). Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(9), 1117\u20131137.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"5","key":"9060_CR4","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"F. A. Aloul","year":"2006","unstructured":"Aloul, F. A., Sakallah, K. A., & Markov, I. L. (2006). Efficient symmetry breaking for Boolean satisfiability. IEEE Transactions on Computers, 55(5), 549\u2013558.","journal-title":"IEEE Transactions on Computers"},{"key":"9060_CR5","unstructured":"Bayardo Jr., R. J. & Schrag, R. C. (1997). Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of AAAI-97: 14th conference on artificial intelligence (pp. 203\u2013208). Providence, RI, July 1997."},{"key":"9060_CR6","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., & Sabharwal, A. (2004). Understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22, 319\u2013351, Dec.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9060_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of DAC-99: 36th design automation conference (pp. 317\u2013320). New Orleans, LA, June 1999.","DOI":"10.21236\/ADA360973"},{"issue":"3","key":"9060_CR8","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1109\/TCAD.2004.842808","volume":"24","author":"D. Chai","year":"2005","unstructured":"Chai, D., & Kuehlmann, A. (2005). A fast pseudo-Boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(3), 305\u2013317.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"9060_CR9","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"Cook, W., Coullard, C. R., & Turan, G. (1987). On the complexity of cutting plane proofs. Discrete Applied Mathematics, 18, 25\u201338.","journal-title":"Discrete Applied Mathematics"},{"key":"9060_CR10","unstructured":"Crawford, J. M., Ginsberg, M. L., Luks, E. M., & Roy, A. (1996). Symmetry-breaking predicates for search problems. In Proceedings of KR-96: 5th international conference on principles of knowledge representation and reasoning (pp. 148\u2013159). Cambridge, MA, Nov 1996."},{"key":"9060_CR11","doi-asserted-by":"crossref","unstructured":"Darga, P. T., Liffiton, M. H., Sakallah, K. A., & Markov, I. L. (2004). Exploiting structure in symmetry detection for CNF. In Proceedings of DAC-04: 41st design automation conference (pp. 518\u2013522). San Diego, CA, June 2004.","DOI":"10.1145\/996566.996712"},{"key":"9060_CR12","first-page":"201","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Communications of the ACM, 7, 201\u2013215.","journal-title":"Communications of the ACM"},{"key":"9060_CR13","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. Communications of the ACM, 5, 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"9060_CR14","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1613\/jair.1555","volume":"22","author":"H. E. Dixon","year":"2004","unstructured":"Dixon, H. E., Ginsberg, M. L., Luks, E. M., & Parkes, A. J. (2004a). Generalizing Boolean satisfiability II: Theory. Journal of Artificial Intelligence Research, 22, 481\u2013534.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9060_CR15","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1613\/jair.1353","volume":"21","author":"H. E. Dixon","year":"2004","unstructured":"Dixon, H. E., Ginsberg, M. L., & Parkes, A. J. (2004b) Generalizing Boolean satisfiability I: Background and survey of existing work. Journal of Artificial Intelligence Research, 21, 193\u2013243.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9060_CR16","volume-title":"Proceedings of SAT-05: 8th international conference on theory and applications of satisfiability testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2005) MiniSat: A SAT solver with conflict-clause minimization. In Proceedings of SAT-05: 8th international conference on theory and applications of satisfiability testing. UK: St. Andrews, June 2005."},{"key":"9060_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-45578-7_7","volume-title":"CP-01: 7th international conference on principles and practice of constraint programming","author":"T. Fahle","year":"2001","unstructured":"Fahle, T., Schamberger, S., & Sellmann, M. (2001). Symmetry breaking. In CP-01: 7th international conference on principles and practice of constraint programming. Lecture notes in computer science (Vol. 2239, pp. 93\u2013107). Cyprus: Paphos, Nov 2001."},{"issue":"3\/4","key":"9060_CR18","first-page":"198","volume":"2","author":"R. E. Fikes","year":"1971","unstructured":"Fikes, R. E., & Nilsson, N. J. (1971). STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2(3\/4), 198\u2013208.","journal-title":"Artificial Intelligence"},{"key":"9060_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-45578-7_6","volume-title":"CP-01: 7th international conference on principles and practice of constraint programming","author":"F. Focacci","year":"2001","unstructured":"Focacci, F., & Milano, M. (2001). Global cut framework for removing symmetries. In CP-01: 7th international conference on principles and practice of constraint programming. Lecture notes in computer science (Vol. 2239, pp. 77\u201392). Cyprus: Paphos, Nov 2001."},{"key":"9060_CR20","unstructured":"Fox, M., & Long, D. (1999). The detection and exploitation of symmetry in planning problems. In Proceedings of IJCAI-99: 16th international joint conference on artificial intelligence (pp. 956\u2013961), July 1999."},{"key":"9060_CR21","unstructured":"Fox, M., & Long, D. (2002). Extending the exploitation of symmetries in planning. In Proceedings of AIPS-02: 6th international conference on artificial intelligence planning systems (pp. 83\u201391), Apr 2002."},{"key":"9060_CR22","volume-title":"Logic for computer science","author":"J. H. Gallier","year":"1986","unstructured":"Gallier, J. H. (1986). Logic for computer science. New York: Harper & Row."},{"key":"9060_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-540-45193-8_23","volume-title":"CP-03: 9th international conference on principles and practice of constraint programming","author":"I. P. Gent","year":"2003","unstructured":"Gent, I. P., Harvey, W., Kelsey, T., & Linton, S. (2003). Generic SBDD using computational group theory. In CP-03: 9th international conference on principles and practice of constraint programming. Lecture notes in computer science (Vol. 2833, pp. 333\u2013347). Ireland: Kinsale, Sept 2003."},{"key":"9060_CR24","unstructured":"Gent, I. P., & Smith, B. M. (2000). Symmetry breaking in constraint programming. In Proceedings of ECAI-00: 14th European conference on artificial intelligence (pp. 599\u2013603). Berlin, Germany, Aug 2000."},{"key":"9060_CR25","doi-asserted-by":"crossref","unstructured":"Goldberg, E., & Novikov, Y. (2002). BerkMin: A fast and robust sat-solver. In Design, automation and test in europe conference and exposition (DATE) (pp. 142\u2013149). Paris, France 2002.","DOI":"10.1109\/DATE.2002.998262"},{"key":"9060_CR26","unstructured":"Gomes, C. P., Selman, B., McAloon, K., & Tretkoff, C. (1998). Randomization in backtrack search: Exploiting heavy-tailed profiles for solving hard scheduling problems. In Proceedings of AIPS-98: 4th international conference on artificial intelligence planning systems (pp. 208\u2013213). Pittsburgh, PA, June 1998."},{"key":"9060_CR27","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A. (1985) The intractability of resolution. Theoretical Computer Science, 39, 297\u2013305.","journal-title":"Theoretical Computer Science"},{"key":"9060_CR28","unstructured":"Heule, M., van Zwieten, J., Dufour, M., & van Maaren, H. (2004). March_eq: Implementing additional reasoning into an efficient lookahead SAT solver. In Proceedings of SAT-04: 7th international conference on theory and applications of satisfiability testing. Lecture notes in computer science (Vol. 3542, pp. 345\u2013359) Vancouver, BC, May 2004."},{"key":"9060_CR29","volume-title":"Cliques, coloring and satisfiability: The second DIMACS implementation challenge. DIMACS series in discrete mathematics and theoretical computer science (Vol. 26)","year":"1996","unstructured":"Johnson, D. S., & Trick, M. A. (eds.) (1996). Cliques, coloring and satisfiability: The second DIMACS implementation challenge. DIMACS series in discrete mathematics and theoretical computer science (Vol. 26). Providence: American Mathematical Society."},{"key":"9060_CR30","unstructured":"Kautz, H. A., & Selman, B. (1992). Planning as satisfiability. In Proceedings of ECAI-92: 10th European conference on artificial intelligence (pp. 359\u2013363), Vienna, Austria, Aug 1992."},{"key":"9060_CR31","unstructured":"Kautz, H. A., & Selman, B. (1998) BLACKBOX: A new approach to the application of theorem proving to problem solving. In Working notes of the workshop on planning as combinatorial search, held in conjunction with AIPS-98, Pittsburgh, PA, 1998."},{"key":"9060_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0333-9","volume-title":"The graph isomorphism problem: Its structural complexity","author":"J. K\u00f6bler","year":"1993","unstructured":"K\u00f6bler, J., Sch\u00f6ning, U., & Tor\u00e1n, J. (1993). The graph isomorphism problem: Its structural complexity. Boston: Birkhauser."},{"key":"9060_CR33","doi-asserted-by":"crossref","unstructured":"Konuk, H., & Larrabee, T. (1993). Explorations of sequential ATPG using Boolean satisfiability. In 11th VLSI test symposium, (pp. 85\u201390).","DOI":"10.1109\/VTEST.1993.313303"},{"key":"9060_CR34","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B. (1985). Short proofs for tricky formulas. Acta Informatica, 22 253\u2013274.","journal-title":"Acta Informatica"},{"key":"9060_CR35","unstructured":"Le Berre, D., & Simon, L. (2004). (Organizers). SAT 2004 competition, May. http:\/\/www.satcompetition.org\/2004 ."},{"key":"9060_CR36","unstructured":"Le Berre, D., & Simon, L. (2005). (Organizers). SAT 2005 competition, June. http:\/\/www.satcompetition.org\/2005 ."},{"key":"9060_CR37","doi-asserted-by":"crossref","unstructured":"Li, C. M., Jurkowiak, B., & Purdom, P. W. (2002). Integrating symmetry breaking into a DLL procedure. In International conference on theory and applications of satisfiability testing (pp. 149\u2013155), Cincinnati, OH, May 2002.","DOI":"10.1023\/A:1016557927479"},{"key":"9060_CR38","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J. P., & Sakallah, K. A. (1996). GRASP\u2014a new search algorithm for satisfiability. In Proceedings of ICCAD-96: International conference on computer aided design (pp. 220\u2013227), San Jose, CA, Nov 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"9060_CR39","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J. P., & Sakallah, K. A. (1997). Robust search algorithms for test pattern generation. In Proceedings of the 27th international symposium on fault-tolerant computing (pp. 152\u2013161). Seattle, WA, June 1997.","DOI":"10.1109\/FTCS.1997.614088"},{"key":"9060_CR40","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Proceedings of DAC-01: 38th design automation conference (pp. 530\u2013535). Las Vegas, NV, June 2001."},{"key":"9060_CR41","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-45643-0_3","volume-title":"ALENEX","author":"D. B. Motter","year":"2002","unstructured":"Motter, D. B., & Markov, I. (2002). A compressed breadth-first search for satisfiability. In ALENEX. Lecture notes in computer science (Vol. 2409, pp. 29\u201342). San Francisco: Springer."},{"issue":"1\u20132","key":"9060_CR42","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s10472-004-8427-2","volume":"44","author":"D. B. Motter","year":"2005","unstructured":"Motter, D. B., Roy, J. A., & Markov, I. (2005). Resolution cannot polynomially simulate compressed-BFS. Annals of Mathematics and Artificial Intelligence, 44,(1\u20132), 121\u2013156.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9060_CR43","unstructured":"Nadel, A. (2002). The Jerusat SAT solver. Master\u2019s thesis, Hebrew University of Jerusalem."},{"key":"9060_CR44","doi-asserted-by":"crossref","unstructured":"Petrie, K. E., & Smith, B. M. (2003). Symmetry breaking in graceful graphs. In CP-03: 9th international conference on principles and practice of constraint programming. Lecture notes in computer science (Vol. 2833, pp. 930\u2013934). Kinsale, Ireland, Sept 2003.","DOI":"10.1007\/978-3-540-45193-8_81"},{"issue":"3","key":"9060_CR45","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P. (1997). Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3) 981\u2013998, Sept.","journal-title":"Journal of Symbolic Logic"},{"key":"9060_CR46","doi-asserted-by":"crossref","unstructured":"Puget, J.-F. (1993). On the satisfiability of symmetrical constrained satisfaction problems. In International symposium on methodologies for intelligent systems. Lecture notes in computer science (Vol. 689, pp. 350\u2013361), Trondheim, Norway, June 1993.","DOI":"10.1007\/3-540-56804-2_33"},{"key":"9060_CR47","doi-asserted-by":"crossref","unstructured":"Puget, J.-F. (2006a). Dynamic lex constraints. In CP-06: 12th international conference on principles and practice of constraint programming. Lecture Notes in Computer Science (Vol. 4204, pp. 453\u2013467). Nantes, France, Sept 2006.","DOI":"10.1007\/11889205_33"},{"key":"9060_CR48","unstructured":"Puget, J.-F. (2006b) An efficient way of breaking value symmetries. In Proceedings of AAAI-06: 21st conference on artificial intelligence. Boston, MA, July 2006."},{"issue":"2","key":"9060_CR49","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1145\/972639.972640","volume":"51","author":"R. Raz","year":"2004","unstructured":"Raz, R. (2004). Resolution lower bounds for the weak pigeonhole principle. Journal of the ACM, 51(2), 115\u2013138.","journal-title":"Journal of the ACM"},{"key":"9060_CR50","unstructured":"Sabharwal, A. (2005a) Algorithmic applications of propositional proof complexity. PhD thesis, Seattle: University of Washington."},{"key":"9060_CR51","unstructured":"Sabharwal, A. (2005b). SymChaff: A structure-aware satisfiability solver. In Proceedings of AAAI-05: 20th national conference on artificial intelligence (pp. 467\u2013474), Pittsburgh, PA, July 2005."},{"key":"9060_CR52","series-title":"DIMACS series in discrete mathematics and theoretical computer science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1090\/dimacs\/026\/25","volume-title":"Cliques, coloring and satisfiability: The second DIMACS implementation challenge","author":"B. Selman","year":"1996","unstructured":"Selman, B., Kautz, H., & Cohen, B. (1996) Local search strategies for satisfiability testing. In D. S. Johnson & M. A. Trick (Eds.), Cliques, coloring and satisfiability: The second DIMACS implementation challenge. DIMACS series in discrete mathematics and theoretical computer science (Vol. 26, pp. 521\u2013532). Providence: American Mathematical Society."},{"key":"9060_CR53","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"1","author":"O. Shtrichman","year":"2004","unstructured":"Shtrichman, O. (2004) Accelerating bounded model checking of safety properties. Formal Methods in System Design, 1, 5\u201324.","journal-title":"Formal Methods in System Design"},{"issue":"9","key":"9060_CR54","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P. R. Stephan","year":"1996","unstructured":"Stephan, P. R., Brayton, R. K., & Sangiovanni-Vincentelli, A. L. (1996). Combinatorial test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(9), 1167\u20131176.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"9060_CR55","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0166-218X(99)00039-6","volume":"96\u201397","author":"A. Urquhart","year":"1999","unstructured":"Urquhart, A. (1999). The symmetry rule in propositional logic. Discrete Applied Mathematics, 96\u201397, 177\u2013193.","journal-title":"Discrete Applied Mathematics"},{"issue":"2","key":"9060_CR56","doi-asserted-by":"crossref","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. (2003). Effective use of Boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. Journal of Symbolic Computation, 35(2), 73\u2013106.","journal-title":"Journal of Symbolic Computation"},{"key":"9060_CR57","doi-asserted-by":"crossref","unstructured":"Walsh, T. (2006). General symmetry breaking constraints. In CP-06: 12th international conference on principles and practice of constraint programming. Lecture notes in computer science (Vol. 4204, pp. 650\u2013664), Sept 2006.","DOI":"10.1007\/11889205_46"},{"key":"9060_CR58","unstructured":"Zhang, H. (1997). SATO: An efficient propositional prover. In Proceedings of CADE-97: 14th international conference on automated deduction. Lecture notes in computer science (Vol. 1249, pp. 272\u2013275). Townsville, Australia, July 1997."},{"key":"9060_CR59","unstructured":"Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In Proceedings of ICCAD-01: International conference on computer aided design (pp. 279\u2013285). San Jose, CA, Nov 2001."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9060-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-008-9060-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9060-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T15:14:14Z","timestamp":1559229254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-008-9060-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10,9]]},"references-count":59,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["9060"],"URL":"https:\/\/doi.org\/10.1007\/s10601-008-9060-1","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10,9]]}}}