Abstract
Equations and disequations over rational trees arise naturally in the context of constraint logic programming [6,10]. In this paper, we reconsider (after Colmerauer [4,7] and Jaffar [9]) the problem of solving these constraints incrementally (semi-dynamically) and consider the problem of determining entailment of these constraints with respect to a monotonically increasing constraint store of equations and disequations. The main contributions of the paper are new algorithms for disequation solving and disequality entailment. The algorithms exploit systematically three simple ideas: global caching, lazy evaluation and detection of implicit equalities. The disequation algorithm is a direct algorithm (contrary to Colmerauer's algorithm which uses unification as a subroutine). Its on-line version, which is almost-quadratic, is shown to be superior to Colmerauer's algorithm, which is almost-cubic, although Colmerauer's algorithm is superior off-line. Incremental disequality entailment is much more subtle, and to our knowledge was not considered before. We present a direct algorithm whose off-line version is almost-quadratic, and on-line version is almost-cubic. Its key idea is to reduce disequality entailment to a Boolean combination of equality entailments. Both versions improve upon a naive indirect algorithm by an order of magnitude asymptotically.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Hassan Ait-Kaci, in Warren's Abstract Machine (A Tutorial Reconstruction), Logic Programming Series, MIT Press, Cambridge, MA Press, 1992.
Hassan Ait-Kaci & Andreas Podelski, “Entailment and disentailment of order-sorted feature constraints,” Fourth International Conference on Logic Programming and Automated Reasoning, New York-Heidelberg-Berlin (1993, to appear).
Hassan Ait-Kaci, Andreas Podelski & Gert Smolka, “A feature-based constraint system for logic programming with entailment,” International Conference on Fifth Generation Computer Systems, Tokyo, Japan (June, 1992).
Alain Colmerauer, “Prolog and infinite trees,” in Logic Programming, Clark & Tarnlund, eds., APIC Studies in Data Processing #16, Academic Press, New York, NY, 1982, 231–251.
Alain Colmerauer, “Prolog II: Reference Manual and Theoretical Model,” Groupe Intelligence Artificielle, Universite Aix-Marseille, Internal report, 1982.
Alain Colmerauer, “Opening the Prolog III universe,” Byte (Aug., 1987).
Alain Colmerauer, “Equations and inequations on finite and infinite trees,” Second International Conference on Fifth Generation Computer Systems, Tokyo (Nov., 1984).
Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, A. Aggoun, Thomas Graf & F. Berthier, “The constraint logic programming language CHIP,” International Conference on Fifth Generation Computer Systems (1988).
Joxan Jaffar, “Efficient unification over infinite terms,” New Gener. Comput. 2 (1984), 207–219.
Joxan Jaffar & Jean-Louis Lassez, “Constraint logic programming,” Fourteenth Symposium on Principles of Programming Languages (Jan., 1987).
Michael J. Maher, “Logic semantics for a class of committed choice programs,” Fourth International Conference on Logic Programming, Melbourne, Australia (May, 1987).
Alberto Martelli & Ugo Montanari, “An efficient unification algorithm,” ACM TOPLAS 4 (Apr., 1982), 258–282.
M. S. Paterson & M. N. Wegman, “Linear unification,” J. Comput. System Sci. 16 (1978), 158–167.
Viswanath Ramachandran & Pascal Van Hentenryck, “Incremental algorithms for constraint solving and entailment over rational trees,” Brown Univ., CS Dept., Tech. Rep., forthcoming.
Vijay A. Saraswat, in Concurrent Constraint Programming, Logic Programming Series/ACM Doctoral Dissertation Award, MIT Press, Cambridge, MA, Nov., 1992.
Donald A. Smith, “Constraint operations for CLP(FT),” Eighth International Conference on Logic Programming, Paris (1991).
Gert Smolka & Ralf Treinen, “Records for logic programming,” DFKI, Research Report RR-92-23, Saarbrucken, Germany, Aug., 1992.
Gert Smolka & Ralf Treinen, “Records for logic programming,” JICSLP-92, Washington, DC (Nov., 1992).
Robert Endre Tarjan, in Data Structures and Network Algorithms, CBMS-NSF Regional Conference Series in Applied Mathematics, Society for Industrial and Applied Mathematics, Philadelphia, PA, 1983.
Robert Endre Tarjan, “On the efficiency of a good but not linear set merging algorithm,” J. Assoc. Comput. Mach. 22 (Apr., 1975), 215–225.
David H. D. Warren, “An abstract Prolog instruction set,” SRI International, Technical Note 309, Menlo Park, CA, Oct., 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramachandran, V., van Hentenryck, P. (1993). Incremental algorithms for constraint solving and entailment over rational trees. In: Shyamasundar, R.K. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1993. Lecture Notes in Computer Science, vol 761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57529-4_54
Download citation
DOI: https://doi.org/10.1007/3-540-57529-4_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57529-0
Online ISBN: 978-3-540-48211-6
eBook Packages: Springer Book Archive