Abstract
The model generation problem, regarded as a special case of the Constraint Satisfaction Problem (CSP), has many applications in AI, computer science and mathematics. In this paper, we describe how to increase propagation of constraints by using the ground congruence closure algorithm. The experimental results show that using the congruence closure algorithm can reduce the search space for some benchmark problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980)
Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proc. 13th IJCAI, pp. 52–57 (1993)
Hasegawa, R., Koshimura, M., Fujita, H.: MGTP: A parallel theorem prover based on lazy model generation. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 776–780. Springer, Heidelberg (1992)
Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Proc. 12th AAAI, pp. 162–167 (1994)
Kumar, V.: Algorithms for constraint satisfaction problems: A survey. AI Magazine 13(1), 32–44 (1992)
Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988)
McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical Report ANL/MCS-TM-194, Argonne National Laboratory (1994)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)
Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 78–90. Springer, Heidelberg (2003)
Slaney, J.: FINDER: Finite domain enumerator – system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798–801. Springer, Heidelberg (1994)
Slaney, J., Fujita, M., Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications 29(2), 115–132 (1995)
Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving, http://www.cs.miami.edu/~tptp/
Zhang, J.: Problems on the generation of finite models. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 753–757. Springer, Heidelberg (1994)
Zhang, J.: Constructing finite algebras with FALCON. J. Automated Reasoning 17(1), 1–22 (1996)
Zhang, J., Zhang, H.: Constraint propagation in model generation. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, pp. 398–414. Springer, Heidelberg (1995)
Zhang, J., Zhang, H.: SEM: A system for enumerating models. In: Proc. 14th IJCAI, pp. 298–303 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, J., Zhang, H. (2004). Extending Finite Model Searching with Congruence Closure Computation. In: Buchberger, B., Campbell, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2004. Lecture Notes in Computer Science(), vol 3249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30210-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30210-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23212-4
Online ISBN: 978-3-540-30210-0
eBook Packages: Springer Book Archive