{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:13Z","timestamp":1725471193749},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_29","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"318-331","source":"Crossref","is-referenced-by-count":4,"title":["A Powerful Technique to Eliminate Isomorphism in Finite Model Search"],"prefix":"10.1007","author":[{"given":"Xiangxue","family":"Jia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/276393.276396","volume":"20","author":"D. Jackson","year":"1998","unstructured":"Jackson, D., Jha, S., Damon, C.A.: Isomorph-free model enumeration: A new method for checking relational specifications. ACM Transactions on Programming Languages and Systems\u00a020(2), 302\u2013343 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"29_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.entcs.2005.01.003","volume":"125","author":"T. Boy de la Tour","year":"2005","unstructured":"Boy de la Tour, T., Countcham, P.: An isomorph-free SEM-like enumeration of models. Electr. Notes Theor. Comput. Sci.\u00a0125(2), 91\u2013113 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., et al.: Chaff: Engineering an efficient SAT solver. In: Proc. 39th Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Audemard, G., Henocque, L.: The extended least number heuristic. In: Proc. of the 1st Int\u2019l Joint Conference on Automated Reasoning, pp. 427\u2013442 (2001)","DOI":"10.1007\/3-540-45744-5_35"},{"issue":"2","key":"29_CR5","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library \u2013 CNF release v1. 2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"29_CR7","unstructured":"Gent, I., Smith, B.: Symmetry breaking in constraint programming. In: Proc. ECAI 2000, pp. 599\u2013603 (2000)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-45193-8_23","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"I. Gent","year":"2003","unstructured":"Gent, I., Harvey, W., Kelsey, T., Linton, S.: Generic SBDD using computational group theory. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 333\u2013347. Springer, Heidelberg (2003)"},{"key":"29_CR9","unstructured":"Crawford, J.: A theoretical analysis of reasoning by symmetry in first order logic. Technical report, AT&T Bell Laboratories (1996)"},{"key":"29_CR10","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proc. KR 1996, pp. 149\u2013159 (1996)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","author":"J. Slaney","year":"1994","unstructured":"Slaney, J.: Finite domain enumerator. system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, Springer, Heidelberg (1994)"},{"issue":"1","key":"29_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00244457","volume":"17","author":"J. Zhang","year":"1996","unstructured":"Zhang, J.: Constructing finite algebras with FALCON. Journal of Automated Reasoning\u00a017(1), 1\u201322 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11532231_32","volume-title":"Automated Deduction \u2013 CADE-20","author":"J. Zhang","year":"2005","unstructured":"Zhang, J.: Computer search for counterexamples to Wilkie\u2019s identity. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 441\u2013451. Springer, Heidelberg (2005)"},{"key":"29_CR14","unstructured":"Zhang, J., Zhang, H.S.: a system for enumerating models. In: Proc. 14th Int\u2019l Joint Conf. on Artificial Intelligence (IJCAI), pp. 298\u2013303 (1995)"},{"key":"29_CR15","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve mace-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (Miami, USA) (2003)"},{"key":"29_CR16","unstructured":"Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proc. 13th Int\u2019l Joint Conf. on Artificial Intelligence (IJCAI), pp. 52\u201357 (1993)"},{"key":"29_CR17","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: The MiniSat page. Webpage, Chalmers University (2005), \n                    \n                      http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"issue":"4","key":"29_CR18","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/8.4.511","volume":"8","author":"N. Peltier","year":"1998","unstructured":"Peltier, N.: A new method for automated finite model building exploiting failures and symmetries. J. of Logic and Computation\u00a08(4), 511\u2013543 (1998)","journal-title":"J. of Logic and Computation"},{"key":"29_CR19","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1142\/S0218196792000104","volume":"2","author":"S. Burris","year":"1992","unstructured":"Burris, S., Lee, S.: Small models of the high school identities. Intl. J. of Algebra and Computatio\u00a02, 139\u2013178 (1992)","journal-title":"Intl. J. of Algebra and Computatio"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45578-7_7","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"T. Fahle","year":"2001","unstructured":"Fahle, T., Schamberger, S., Sellmann, M.: Symmetry breaking. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, pp. 93\u2013107. Springer, Heidelberg (2001)"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"McCune, W.: MACE 2.0 reference manual and guide. Technical Report No. 249, Argonne National Laboratory, Argonne, IL, USA (2001)","DOI":"10.2172\/797949"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. Technical Report No. 264, Argonne National Laboratory, Argonne, IL, USA (2003)","DOI":"10.2172\/822574"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:34:43Z","timestamp":1558308883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11814771_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}