A multi-theory constraint satisfaction system

ABSTRACT

Constraint satisfaction systems are usually designed to work within a single-theory. This paper presents an approach to multi-theory constraint satisfaction characterized by cooperation among a variety of single-theory specialists. The system consists of three main components: a blackboard, a controlling Refine procedure, and a set of specialists. Two essential techniques used in our system are item propagation and case splitting. Potential applications of this system include software testing and analysis tools.

REFERENCES

• 1: W. Bibel, Constraint satisfaction from a deductive viewpoint (Research Note), Artificial Intelligence, v.35 n.3, p.401-416, July 1988 [doi>10.1016/0004-3702(88)90023-9]
• 2: Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 3: Lori A. Clarke , Debra J. Richardson , Steven J. Zeil, TEAM: a support environment for testing, evaluation, and analysis, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.153-162, November 28-30, 1988, Boston, Massachusetts, United States
• 4: Jacques Cohen, Constraint logic programming languages, Communications of the ACM, v.33 n.7, p.52-68, July 1990 [doi>10.1145/79204.79209]
• 5: G. Huet and D. OPtgn. Equations and rewriting roles: a survey. In R. Book, editor, Formal Languages: Perspecti~es and Open Problems. Academic Press, 1980.
• 6: Joxan Jaffar , Spiro Michaylov , Peter J. Stuckey , Roland H. C. Yap, The CLP( R ) language and system, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.339-395, July 1992 [doi>10.1145/129393.129398]
• 7: William Leler, Constraint programming languages: their specification and generation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 8: A. IC Mackworth. Consistency in netwot~ of relations. Artificial Intelligence, 8(1):99-118, Fe~. 1977.
• 9: Zohar Manna , Richard Waldinger, The logical basis for computer programming. Volume 1: deductive reasoning, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985
• 10: Ramon E. Moore , Fritz Bierbaum, Methods and Applications of Interval Analysis (SIAM Studies in Applied and Numerical Mathematics) (Siam Studies in Applied Mathematics, 2.), Soc for Industrial & Applied Math, 1979
• 11: IC Murty. /.a'near Programmin8. Wiley, New York, 1983.
• 12: B. A. Nadel. The consistent labeling problem, part 1: Background and problem formulation. Technical Report DCS-TR-164, University of Michigan, Nov. 1985.
• 13: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 14: Manfred Schmidt-Schaub, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, v.8 n.1-2, p.51-99, Jul./Aug. 1989 [doi>10.1016/S0747-7171(89)80022-7]
• 15: Robert E. Shostak, On the SUP-INF Method for Proving Presburger Formulas, Journal of the ACM (JACM), v.24 n.4, p.529-543, Oct. 1977 [doi>10.1145/322033.322034]
• 16: Robert E. Shostak, Deciding Combinations of Theories, Proceedings of the 6th Conference on Automated Deduction, p.209-222, June 07-09, 1982
• 17: Jörg H. Siekmann, Unification theory, Journal of Symbolic Computation, v.7 n.3-4, p.207-274, March/April 1989 [doi>10.1016/S0747-7171(89)80012-4]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Linear programming

General Terms:
Algorithms, Languages, Theory