Abstract
This article introduces two techniques to improve the propagation efficiency of CSP based finite model generation methods. One approach consists in statically rewriting some selected clauses so as to trigger added constraint propagations. The other approach uses a dynamic lookahead strategy to both filter out inconsistent domain values and select the most appropriate branching variable according to a first fail heuristic.
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.
References
Audemard, G., Benhamou, B., Henocque, L.: Two techniques to improve finite model search. Technical report, Laboratoire d’Informatique de Marseille (1999), accessible electronicaly at http://www.cmi.univ-mrs.fr/~audemard/publi.html
Audemard, G., Benhamou, B., Siegel, P.: La mĄéthode d’avalanche aval: une mĄéthode ĄénumĄérative pour sat. In: JNPC, pp. 17–25 (1999)
Benhamou, B., Henocque, L.: A hybrid method for finite model search in equational theories. Fundamenta Informaticae 39(l-2), 21–38 (1999)
Li, C.M., Anbulagan, A.: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), August 23-29, pp. 366–371 (1997)
Peltier, N.: A new method for automated finite model building exploiting failures and symmetries. Journal of logic and Computation 8(4), 511–543 (1998)
Slaney, J., Fujita, M., Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications 29(2), 115–132 (1993)
Slanley, J.: Finder: Finite domain enumerator, version 3 notes and guides. Technical report, Austrian National University (1993)
Zhang, H., Stickel, M.E.: Implementing the davis-putnam algorithm by tries. Technical report, Department of Computer Science, University of Iowa (1994)
Zhang, J., Zhang, H.: Constraint propagation in model generation. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976. Springer, Heidelberg (1995)
Zhang, J.: Constructing finite algebras with FALCON. Journal of Automated Reasoning 17(l), 1–22 (1996)
Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Mellish, C.S. (ed.) Proceedings of the Fourteenth IJCAI, pp. 298–303 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Benhamou, B., Henocque, L. (2000). Two Techniques to Improve Finite Model Search. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_24
Download citation
DOI: https://doi.org/10.1007/10721959_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive