iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1023/A:1009868906501
A Methodological View of Constraint Solving | Constraints Skip to main content
Springer Nature Link
Log in

A Methodological View of Constraint Solving

  • Published:
Constraints Aims and scope Submit manuscript

Abstract

Constraints are an effective tool to define sets of data by means of logical formulae. Our goal here is to survey the notion of constraint system and to give examples of constraint systems operating on various domains, such as natural, rational or real numbers, finite domains, and term domains. We classify the different methods used for solving constraints, syntactic methods based on transformations, semantic methods based on adequate representations of constraints, hybrid methods combining transformations and enumerations. The concepts and methods are illustrated via examples. We also discuss applications of constraints to various fields, such as programming, operations research, and theorem proving.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Abdulrab, H., & Maksimenko, M. (1995). General solutions of systems of linear diophantine equations and inequations. In 6th International Conference on Rewriting Techniques and Applications (J. Hsiang, ed.), volume 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, Springer-Verlag.

    Google Scholar 

  2. Aït-Kaci, H., & Podelski, A. (1991). Towards a meaning of life. In 3rd International Symposium on Programming Language Implementation and Logic Programming (J. Maluszyński and M. Wirsing, eds.), volume 528 of Lecture Notes in Computer Science, pages 255–274.

  3. Baader, F., & Schulz, K. (1992). Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 50–65.

  4. Backofen, R., & Smolka, G. (1995).Acomplete and recursive feature theory. Theoretical Computer Science, 146(1–2):143–268.

    Google Scholar 

  5. Beldiceanu, N., & Contejean, E. (1994). Introducing global constraints in CHIP. jmcm, 20(12):97–123.

    Google Scholar 

  6. Caferra, R., & Zabel, N. (1992). A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13(6):613–642.

    Google Scholar 

  7. Castro, C. (1998). Building constraint satisfaction problem solvers using rewrite rules and strategies. Fundamenta Informaticae, 34:263–293.

    Google Scholar 

  8. Cheng, A., & Kozen, D. (1996). Some notes on rational spaces. Technical report, Comp. Science Department, Cornell University.

  9. Colmerauer, A. (1984). Equations and inequations on finite and infinite trees. In Proceedings of FGCS'84, pages 85–99.

  10. Comon, H. (1990). Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387–411.

    Google Scholar 

  11. Comon, H. (1991). Disunification: A survey. In Computational Logic. Essays in honor of Alan Robinson (J.-L. Lassez and G. Plotkin, editors), chapter 9, pages 322–359. Cambridge (MA, USA), The MIT Press.

    Google Scholar 

  12. Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., & Tommasi, M. Tree automata techniques and applications. A preliminary version of this unpublished book is available on http://l3ux02.univ-lille3.fr/tata.

  13. Comon, H., & Delor, C. (1994). Equational formulae with membership constraints. Information and Computation, 112(2):167–216.

    Google Scholar 

  14. Comon, H., & Lescanne, P. (1989). Equational Problems and Disunification. Journal of Symbolic Computation, 7:371–425.

    Google Scholar 

  15. Comon, H., & Treinen, R. (1994). Ordering constraints on trees. In Colloquium on Trees in Algebra and Programming (S. Tison, editor), volume 787 of Lecture Notes in Computer Science, pages 1–14, Edinburgh, Scotland, Springer-Verlag. (Invited Lecture).

    Google Scholar 

  16. Contejean, E., & Devie, H. (1994). An efficient algorithm for solving systems of diophantine equations.Information and Computation, 113(1):143–172.

    Google Scholar 

  17. Dantzig, G. (1963). Linear Programming and Extensions. Princeton University Press.

  18. Dauchet, M. (1994). Rewriting and tree automata. In Proc. Spring School on Theoretical Computer Science: Rewriting (H. Comon and J.-P. Jouannaud, editors), volume 909 of Lecture Notes in Computer Science, Odeillo, France, Springer-Verlag.

    Google Scholar 

  19. Dincbas, M., van Hentenryck, P., Simonis, H., Aggoun, A., Graf, T., & Berthier, F. (1988). The constraint logic programming language CHIP. In Proceedings of the International Conference on Fifth Generation Computer Systems, volume 2, pages 693–702. Institute for New Generation Computer Technology.

    Google Scholar 

  20. Domenjoud, E. (1991). Outils pour la d´eduction automatique dans les th´eories associatives-commutatives.Thèse de doctorat de l'universit´e de Nancy I.

  21. Domenjoud, E., Klay, F., & Ringeissen, C. (1994). Combination techniques for non-disjoint equational theories. In Proceedings 12th International Conference onAutomated Deduction, Nancy (France) (A. Bundy, editor), volume 814 of Lecture Notes in Artificial Intelligence, pages 267–281, Springer-Verlag.

  22. Dowek, G., Hardin, T., and Kirchner, C. (1995). Higher-order unification via explicit substitutions, extended abstract. In Proceedings of LICS'95 (D. Kozen, editor), pages 366–374, San Diego.

  23. Dowek, G., Hardin, T., Kirchner, C., & Pfenning, F. (1996). Unification via explicit substitutions: The case of higher-order patterns. In Proceedings of JICSLP'96 (M. Maher, editor), Bonn (Germany), The MIT Press.

    Google Scholar 

  24. Fages, F. (1984). Associative-commutative unification. In Proceedings 7th International Conference on Automated Deduction, Napa Valley (Calif., USA) (R. Shostak, editor), volume 170 of Lecture Notes in Computer Science, pages 194–208, Springer-Verlag.

  25. Filgueiras, M., & Tomás, A. P. (1995). A fast method for finding the basis of nonnegative solutions to a linear Diophantine equation. Journal of Symbolic Computation, 19:507–526.

    Google Scholar 

  26. Frühwirth, T., Shapiro, E., Vardi, M., & Yardeni, E. (1991). Logic programs as types for logic programs. In Proc. 6th IEEE Symp Logic in Computer Science, Amsterdam, pages 300–309.

  27. Ganzinger, H., & Nieuwenhuis, R. (1996). The Saturate System. This manual is available at http://www.mpi-sb.mpg.de/ hg/systems/SATURATE/Saturate.html.

  28. Gilleron, R., Tison, S., & Tommasi, M. (1993). Solving systems of set constraints using tree automata. In Proc. 10th Symposium on Theoretical Aspects of Computer Science, Würzburg, LNCS.

    Google Scholar 

  29. Gilleron, R., Tison, S., & Tommasi, M. (1993). Solving systems of set constraints with negated subset relationships. In Proc. 34th Symposium on Foundations of Computer Science, pages 372–380, Palo Alto, CA, IEEE Computer Society Press.

    Google Scholar 

  30. Heintze, N. (1992). Set based program analysis. Ph.D. thesis, Carnegie Mellon University.

  31. Herbrand, J. (1930). Recherches sur la théorie de la démonstration. Travaux de la Soc. des Sciences et des Lettres de Varsovie, Classe III, 33(128).

  32. Huet, G. (1976). R´esolution d'´equations dans les langages d'ordre 1; 2;::: ω. Th´ese d'Etat, Univ. Paris 7.

  33. Jaffar, J., & Lassez, J.-L. (1987). Constraint logic programming. In Proceedings of the 14th Annual ACM Symposium on Principles Of Programming Languages, Munich (Germany), pages 111–119.

  34. Jaffar, J., & Maher, M. (1994). Constraint logic programming: A survey. Journal of Logic Programming, 19-20:503–582.

    Google Scholar 

  35. Jouannaud, J.-P., editor. (1994). First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, München, Germany, Springer-Verlag.

    Google Scholar 

  36. Jouannaud, J.-P., & Kirchner, C. (1991). Solving equations in abstract algebras: A rule-based survey of unification. In Computational Logic. Essays in Honor of Alan Robinson (J.-L. Lassez and G. Plotkin, editors), chapter 8, pages 257–321. Cambridge (MA, USA), The MIT Press.

    Google Scholar 

  37. Jouannaud, J.-P., & Kounalis, E. (1989). Automatic proofs by induction in theories without constructors.Information and Computation, 82(1).

  38. Jouannaud, J.-P., & Okada, M. (1991). Satisfiability of systems of ordinal notations with the subterm property is decidable. In 18th International Colloquium on Automata, Languages and Programming (J. L. Albert, B. Monien, and M. R. Artalejo, editors), volume 510 of Lecture Notes in Computer Science, pages 455–468, Madrid, Spain, Springer-Verlag.

    Google Scholar 

  39. Karmarkar, N. (1984). A new polynomial–time algorithm for linear programming. Combinatorica, 4:373–395.

    Google Scholar 

  40. Kirchner, C. (1989). From unification in combination of equational theories to a new AC-unification algorithm.In Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques (H. Aït-Kaci and M. Nivat, editors), pages 171–210, New York, Academic Press Inc.

    Google Scholar 

  41. Kirchner, C., Kirchner, H., & Rusinowitch, M. (1990). Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3):9–52. Special issue on Automatic Deduction. 360 H. COMON ET AL

    Google Scholar 

  42. Kirchner, C., Kirchner, H., & Vittek, M. (1995). Designing constraint logic programming languages using computational systems. In Principles and Practice of Constraint Programming. The Newport Papers. (P. Van Hentenryck and V. Saraswat, editors), chapter 8, pages 131–158, The MIT Press.

  43. Kozen, D. (1995). Set constraints in logic programming. Information and Computation. To appear.

  44. Lassez, J.-L., & Marriott, K. G. (1987). Explicit representation of terms defined by counter examples.Journal of Automated Reasoning, 3(3):1–17.

    Google Scholar 

  45. Maher, M. J. (1988). Complete axiomatization of the algebra of finite, rational trees and infinite trees. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK). Computer Society Press.

    Google Scholar 

  46. Martelli, A., & Montanari, U. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282.

  47. Martin, U., & Nipkow, T. (1989). Boolean unification. the story so far. Journal of Symbolic Computation, 7(3 & 4).

    Google Scholar 

  48. Miller, D. (1991). A logic programming language with lambda-abstraction, function variables, and simple unification. In Extensions of Logic Programming (P. Schroeder-Heister, editor). LNCS 475, Springer Verlag.

  49. Mishra, P. (1984). Towards a theory of types in prolog. In 1st IEEE Symposium on Logic Programming, pages 456–461, Atlantic City.

  50. Nelson, C. G., & Oppen, D. C. (1979). Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2).

  51. Nieuwenhuis, R. (1993). Simple LPO constraint solving methods. Information Processing Letters, 47(2):65–69.

    Google Scholar 

  52. Nipkow, T. (1989). Combining matching algorithms: The regular case. In Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA) (N. Dershowitz, editor), volume 355 of Lecture Notes in Computer Science, pages 343–358, Springer-Verlag.

  53. Podelski, A., editor. (1995). Constraint Programming: Basics and Trends, volume 910 of Lecture Notes in Computer Science, Springer-Verlag.

  54. Pottier, L. (1991). Minimal solutions of linear diophantine systems: Bounds and algorithms. In Proceedings of the Fourth International Conference on Rewriting Techniques and Applications, pages 162–173, Como, Italy.

  55. Puget, J.-F., & Leconte, M. (1995). Beyond the black box: Constraints as objects. In Proceedings of the International Logic Programming Symposium (J. Loyd, editor), pages 513–527, The MIT Press.

  56. Ringeissen, C. (1996). Combining decision algorithms for matching in the union of disjoint equational theories. Information and Computation, 126(2):144–160.

    Google Scholar 

  57. Ringeissen, C. (1996). Cooperation of decision procedures for the satisfiability problem. In Frontiers of Combining Systems, First International Workshop, Munich (Germany) (F. Baader and K. Schulz, editors), Applied Logic, pages 121–140, Kluwer Academic Publishers.

  58. Rounds, W. C., & Kasper, R. (1986).Acomplete logical calculus for record structures representing linguistic information. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass.

  59. Schmidt-Schauß, M. (1990). Unification in a combination of arbitrary disjoint equational theories. In Unification ( C. Kirchner, editor), pages 217–266, London, Academic Press Inc.

    Google Scholar 

  60. Schmidt-Schauß, M. (1994). An algorithm for distributive unification. Research Report 13/94, Fachbereich Informatik, Univ. Frankfurt.

  61. Smolka, G. (1994). A foundation for higher-order concurrent constraint programming. In Proceedings of the 1st International Conference on Constraints in Computational Logics, Munich (Germany) (J.-P. Jouannaud, editor), volume 845 of Lecture Notes in Computer Science, pages 50–72, Springer-Verlag.

  62. Smolka, G. (1995). The oz programming model. In Current Trends in Computer Science (J. van Leeuwen, editor), volume 1000 of Lecture Notes in Computer Science, pages 324–343.

  63. Smolka, G., & Aït-Kaci, H. (1990). Inheritance hierarchies: Semantics and unification. In Unification (C. Kirchner, editor), pages 489–516, London, Academic Press Inc.

    Google Scholar 

  64. Stickel, M. E. (1975). A complete unification algorithm for associative-commutative functions. In Proceedings 4th International Joint Conference on Artificial Intelligence, Tbilissi (USSR), pages 71–76.

  65. Tajine, M. (1993). The negation elimination from syntactic equational formulas is decidable. In Proc. 5th Rewriting Techniques and Applications, Montr´eal, LNCS 690 (C. Kirchner, editor).

  66. Thomas, W. (1990). Automata on infinite objects. In Handbook of Theoretical Computer Science (J. van Leeuwen, editor), pages 134–191, Elsevier.

  67. Tidén, E. (1986). Unification in combinations of collapse-free theories with disjoint sets of functions symbols.In Proceedings 8th International Conference on Automated Deduction, Oxford (UK) (J. Siekmann, editor), volume 230 of Lecture Notes in Computer Science, pages 431–449, Springer-Verlag.

  68. Tomás, A. P., & Filgueiras, M. (1997). Solving linear diophantine equations using the geometric structure of the solution space. In Proc. 8th Conf. Rewriting Techniques and Applications (H. Comon, editor), volume 1232 of Lecture Notes in Computer Science, pages 269–283.

  69. Tommasi, M. (1994). Automates et contraintes ensemblistes. Th´ese de l'Univ. de Lille.

  70. Treinen, R. (1992). A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437–458.

    Google Scholar 

  71. Treinen, R. (1997). Feature trees over arbitrary structures. In Specifying Syntactic Structures (P. Blackburn and M. de Rijke, editors), chapter 7, pages 185–211, CSLI Publications and FoLLI.

  72. Yelick, K. (1987). Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation, 3(1 & 2):153–182.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, Ecole Normale Supérieure de Cachan, 61 Ave. Président Wilson, 94235, Cachan Cedex, France

    Hubert Comon

  2. COSYTEC, Parc Club Orsay Université, 4 Rue Jean Rostand, 91893, Orsay Cedex, France

    Mehmet Dincbas

  3. CNRS and LRI, Bat. 490, Université de Paris Sud, 91405, ORSAY Cedex, France

    Jean-Pierre Jouannaud

  4. LORIA & INRIA, 615 Rue du Jardin Botanique, 54602, Villers-lès-Nancy Cedex, France

    Claude Kirchner

Authors
  1. Hubert Comon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mehmet Dincbas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean-Pierre Jouannaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Claude Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Comon, H., Dincbas, M., Jouannaud, JP. et al. A Methodological View of Constraint Solving. Constraints 4, 337–361 (1999). https://doi.org/10.1023/A:1009868906501

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1009868906501

Search

Navigation