{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:20:58Z","timestamp":1743153658356,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":62,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642366741"},{"type":"electronic","value":"9783642366758"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36675-8_5","type":"book-chapter","created":{"date-parts":[[2013,2,28]],"date-time":"2013-02-28T19:04:22Z","timestamp":1362078262000},"page":"101-130","source":"Crossref","is-referenced-by-count":6,"title":["MACE4 and SEM: A Comparison of Finite Model Generators"],"prefix":"10.1007","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-45620-1_19","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Benhamou, B.: Reasoning by Symmetry and Function Ordering in Finite Model Generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 226. Springer, Heidelberg (2002)"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s10817-006-9040-3","volume":"36","author":"G. Audemard","year":"2006","unstructured":"Audemard, G., Benhamou, B., Henocque, L.: Predicting and Detecting Symmetries in FOL Finite Model Search. Journal of Automated Reasoning\u00a036(3), 177\u2013212 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-45744-5_35","volume-title":"Automated Reasoning","author":"G. Audemard","year":"2001","unstructured":"Audemard, G., Henocque, L.: The eXtended Least Number Heuristic. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 427\u2013442. Springer, Heidelberg (2001)"},{"key":"5_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solver. In: Twenty-First International Joint Conference on Artificial Intelligence, IJCAI 2009 (2009)"},{"issue":"1","key":"5_CR5","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P. Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., De Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. of Applied Logic\u00a07(1), 58\u201374 (2009)","journal-title":"J. of Applied Logic"},{"key":"5_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"issue":"1,2","key":"5_CR7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/FI-1999-391202","volume":"39","author":"B. Benhamou","year":"1999","unstructured":"Benhamou, B., Henocque, L.: A new method for finite model search in equational theories: FMSET system. Fundamenta Informaticae\u00a039(1,2), 21\u201338 (1999)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1002\/(SICI)1520-6610(1997)5:6<449::AID-JCD6>3.0.CO;2-F","volume":"5","author":"F.E. Bennett","year":"1997","unstructured":"Bennett, F.E., Du, B., Zhang, H.: Existence of conjugate orthogonal diagonal Latin squares. J. Combin. Designs\u00a05, 449\u2013461 (1997)","journal-title":"J. Combin. Designs"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0012-365X(02)00461-2","volume":"261","author":"F.E. Bennett","year":"2003","unstructured":"Bennett, F.E., Du, B., Zhang, H.: Existence of self-orthogonal diagonal Latin squares with a missing subsquare. Discrete Math.\u00a0261, 69\u201386 (2003)","journal-title":"Discrete Math."},{"key":"5_CR10","first-page":"41","volume-title":"Contemporary Design Theory: A Collection of Surveys","author":"F.E. Bennett","year":"1992","unstructured":"Bennett, F.E., Zhu, L.: Conjugate-orthogonal Latin squares and related structures. In: Dinitz, J., Stinson, D. (eds.) Contemporary Design Theory: A Collection of Surveys, pp. 41\u201396. Wiley, New York (1992)"},{"key":"5_CR11","unstructured":"Boy de la Tour, T.: Up-to-Isomorphism Enumeration of Finite Models - The Monadic Case. In: Bonacina, M.P., Furbach, U. (eds.) International Workshop First-Order Theorem Proving (FTP 1997). RISC-Linz Report Series No. 97-50, pp. 29\u201333. Schloss Hagenberg by Linz, Austria (1997)"},{"key":"5_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-44990-6_20","volume-title":"Artificial Intelligence and Symbolic Computation","author":"T. Boy de la Tour","year":"2001","unstructured":"Boy de la Tour, T.: Some Techniques of Isomorph-Free Search. In: Campbell, J., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol.\u00a01930, pp. 240\u2013252. Springer, Heidelberg (2001)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J., Herold, A., Kapur, D., Siekmann, J.H., Stickel, M., Tepp, M., Zhang, H.: Opening the AC-unification race. J. of Automated Reasoning\u00a0(4), 465\u2013474 (1988)","DOI":"10.1007\/BF00297251"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s00012-004-1900-2","volume":"52","author":"S. Burris","year":"2004","unstructured":"Burris, S., Yeats, K.: The saga of the high school identities. Algebra Universalis\u00a052, 325\u2013342 (2004)","journal-title":"Algebra Universalis"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol.\u00a031. Kluwer Academic Publisher (2004)","DOI":"10.1007\/978-1-4020-2653-9"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0018439","volume-title":"Logics in AI","author":"R. Caferra","year":"1991","unstructured":"Caferra, R., Zabel, N.: Extending Resolution for Model Construction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol.\u00a0478, pp. 153\u2013169. Springer, Heidelberg (1991)"},{"key":"5_CR17","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve Mace-style finite model finding. In: Model Computation \u2013 Principles, Algorithms, Applications, CADE-19 Workshop W4, Miami, Florida, USA (2003)"},{"key":"5_CR18","volume-title":"Latin squares and their applications","author":"J. D\u00e9nes","year":"1974","unstructured":"D\u00e9nes, J., Keedwell, A.D.: Latin squares and their applications. Academic Press, New York (1974)"},{"key":"5_CR19","first-page":"193","volume":"37","author":"B. Du","year":"2001","unstructured":"Du, B.: Self-orthogonal diagonal Latin square with missing subsquare. JCMCC\u00a037, 193\u2013203 (2001)","journal-title":"JCMCC"},{"key":"5_CR20","unstructured":"Een, N., Svrensson, N.: Minisat: A SAT solver with conflict-clause minimization. In: SAT 2005 (2005) (poster paper)"},{"key":"5_CR21","unstructured":"Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proc. Int\u2019l Joint Conf. on Artificial Intelligence (IJCAI 1993), pp. 52\u201357 (1993)"},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/logcom\/6.1.1","volume":"6","author":"A. Galton","year":"1996","unstructured":"Galton, A.: Note on a lemma of Ladkin. Journal of Logic and Computation\u00a06(1), 1\u20134 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1007\/3-540-55602-8_223","volume-title":"Automated Deduction - CADE-11","author":"R. Hasegawa","year":"1992","unstructured":"Hasegawa, R., Koshimura, M., Fujita, H.: MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. In: Kapur, D. (ed.) CADE-11. LNCS, vol.\u00a0607, pp. 776\u2013780. Springer, Heidelberg (1992)"},{"key":"5_CR24","unstructured":"Huang, Z., Zhang, H., Zhang, J.: Improving first-order model searching by propositional reasoning and lemma learning. In: The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada (May 2004)"},{"key":"5_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/11814771_29","volume-title":"Automated Reasoning","author":"X. Jia","year":"2006","unstructured":"Jia, X., Zhang, J.: A Powerful Technique to Eliminate Isomorphism in Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 318\u2013331. Springer, Heidelberg (2006)"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-51081-8_138","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1989","unstructured":"Kapur, D., Zhang, H.: An Overview of RRL: Rewrite Rule Laboratory. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 513\u2013529. Springer, Heidelberg (1989)"},{"key":"5_CR27","unstructured":"Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Proc. of National Conference of American Association on Artificial Intelligence (AAAI 1994), Seattle, WA, pp. 162\u2013167. MIT Press (1994)"},{"issue":"1","key":"5_CR28","first-page":"32","volume":"13","author":"V. Kumar","year":"1992","unstructured":"Kumar, V.: Algorithms for constraint satisfaction problems: A survey. AI Magazine\u00a013(1), 32\u201344 (1992)","journal-title":"AI Magazine"},{"issue":"6","key":"5_CR29","doi-asserted-by":"publisher","first-page":"2889","DOI":"10.1090\/S0002-9947-00-02350-3","volume":"352","author":"K. Kunen","year":"2000","unstructured":"Kunen, K.: The structure of conjugacy closed loops. Transactions of the American Mathematical Society\u00a0352(6), 2889\u20132911 (2000)","journal-title":"Transactions of the American Mathematical Society"},{"key":"5_CR30","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BF01243872","volume":"26","author":"J. Leech","year":"1989","unstructured":"Leech, J.: Skew lattices in rings. Algebra Universalis\u00a026, 48\u201372 (1989)","journal-title":"Algebra Universalis"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: A Theorem Prover Implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"issue":"2","key":"5_CR32","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination tree indexing and path indexing for term retrieval. J. of Automated Reasoning\u00a09(2), 147\u2013167 (1992)","journal-title":"J. of Automated Reasoning"},{"key":"5_CR33","unstructured":"McCune, W.: MACE 2.0 Reference Manual and Guide. Technical Memorandum No. 249, ANL\/MCS-TM-249, Argonne National Lab, Argonne, IL, USA (1994), http:\/\/www-unix.mcs.anl.gov\/AR\/mace2\/"},{"key":"5_CR34","unstructured":"McCune, W.: Otter 3.3 Reference Manual, Technical Memorandum No. 263, Argonne National Laboratory, Argonne, IL, USA (August 2003), http:\/\/www-unix.mcs.anl.gov\/AR\/otter\/otter33.pdf"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide, Technical Memorandum No. 264, Argonne National Laboratory, Argonne, IL, USA (August 2003), http:\/\/www.cs.unm.edu\/~mccune\/prover9\/","DOI":"10.2172\/822574"},{"key":"5_CR36","unstructured":"McCune, W.: Library for Automated Deduction Research (2009), http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"issue":"3","key":"5_CR37","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"J. of Automated Reasoning"},{"issue":"3","key":"5_CR38","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/BF00244271","volume":"1","author":"W. McCune","year":"1985","unstructured":"McCune, W., Henschen, L.J.: Experiments with semantic paramodulation. J. of Automated Reasoning\u00a01(3), 231\u2013261 (1985)","journal-title":"J. of Automated Reasoning"},{"issue":"2","key":"5_CR39","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"5_CR40","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-49545-2_14","volume-title":"Logics in Artificial Intelligence","author":"R. Pichler","year":"1998","unstructured":"Pichler, R.: Algorithms on Atomic Representations of Herbrand Models. In: Dix, J., Fari\u00f1as del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol.\u00a01489, pp. 199\u2013215. Springer, Heidelberg (1998)"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Automated Deduction - CADE-12","author":"J. Slaney","year":"1994","unstructured":"Slaney, J.: Finder: Finite Domain Enumerator. In: Bundy, A. (ed.) CADE-12. LNCS, vol.\u00a0814, pp. 798\u2013801. Springer, Heidelberg (1994)"},{"issue":"2","key":"5_CR42","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0898-1221(94)00219-B","volume":"29","author":"J. Slaney","year":"1995","unstructured":"Slaney, J., Fujita, M., Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Computers & Math. with Appl.\u00a029(2), 115\u2013132 (1995)","journal-title":"Computers & Math. with Appl."},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"764","DOI":"10.1007\/3-540-58156-1_56","volume-title":"Automated Deduction - CADE-12","author":"J. Slaney","year":"1994","unstructured":"Slaney, J., Lusk, E.L., McCune, W.: SCOTT: Semantically Constrained Otter (System Description). In: Bundy, A. (ed.) CADE-12. LNCS, vol.\u00a0814, pp. 764\u2013768. Springer, Heidelberg (1994)"},{"issue":"3","key":"5_CR44","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/PL00006032","volume":"61","author":"M. Spinks","year":"2000","unstructured":"Spinks, M.: On middle distributivity for Skew lattices. Semigroup Forum\u00a061(3), 341\u2013345 (2000)","journal-title":"Semigroup Forum"},{"key":"5_CR45","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1090\/S0002-9947-1957-0094404-6","volume":"85","author":"S.K. Stein","year":"1957","unstructured":"Stein, S.K.: On the foundations of quasigroups. Trans. Amer. Math. Soc.\u00a085, 228\u2013256 (1957)","journal-title":"Trans. Amer. Math. Soc."},{"key":"5_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0019355","volume-title":"Baltic Computer Science","author":"T. Tammet","year":"1991","unstructured":"Tammet, T.: Using Resolution for Deciding Solvable Classes and Building Finite Models. In: Barzdins, J., Bjorner, D. (eds.) Baltic Computer Science. LNCS, vol.\u00a0502, pp. 33\u201364. Springer, Heidelberg (1991)"},{"key":"5_CR47","unstructured":"Tammet, T.: Finite model building: improvements and comparisons. In: Model Computation \u2013 Principles, Algorithms, Applications, CADE-19 Workshop W4, Miami, Florida, USA (2003)"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Sato: An Efficient Propositional Prover. In: McCune, W. (ed.) CADE-14. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"5_CR49","unstructured":"Zhang, H.: Specifying Latin squares in propositional logic. In: Veroff, R. (ed.) Automated Reasoning and Its Applications, Essays in Honor of Larry Wos. MIT Press (1997)"},{"key":"5_CR50","unstructured":"Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, A., Heule, M., Van Haaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 17. IOS Press (2009)"},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"Zhang, H., Stickel, M.: Implementing the Davis-Putnam method. J. of Automated Reasoning\u00a024, 277\u2013296 (2000)","journal-title":"J. of Automated Reasoning"},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1007\/3-540-58156-1_54","volume-title":"Automated Deduction - CADE-12","author":"J. Zhang","year":"1994","unstructured":"Zhang, J.: Problems on the Generation of Finite Models. In: Bundy, A. (ed.) CADE-12. LNCS, vol.\u00a0814, pp. 753\u2013757. Springer, Heidelberg (1994)"},{"issue":"1","key":"5_CR53","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. J. of Automated Reasoning\u00a017(1), 1\u201322 (1996)","journal-title":"J. of Automated Reasoning"},{"key":"5_CR54","unstructured":"Zhang, J.: On the relational translation method for propositional modal logics. Technical Report ISCAS-LCS-96-12, Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (December 1996)"},{"key":"5_CR55","unstructured":"Zhang, J.: Showing the independence of an axiom for temporal intervals by model generation. Association for Automated Reasoning Newsletter, No. 40 (1998), http:\/\/www.aarinc.org\/Newsletters\/040-1998-06.html"},{"key":"5_CR56","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-48660-7_37","volume-title":"Automated Deduction - CADE-16","author":"J. Zhang","year":"1999","unstructured":"Zhang, J.: System Description: MCS: Model-Based Conjecture Searching. In: Ganzinger, H. (ed.) CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 393\u2013397. Springer, Heidelberg (1999)"},{"key":"5_CR57","unstructured":"Zhang, J.: Test problem and Perl scripts for finite model searching. Association for Automated Reasoning Newsletter, No. 47 (April 2000), http:\/\/www.aarinc.org\/Newsletters\/047-2000-04.html"},{"key":"5_CR58","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":"5_CR59","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proc. 14th Int\u2019l Joint Conf. on Artif. Intel. (IJCAI), pp. 298\u2013303 (1995)"},{"key":"5_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-60299-2_24","volume-title":"Principles and Practice of Constraint Programming - CP \u201995","author":"J. Zhang","year":"1995","unstructured":"Zhang, J., Zhang, H.: Constraint Propagation in Model Generation. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol.\u00a0976, pp. 398\u2013414. Springer, Heidelberg (1995)"},{"key":"5_CR61","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-30210-0_9","volume-title":"Artificial Intelligence and Symbolic Computation","author":"J. Zhang","year":"2004","unstructured":"Zhang, J., Zhang, H.: Extending Finite Model Searching with Congruence Closure Computation. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 94\u2013102. Springer, Heidelberg (2004)"},{"key":"5_CR62","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0012-365X(01)00342-9","volume":"254","author":"X. Zhang","year":"2002","unstructured":"Zhang, X.: Incomplete perfect Mendelsohn designs with block size four. Discrete Mathematics\u00a0254, 565\u2013597 (2002)","journal-title":"Discrete Mathematics"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36675-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,23]],"date-time":"2020-07-23T00:11:34Z","timestamp":1595463094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36675-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642366741","9783642366758"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36675-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}