Tractable constraints in finite semilattices

  • Jakob Rehof
  • Torben Æ. Mogensen
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


We introduce the notion of definite inequality constraints involving monotone functions in a finite meet-semilattice, generalizing the logical notion of Horn-clauses, and we give a linear time algorithm for deciding satisfiability. We characterize the expressiveness of the framework of definite constraints and show that the algorithm uniformly solves exactly the set of all meet-closed relational constraint problems, running with small linear time constant factors for any fixed problem. We give an alternative technique which reduces inequalities to satisfiability of Horn-clauses (hornsat) and study its efficiency. Finally, we show that the algorithm is complete for a maximal class of tractable constraints, by proving that any strict extension will lead to NP-hard problems in any meet-semilattice.


Finite semilattices constraint satisfiability program analysis tractability algorithms 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference. In Proc. 23rd Annual ACM Symposium on Principles of Programming Languages (POPL), pages 171–183. ACM Press, January 1996.Google Scholar
  2. 2.
    L. Birkedal and M. Welinder. Binding-time analysis for Standard ML. Lisp and Symbolic Computation, 8(3):191–208, September 1995.Google Scholar
  3. 3.
    A. Bondorf and J. JØrgensen. Efficient analyses for realistic off-line partial evaluation. Journal of Functional Programming, 3(3):315–346, July 1993.Google Scholar
  4. 4.
    C.C. Chang and H.J. Keisler. Model Theory. Studies in Logic and the Foundation of Mathematics, Vol. 73, 3rd ed., North Holland, 1990.Google Scholar
  5. 5.
    B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks, Cambridge University Press, 1990.Google Scholar
  6. 6.
    R. Dechter and J. Pearl. Structure identification in relational data. Artificial Intelligence, 58:237–270, 1992.CrossRefGoogle Scholar
  7. 7.
    William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 3:267–284, 1984.CrossRefGoogle Scholar
  8. 8.
    Dirk Dussart, Fritz Henglein, and Christian Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Proc. 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland, Lecture Notes in Computer Science. Springer-Verlag, September 1995.Google Scholar
  9. 9.
    M. Garey and D. Johnson. Computers and Intractability — A Guide to the Theory of NP-Completeness, Freeman, 1979.Google Scholar
  10. 10.
    R. Greenlaw, H.J. Hoover, and W. Ruzzo. Limits to Parallel Computation. P-Completeness Theory. Oxford University Press, 1995.Google Scholar
  11. 11.
    F. Henglein. Efficient type inference for higher-order binding-time analysis. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, Cambridge, Massachusetts, August 1991 (Lecture Notes in Computer Science, vol. 523), pages 448–472. ACM, Berlin: Springer-Verlag, 1991.Google Scholar
  12. 12.
    W. Hodges. Model Theory. Encyclopedia of Mathematics and its Applications, Vol. 42, Cambridge University Press, 1993.Google Scholar
  13. 13.
    P. Jeavons and M. Cooper. Tractable constraints on ordered domains. Artificial Intelligence, 79:327–339, 1995.Google Scholar
  14. 14.
    Peter Jeavons and David Cohen. An algebraic characterization of tractable constraints. In First Annual Conference on Computing and Combinatorics (COCOON), pages 633–642. Springer Verlag, LNCS 959, 1995.Google Scholar
  15. 15.
    Peter Jeavons, David Cohen, and Marc Gyssens. A unifying framework for tractable constraints. In First International Conference on Principles and Practice of Constraint Programming, pages 276–291. Springer Verlag, LNCS 976, 1995.Google Scholar
  16. 16.
    G. Kildall. A unified approach to global program optimization. Proc. ACM Symp. on Principles of Programming Languages (POPL), 1973.Google Scholar
  17. 17.
    T. Æ. Mogensen. Types for 0, 1 or many uses. Technical report, In preparation, 1996.Google Scholar
  18. 18.
    Vaughan Pratt and Jerzy Tiuryn. Satisfiability of inequalities in a poset. Studia Logica, Helene Rasiowa memorial issue (to appear), 1996.Google Scholar
  19. 19.
    Jakob Rehof and Torben Mogensen. Report on tractable constraints in finite semilattices. Technical report, DIKU, Dept. of Computer Science, University of Copenhagen, Denmark, Available at rehof/publications.html, 1996.Google Scholar
  20. 20.
    Thomas J. Schaefer. The complexity of satisfiability problems. In Tenth Annual Symposium on the Theory of Computing (STOC), pages 216–226. ACM, 1978.Google Scholar
  21. 21.
    Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λcalculus using a stack of regions. In Proc. 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Portland, Oregon. ACM, ACM Press, January 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Jakob Rehof
    • 1
  • Torben Æ. Mogensen
    • 1
  1. 1.Department of Computer ScienceDIKUCopenhagen ØDenmark

Personalised recommendations